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 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 (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 (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 (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 (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 (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 : G β†’ E} {f' g' : G β†’L[ℝ] E} {x : G} (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) :
    HasStrictFDerivAt (fun (t : G) => inner (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 : G β†’ E} {f' g' : G β†’L[ℝ] E} {x : G} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
    HasFDerivAt (fun (t : G) => inner (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 g : ℝ β†’ E} {f' g' : E} {s : Set ℝ} {x : ℝ} (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) :
    HasDerivWithinAt (fun (t : ℝ) => inner (f t) (g t)) (inner (f x) g' + 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 (f t) (g t)) (inner (f x) g' + 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 (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 (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 (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 (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) :
    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 (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 (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 (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 (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 * 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)).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 * 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 (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 : 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 : 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 : 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

    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] [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) ((PiLp.proj 2 (fun (x : ΞΉ) => π•œ) 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) ((PiLp.proj 2 (fun (x : ΞΉ) => π•œ) 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 : WithTop β„•βˆž} :
    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 : WithTop β„•βˆž} :
    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 : WithTop β„•βˆž} :
    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 : WithTop β„•βˆž} :
    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)