Documentation

Mathlib.Analysis.InnerProductSpace.Calculus

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.

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
Instances For
    @[simp]
    theorem fderivInnerCLM_apply (π•œ : Type u_1) {E : Type u_2} [RCLike π•œ] [NormedAddCommGroup E] [InnerProductSpace π•œ E] [NormedSpace ℝ E] (p : E Γ— E) (x : E Γ— E) :
    (fderivInnerCLM π•œ p) x = βŸͺp.1, x.2⟫_π•œ + βŸͺx.1, p.2⟫_π•œ
    theorem contDiff_inner {π•œ : Type u_1} {E : Type u_2} [RCLike π•œ] [NormedAddCommGroup E] [InnerProductSpace π•œ E] [NormedSpace ℝ E] {n : β„•βˆž} :
    ContDiff ℝ n fun (p : E Γ— E) => βŸͺ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 : β„•βˆž} :
    ContDiffAt ℝ n (fun (p : E Γ— E) => βŸͺ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) => βŸͺ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 β†’ E} {g : G β†’ E} {s : Set G} {x : G} {n : β„•βˆž} (hf : ContDiffWithinAt ℝ n f s x) (hg : ContDiffWithinAt ℝ n g s x) :
    ContDiffWithinAt ℝ n (fun (x : G) => βŸͺ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 β†’ E} {g : G β†’ E} {x : G} {n : β„•βˆž} (hf : ContDiffAt ℝ n f x) (hg : ContDiffAt ℝ n g x) :
    ContDiffAt ℝ n (fun (x : G) => βŸͺ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 β†’ E} {g : G β†’ E} {s : Set G} {n : β„•βˆž} (hf : ContDiffOn ℝ n f s) (hg : ContDiffOn ℝ n g s) :
    ContDiffOn ℝ n (fun (x : G) => βŸͺ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 β†’ E} {g : G β†’ E} {n : β„•βˆž} (hf : ContDiff ℝ n f) (hg : ContDiff ℝ n g) :
    ContDiff ℝ n fun (x : G) => βŸͺ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 β†’ E} {g : G β†’ E} {f' : G β†’L[ℝ] E} {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) => βŸͺf t, g t⟫_π•œ) ((fderivInnerCLM π•œ (f x, g x)).comp (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 β†’ E} {g : G β†’ E} {f' : G β†’L[ℝ] E} {g' : G β†’L[ℝ] E} {x : G} (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) :
    HasStrictFDerivAt (fun (t : G) => βŸͺf t, g t⟫_π•œ) ((fderivInnerCLM π•œ (f x, g x)).comp (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 β†’ E} {g : G β†’ E} {f' : G β†’L[ℝ] E} {g' : G β†’L[ℝ] E} {x : G} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
    HasFDerivAt (fun (t : G) => βŸͺf t, g t⟫_π•œ) ((fderivInnerCLM π•œ (f x, g x)).comp (f'.prod g')) x
    theorem HasDerivWithinAt.inner (π•œ : Type u_1) {E : Type u_2} [RCLike π•œ] [NormedAddCommGroup E] [InnerProductSpace π•œ E] [NormedSpace ℝ E] {f : ℝ β†’ E} {g : ℝ β†’ E} {f' : E} {g' : E} {s : Set ℝ} {x : ℝ} (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) :
    HasDerivWithinAt (fun (t : ℝ) => βŸͺf t, g t⟫_π•œ) (βŸͺf x, g'⟫_π•œ + βŸͺf', g x⟫_π•œ) s x
    theorem HasDerivAt.inner (π•œ : Type u_1) {E : Type u_2} [RCLike π•œ] [NormedAddCommGroup E] [InnerProductSpace π•œ E] [NormedSpace ℝ E] {f : ℝ β†’ E} {g : ℝ β†’ E} {f' : E} {g' : E} {x : ℝ} :
    HasDerivAt f f' x β†’ HasDerivAt g g' x β†’ HasDerivAt (fun (t : ℝ) => βŸͺf t, g t⟫_π•œ) (βŸͺf x, g'⟫_π•œ + βŸͺ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 β†’ E} {g : G β†’ E} {s : Set G} {x : G} (hf : DifferentiableWithinAt ℝ f s x) (hg : DifferentiableWithinAt ℝ g s x) :
    DifferentiableWithinAt ℝ (fun (x : G) => βŸͺ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 β†’ E} {g : G β†’ E} {x : G} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) :
    DifferentiableAt ℝ (fun (x : G) => βŸͺ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 β†’ E} {g : G β†’ E} {s : Set G} (hf : DifferentiableOn ℝ f s) (hg : DifferentiableOn ℝ g s) :
    DifferentiableOn ℝ (fun (x : G) => βŸͺ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 β†’ E} {g : G β†’ E} (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) :
    Differentiable ℝ fun (x : G) => βŸͺ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 β†’ E} {g : G β†’ E} {x : G} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (y : G) :
    (fderiv ℝ (fun (t : G) => βŸͺf t, g t⟫_π•œ) x) y = βŸͺf x, (fderiv ℝ g x) y⟫_π•œ + βŸͺ(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 : ℝ β†’ E} {g : ℝ β†’ E} {x : ℝ} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) :
    deriv (fun (t : ℝ) => βŸͺf t, g t⟫_π•œ) x = βŸͺf x, deriv g x⟫_π•œ + βŸͺderiv f x, g x⟫_π•œ
    theorem contDiff_norm_sq (π•œ : Type u_1) {E : Type u_2} [RCLike π•œ] [NormedAddCommGroup E] [InnerProductSpace π•œ E] [NormedSpace ℝ E] {n : β„•βˆž} :
    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 : β„•βˆž} (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 : β„•βˆž} (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 : β„•βˆž} (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 : β„•βˆž} {x : E} (hx : x β‰  0) :
    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 : β„•βˆž} (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 β†’ E} {g : G β†’ E} {x : G} {n : β„•βˆž} (hf : ContDiffAt ℝ n f x) (hg : ContDiffAt ℝ n g x) (hne : f x β‰  g x) :
    ContDiffAt ℝ n (fun (y : G) => 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 : β„•βˆž} (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 β†’ E} {g : G β†’ E} {s : Set G} {x : G} {n : β„•βˆž} (hf : ContDiffWithinAt ℝ n f s x) (hg : ContDiffWithinAt ℝ n g s x) (hne : f x β‰  g x) :
    ContDiffWithinAt ℝ n (fun (y : G) => 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 : β„•βˆž} (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 : β„•βˆž} (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 β†’ E} {g : G β†’ E} {s : Set G} {n : β„•βˆž} (hf : ContDiffOn ℝ n f s) (hg : ContDiffOn ℝ n g s) (hne : βˆ€ x ∈ s, f x β‰  g x) :
    ContDiffOn ℝ n (fun (y : G) => 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 : β„•βˆž} (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 β†’ E} {g : G β†’ E} {n : β„•βˆž} (hf : ContDiff ℝ n f) (hg : ContDiff ℝ n g) (hne : βˆ€ (x : G), f x β‰  g x) :
    ContDiff ℝ n fun (y : G) => dist (f y) (g y)
    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)).comp 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 * βŸͺ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)).comp 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 * βŸͺ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 β†’ E} {g : G β†’ E} {x : G} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (hne : f x β‰  g x) :
    DifferentiableAt ℝ (fun (y : G) => 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) :
    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 β†’ E} {g : G β†’ E} (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) (hne : βˆ€ (x : G), f x β‰  g x) :
    Differentiable ℝ fun (y : G) => 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) :
    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 β†’ E} {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 (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 β†’ E} {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 (f y) (g y)) s
    theorem differentiableWithinAt_euclidean {π•œ : Type u_1} {ΞΉ : Type u_2} {H : Type u_3} [RCLike π•œ] [NormedAddCommGroup H] [NormedSpace π•œ H] [Fintype ΞΉ] {f : H β†’ EuclideanSpace π•œ ΞΉ} {t : Set H} {y : H} :
    DifferentiableWithinAt π•œ f t y ↔ βˆ€ (i : ΞΉ), DifferentiableWithinAt π•œ (fun (x : H) => f x i) t y
    theorem differentiableAt_euclidean {π•œ : Type u_1} {ΞΉ : Type u_2} {H : Type u_3} [RCLike π•œ] [NormedAddCommGroup H] [NormedSpace π•œ H] [Fintype ΞΉ] {f : H β†’ EuclideanSpace π•œ ΞΉ} {y : H} :
    DifferentiableAt π•œ f y ↔ βˆ€ (i : ΞΉ), DifferentiableAt π•œ (fun (x : H) => f x i) y
    theorem differentiableOn_euclidean {π•œ : Type u_1} {ΞΉ : Type u_2} {H : Type u_3} [RCLike π•œ] [NormedAddCommGroup H] [NormedSpace π•œ H] [Fintype ΞΉ] {f : H β†’ EuclideanSpace π•œ ΞΉ} {t : Set H} :
    DifferentiableOn π•œ f t ↔ βˆ€ (i : ΞΉ), DifferentiableOn π•œ (fun (x : H) => f x i) t
    theorem differentiable_euclidean {π•œ : Type u_1} {ΞΉ : Type u_2} {H : Type u_3} [RCLike π•œ] [NormedAddCommGroup H] [NormedSpace π•œ H] [Fintype ΞΉ] {f : H β†’ EuclideanSpace π•œ ΞΉ} :
    Differentiable π•œ f ↔ βˆ€ (i : ΞΉ), Differentiable π•œ fun (x : H) => f x i
    theorem hasStrictFDerivAt_euclidean {π•œ : Type u_1} {ΞΉ : Type u_2} {H : Type u_3} [RCLike π•œ] [NormedAddCommGroup H] [NormedSpace π•œ H] [Fintype ΞΉ] {f : H β†’ EuclideanSpace π•œ ΞΉ} {f' : H β†’L[π•œ] EuclideanSpace π•œ ΞΉ} {y : H} :
    HasStrictFDerivAt f f' y ↔ βˆ€ (i : ΞΉ), HasStrictFDerivAt (fun (x : H) => f x i) ((EuclideanSpace.proj i).comp f') y
    theorem hasFDerivWithinAt_euclidean {π•œ : Type u_1} {ΞΉ : Type u_2} {H : Type u_3} [RCLike π•œ] [NormedAddCommGroup H] [NormedSpace π•œ H] [Fintype ΞΉ] {f : H β†’ EuclideanSpace π•œ ΞΉ} {f' : H β†’L[π•œ] EuclideanSpace π•œ ΞΉ} {t : Set H} {y : H} :
    HasFDerivWithinAt f f' t y ↔ βˆ€ (i : ΞΉ), HasFDerivWithinAt (fun (x : H) => f x i) ((EuclideanSpace.proj i).comp f') t y
    theorem contDiffWithinAt_euclidean {π•œ : Type u_1} {ΞΉ : Type u_2} {H : Type u_3} [RCLike π•œ] [NormedAddCommGroup H] [NormedSpace π•œ H] [Fintype ΞΉ] {f : H β†’ EuclideanSpace π•œ ΞΉ} {t : Set H} {y : H} {n : β„•βˆž} :
    ContDiffWithinAt π•œ n f t y ↔ βˆ€ (i : ΞΉ), ContDiffWithinAt π•œ n (fun (x : H) => f x i) t y
    theorem contDiffAt_euclidean {π•œ : Type u_1} {ΞΉ : Type u_2} {H : Type u_3} [RCLike π•œ] [NormedAddCommGroup H] [NormedSpace π•œ H] [Fintype ΞΉ] {f : H β†’ EuclideanSpace π•œ ΞΉ} {y : H} {n : β„•βˆž} :
    ContDiffAt π•œ n f y ↔ βˆ€ (i : ΞΉ), ContDiffAt π•œ n (fun (x : H) => f x i) y
    theorem contDiffOn_euclidean {π•œ : Type u_1} {ΞΉ : Type u_2} {H : Type u_3} [RCLike π•œ] [NormedAddCommGroup H] [NormedSpace π•œ H] [Fintype ΞΉ] {f : H β†’ EuclideanSpace π•œ ΞΉ} {t : Set H} {n : β„•βˆž} :
    ContDiffOn π•œ n f t ↔ βˆ€ (i : ΞΉ), ContDiffOn π•œ n (fun (x : H) => f x i) t
    theorem contDiff_euclidean {π•œ : Type u_1} {ΞΉ : Type u_2} {H : Type u_3} [RCLike π•œ] [NormedAddCommGroup H] [NormedSpace π•œ H] [Fintype ΞΉ] {f : H β†’ EuclideanSpace π•œ ΞΉ} {n : β„•βˆž} :
    ContDiff π•œ n f ↔ βˆ€ (i : ΞΉ), ContDiff π•œ n fun (x : H) => f x i
    theorem PartialHomeomorph.contDiff_univUnitBall {n : β„•βˆž} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] :
    ContDiff ℝ n ↑PartialHomeomorph.univUnitBall
    theorem PartialHomeomorph.contDiffOn_univUnitBall_symm {n : β„•βˆž} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] :
    ContDiffOn ℝ n (↑PartialHomeomorph.univUnitBall.symm) (Metric.ball 0 1)
    theorem Homeomorph.contDiff_unitBall {n : β„•βˆž} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] :
    ContDiff ℝ n fun (x : E) => ↑(Homeomorph.unitBall x)