# 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`.

source
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

Instances For

source
@[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
source
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
source
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
source
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
source
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
source
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
source
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
source
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)
source
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)).comp (f'.prod g')) s x
source
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)).comp (f'.prod g')) x
source
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)).comp (f'.prod g')) x
source
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
source
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
source
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
source
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
source
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
source
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)
source
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)
source
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)
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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‖
source
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)
source
theorem hasStrictFDerivAt_norm_sq {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) :
HasStrictFDerivAt (fun (x : F) => ‖x‖ ^ 2) (2 • (innerSL ℝ) x) x
source
@[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
source
theorem fderiv_norm_sq {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] :
(fderiv ℝ fun (x : F) => ‖x‖ ^ 2) = 2 • ⇑(innerSL ℝ)
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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‖
source
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)
source
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
source
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
source
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
source
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
source
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
source
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` #

source
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).ofLp i) t y
source
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).ofLp i) y
source
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).ofLp i) t
source
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).ofLp i
source
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).ofLp i) ((PiLp.proj 2 (fun (x : ι) => 𝕜) i).comp f') y
source
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).ofLp i) ((PiLp.proj 2 (fun (x : ι) => 𝕜) i).comp f') t y
source
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).ofLp i) t y
source
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).ofLp i) y
source
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).ofLp i) t
source
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).ofLp i
source
theorem OpenPartialHomeomorph.contDiff_univUnitBall {n : ℕ∞} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] :
ContDiff ℝ ↑n ↑univUnitBall
source
theorem OpenPartialHomeomorph.contDiffOn_univUnitBall_symm {n : ℕ∞} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] :
ContDiffOn ℝ (↑n) (↑univUnitBall.symm) (Metric.ball 0 1)
source
theorem Homeomorph.contDiff_unitBall {n : ℕ∞} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] :
ContDiff ℝ ↑n fun (x : E) => ↑(unitBall x)
source
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)
source
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
source
theorem OpenPartialHomeomorph.contDiff_univBall {n : ℕ∞} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {c : E} {r : ℝ} :
ContDiff ℝ ↑n ↑(univBall c r)
source
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)