Calculus in inner product spaces

In this file we prove that the inner product and square of the norm in an inner space are infinitely ℝ-smooth. In order to state these results, we need a NormedSpace ℝ E instance. Though we can deduce this structure from InnerProductSpace 𝕜 E, this instance may be not definitionally equal to some other “natural” instance. So, we assume [NormedSpace ℝ E].

We also prove that functions to a EuclideanSpace are (higher) differentiable if and only if their components are. This follows from the corresponding fact for finite product of normed spaces, and from the equivalence of norms in finite dimensions.

TODO

The last part of the file should be generalized to PiLp.

noncomputable def fderivInnerCLM (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] (p : E × E) : E × E →L[ℝ] 𝕜

Derivative of the inner product.

Equations

• fderivInnerCLM 𝕜 p = ⋯.deriv p

@[simp]

theorem fderivInnerCLM_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] (p x : E × E) : (fderivInnerCLM 𝕜 p) x = inner 𝕜 p.1 x.2 + inner 𝕜 x.1 p.2

theorem contDiff_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {n : WithTop ℕ∞} : ContDiff ℝ n fun (p : E × E) => inner 𝕜 p.1 p.2

theorem contDiffAt_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {p : E × E} {n : WithTop ℕ∞} : ContDiffAt ℝ n (fun (p : E × E) => inner 𝕜 p.1 p.2) p

theorem differentiable_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] : Differentiable ℝ fun (p : E × E) => inner 𝕜 p.1 p.2

theorem ContDiffWithinAt.inner (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {s : Set G} {x : G} {n : WithTop ℕ∞} (hf : ContDiffWithinAt ℝ n f s x) (hg : ContDiffWithinAt ℝ n g s x) : ContDiffWithinAt ℝ n (fun (x : G) => Inner.inner 𝕜 (f x) (g x)) s x

theorem ContDiffAt.inner (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {x : G} {n : WithTop ℕ∞} (hf : ContDiffAt ℝ n f x) (hg : ContDiffAt ℝ n g x) : ContDiffAt ℝ n (fun (x : G) => Inner.inner 𝕜 (f x) (g x)) x

theorem ContDiffOn.inner (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {s : Set G} {n : WithTop ℕ∞} (hf : ContDiffOn ℝ n f s) (hg : ContDiffOn ℝ n g s) : ContDiffOn ℝ n (fun (x : G) => Inner.inner 𝕜 (f x) (g x)) s

theorem ContDiff.inner (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {n : WithTop ℕ∞} (hf : ContDiff ℝ n f) (hg : ContDiff ℝ n g) : ContDiff ℝ n fun (x : G) => Inner.inner 𝕜 (f x) (g x)

theorem HasFDerivWithinAt.inner (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {f' g' : G →L[ℝ] E} {s : Set G} {x : G} (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) : HasFDerivWithinAt (fun (t : G) => Inner.inner 𝕜 (f t) (g t)) (fderivInnerCLM 𝕜 (f x, g x) ∘SL f'.prod g') s x

theorem HasStrictFDerivAt.inner (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {f' g' : G →L[ℝ] E} {x : G} (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) : HasStrictFDerivAt (fun (t : G) => Inner.inner 𝕜 (f t) (g t)) (fderivInnerCLM 𝕜 (f x, g x) ∘SL f'.prod g') x

theorem HasFDerivAt.inner (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {f' g' : G →L[ℝ] E} {x : G} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) : HasFDerivAt (fun (t : G) => Inner.inner 𝕜 (f t) (g t)) (fderivInnerCLM 𝕜 (f x, g x) ∘SL f'.prod g') x

theorem HasDerivWithinAt.inner (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {f g : ℝ → E} {f' g' : E} {s : Set ℝ} {x : ℝ} (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) : HasDerivWithinAt (fun (t : ℝ) => Inner.inner 𝕜 (f t) (g t)) (Inner.inner 𝕜 (f x) g' + Inner.inner 𝕜 f' (g x)) s x

theorem HasDerivAt.inner (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {f g : ℝ → E} {f' g' : E} {x : ℝ} : HasDerivAt f f' x → HasDerivAt g g' x → HasDerivAt (fun (t : ℝ) => Inner.inner 𝕜 (f t) (g t)) (Inner.inner 𝕜 (f x) g' + Inner.inner 𝕜 f' (g x)) x

theorem DifferentiableWithinAt.inner (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {s : Set G} {x : G} (hf : DifferentiableWithinAt ℝ f s x) (hg : DifferentiableWithinAt ℝ g s x) : DifferentiableWithinAt ℝ (fun (x : G) => Inner.inner 𝕜 (f x) (g x)) s x

theorem DifferentiableAt.inner (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {x : G} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) : DifferentiableAt ℝ (fun (x : G) => Inner.inner 𝕜 (f x) (g x)) x

theorem DifferentiableOn.inner (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {s : Set G} (hf : DifferentiableOn ℝ f s) (hg : DifferentiableOn ℝ g s) : DifferentiableOn ℝ (fun (x : G) => Inner.inner 𝕜 (f x) (g x)) s

theorem Differentiable.inner (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) : Differentiable ℝ fun (x : G) => Inner.inner 𝕜 (f x) (g x)

theorem fderiv_inner_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {x : G} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (y : G) : (fderiv ℝ (fun (t : G) => inner 𝕜 (f t) (g t)) x) y = inner 𝕜 (f x) ((fderiv ℝ g x) y) + inner 𝕜 ((fderiv ℝ f x) y) (g x)

theorem deriv_inner_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {f g : ℝ → E} {x : ℝ} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) : deriv (fun (t : ℝ) => inner 𝕜 (f t) (g t)) x = inner 𝕜 (f x) (deriv g x) + inner 𝕜 (deriv f x) (g x)

theorem contDiff_norm_sq (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {n : WithTop ℕ∞} : ContDiff ℝ n fun (x : E) => ‖x‖ ^ 2

theorem ContDiff.norm_sq (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : G → E} {n : WithTop ℕ∞} (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : G) => ‖f x‖ ^ 2

theorem ContDiffWithinAt.norm_sq (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : G → E} {s : Set G} {x : G} {n : WithTop ℕ∞} (hf : ContDiffWithinAt ℝ n f s x) : ContDiffWithinAt ℝ n (fun (y : G) => ‖f y‖ ^ 2) s x

theorem ContDiffAt.norm_sq (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : G → E} {x : G} {n : WithTop ℕ∞} (hf : ContDiffAt ℝ n f x) : ContDiffAt ℝ n (fun (x : G) => ‖f x‖ ^ 2) x

theorem contDiffAt_norm (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {n : WithTop ℕ∞} {x : E} (hx : x ≠ 0) : ContDiffAt ℝ n norm x

theorem ContDiffAt.norm (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : G → E} {x : G} {n : WithTop ℕ∞} (hf : ContDiffAt ℝ n f x) (h0 : f x ≠ 0) : ContDiffAt ℝ n (fun (y : G) => ‖f y‖) x

theorem ContDiffAt.dist (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {x : G} {n : WithTop ℕ∞} (hf : ContDiffAt ℝ n f x) (hg : ContDiffAt ℝ n g x) (hne : f x ≠ g x) : ContDiffAt ℝ n (fun (y : G) => Dist.dist (f y) (g y)) x

theorem ContDiffWithinAt.norm (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : G → E} {s : Set G} {x : G} {n : WithTop ℕ∞} (hf : ContDiffWithinAt ℝ n f s x) (h0 : f x ≠ 0) : ContDiffWithinAt ℝ n (fun (y : G) => ‖f y‖) s x

theorem ContDiffWithinAt.dist (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {s : Set G} {x : G} {n : WithTop ℕ∞} (hf : ContDiffWithinAt ℝ n f s x) (hg : ContDiffWithinAt ℝ n g s x) (hne : f x ≠ g x) : ContDiffWithinAt ℝ n (fun (y : G) => Dist.dist (f y) (g y)) s x

theorem ContDiffOn.norm_sq (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : G → E} {s : Set G} {n : WithTop ℕ∞} (hf : ContDiffOn ℝ n f s) : ContDiffOn ℝ n (fun (y : G) => ‖f y‖ ^ 2) s

theorem ContDiffOn.norm (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : G → E} {s : Set G} {n : WithTop ℕ∞} (hf : ContDiffOn ℝ n f s) (h0 : ∀ x ∈ s, f x ≠ 0) : ContDiffOn ℝ n (fun (y : G) => ‖f y‖) s

theorem ContDiffOn.dist (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {s : Set G} {n : WithTop ℕ∞} (hf : ContDiffOn ℝ n f s) (hg : ContDiffOn ℝ n g s) (hne : ∀ x ∈ s, f x ≠ g x) : ContDiffOn ℝ n (fun (y : G) => Dist.dist (f y) (g y)) s

theorem ContDiff.norm (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : G → E} {n : WithTop ℕ∞} (hf : ContDiff ℝ n f) (h0 : ∀ (x : G), f x ≠ 0) : ContDiff ℝ n fun (y : G) => ‖f y‖

theorem ContDiff.dist (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {n : WithTop ℕ∞} (hf : ContDiff ℝ n f) (hg : ContDiff ℝ n g) (hne : ∀ (x : G), f x ≠ g x) : ContDiff ℝ n fun (y : G) => Dist.dist (f y) (g y)

theorem hasStrictFDerivAt_norm_sq {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) : HasStrictFDerivAt (fun (x : F) => ‖x‖ ^ 2) (2 • (innerSL ℝ) x) x

@[simp]

theorem fderiv_norm_sq_apply {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) : fderiv ℝ (fun (x : F) => ‖x‖ ^ 2) x = 2 • (innerSL ℝ) x

theorem fderiv_norm_sq {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] : (fderiv ℝ fun (x : F) => ‖x‖ ^ 2) = 2 • ⇑(innerSL ℝ)

theorem HasFDerivAt.norm_sq {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {x : G} {f : G → F} {f' : G →L[ℝ] F} (hf : HasFDerivAt f f' x) : HasFDerivAt (fun (x : G) => ‖f x‖ ^ 2) (2 • (innerSL ℝ) (f x) ∘SL f') x

theorem HasDerivAt.norm_sq {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {f : ℝ → F} {f' : F} {x : ℝ} (hf : HasDerivAt f f' x) : HasDerivAt (fun (x : ℝ) => ‖f x‖ ^ 2) (2 * Inner.inner ℝ (f x) f') x

theorem HasFDerivWithinAt.norm_sq {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {s : Set G} {x : G} {f : G → F} {f' : G →L[ℝ] F} (hf : HasFDerivWithinAt f f' s x) : HasFDerivWithinAt (fun (x : G) => ‖f x‖ ^ 2) (2 • (innerSL ℝ) (f x) ∘SL f') s x

theorem HasDerivWithinAt.norm_sq {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {f : ℝ → F} {f' : F} {s : Set ℝ} {x : ℝ} (hf : HasDerivWithinAt f f' s x) : HasDerivWithinAt (fun (x : ℝ) => ‖f x‖ ^ 2) (2 * Inner.inner ℝ (f x) f') s x

theorem DifferentiableAt.norm_sq (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : G → E} {x : G} (hf : DifferentiableAt ℝ f x) : DifferentiableAt ℝ (fun (y : G) => ‖f y‖ ^ 2) x

theorem DifferentiableAt.norm (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : G → E} {x : G} (hf : DifferentiableAt ℝ f x) (h0 : f x ≠ 0) : DifferentiableAt ℝ (fun (y : G) => ‖f y‖) x

theorem DifferentiableAt.dist (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {x : G} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (hne : f x ≠ g x) : DifferentiableAt ℝ (fun (y : G) => Dist.dist (f y) (g y)) x

theorem Differentiable.norm_sq (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : G → E} (hf : Differentiable ℝ f) : Differentiable ℝ fun (y : G) => ‖f y‖ ^ 2

theorem Differentiable.norm (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : G → E} (hf : Differentiable ℝ f) (h0 : ∀ (x : G), f x ≠ 0) : Differentiable ℝ fun (y : G) => ‖f y‖

theorem Differentiable.dist (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) (hne : ∀ (x : G), f x ≠ g x) : Differentiable ℝ fun (y : G) => Dist.dist (f y) (g y)

theorem DifferentiableWithinAt.norm_sq (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : G → E} {s : Set G} {x : G} (hf : DifferentiableWithinAt ℝ f s x) : DifferentiableWithinAt ℝ (fun (y : G) => ‖f y‖ ^ 2) s x

theorem DifferentiableWithinAt.norm (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : G → E} {s : Set G} {x : G} (hf : DifferentiableWithinAt ℝ f s x) (h0 : f x ≠ 0) : DifferentiableWithinAt ℝ (fun (y : G) => ‖f y‖) s x

theorem DifferentiableWithinAt.dist (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {s : Set G} {x : G} (hf : DifferentiableWithinAt ℝ f s x) (hg : DifferentiableWithinAt ℝ g s x) (hne : f x ≠ g x) : DifferentiableWithinAt ℝ (fun (y : G) => Dist.dist (f y) (g y)) s x

theorem DifferentiableOn.norm_sq (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : G → E} {s : Set G} (hf : DifferentiableOn ℝ f s) : DifferentiableOn ℝ (fun (y : G) => ‖f y‖ ^ 2) s

theorem DifferentiableOn.norm (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : G → E} {s : Set G} (hf : DifferentiableOn ℝ f s) (h0 : ∀ x ∈ s, f x ≠ 0) : DifferentiableOn ℝ (fun (y : G) => ‖f y‖) s

theorem DifferentiableOn.dist (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {f g : G → E} {s : Set G} (hf : DifferentiableOn ℝ f s) (hg : DifferentiableOn ℝ g s) (hne : ∀ x ∈ s, f x ≠ g x) : DifferentiableOn ℝ (fun (y : G) => Dist.dist (f y) (g y)) s

Convenience aliases of PiLp lemmas for EuclideanSpace

theorem differentiableWithinAt_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {t : Set H} {y : H} [Finite ι] : DifferentiableWithinAt 𝕜 f t y ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun (x : H) => (f x).ofLp i) t y

theorem differentiableAt_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {y : H} [Finite ι] : DifferentiableAt 𝕜 f y ↔ ∀ (i : ι), DifferentiableAt 𝕜 (fun (x : H) => (f x).ofLp i) y

theorem differentiableOn_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {t : Set H} [Finite ι] : DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun (x : H) => (f x).ofLp i) t

theorem differentiable_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} [Finite ι] : Differentiable 𝕜 f ↔ ∀ (i : ι), Differentiable 𝕜 fun (x : H) => (f x).ofLp i

theorem hasStrictFDerivAt_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {f' : H →L[𝕜] EuclideanSpace 𝕜 ι} {y : H} [Finite ι] : HasStrictFDerivAt f f' y ↔ ∀ (i : ι), HasStrictFDerivAt (fun (x : H) => (f x).ofLp i) (PiLp.proj 2 (fun (x : ι) => 𝕜) i ∘SL f') y

theorem hasFDerivWithinAt_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {f' : H →L[𝕜] EuclideanSpace 𝕜 ι} {t : Set H} {y : H} [Finite ι] : HasFDerivWithinAt f f' t y ↔ ∀ (i : ι), HasFDerivWithinAt (fun (x : H) => (f x).ofLp i) (PiLp.proj 2 (fun (x : ι) => 𝕜) i ∘SL f') t y

theorem contDiffWithinAt_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {t : Set H} {y : H} [Fintype ι] {n : WithTop ℕ∞} : ContDiffWithinAt 𝕜 n f t y ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun (x : H) => (f x).ofLp i) t y

theorem contDiffAt_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {y : H} [Fintype ι] {n : WithTop ℕ∞} : ContDiffAt 𝕜 n f y ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun (x : H) => (f x).ofLp i) y

theorem contDiffOn_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {t : Set H} [Fintype ι] {n : WithTop ℕ∞} : ContDiffOn 𝕜 n f t ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun (x : H) => (f x).ofLp i) t

theorem contDiff_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} [Fintype ι] {n : WithTop ℕ∞} : ContDiff 𝕜 n f ↔ ∀ (i : ι), ContDiff 𝕜 n fun (x : H) => (f x).ofLp i

theorem OpenPartialHomeomorph.contDiff_univUnitBall {n : ℕ∞} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : ContDiff ℝ ↑n ↑univUnitBall

theorem OpenPartialHomeomorph.contDiffOn_univUnitBall_symm {n : ℕ∞} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : ContDiffOn ℝ (↑n) (↑univUnitBall.symm) (Metric.ball 0 1)

theorem Homeomorph.contDiff_unitBall {n : ℕ∞} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : ContDiff ℝ ↑n fun (x : E) => ↑(unitBall x)

theorem OpenPartialHomeomorph.contDiff_unitBallBall {n : ℕ∞} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {c : E} {r : ℝ} (hr : 0 < r) : ContDiff ℝ ↑n ↑(unitBallBall c r hr)

theorem OpenPartialHomeomorph.contDiff_unitBallBall_symm {n : ℕ∞} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {c : E} {r : ℝ} (hr : 0 < r) : ContDiff ℝ ↑n ↑(unitBallBall c r hr).symm

theorem OpenPartialHomeomorph.contDiff_univBall {n : ℕ∞} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {c : E} {r : ℝ} : ContDiff ℝ ↑n ↑(univBall c r)

theorem OpenPartialHomeomorph.contDiffOn_univBall_symm {n : ℕ∞} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {c : E} {r : ℝ} : ContDiffOn ℝ (↑n) (↑(univBall c r).symm) (Metric.ball c r)