# mathlib3documentation

analysis.inner_product_space.calculus

# Calculus in inner product spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 normed_space ℝ E instance. Though we can deduce this structure from inner_product_space 𝕜 E, this instance may be not definitionally equal to some other “natural” instance. So, we assume [normed_space ℝ E].

We also prove that functions to a euclidean_space 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 pi_Lp.

noncomputable def fderiv_inner_clm (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] (p : E × E) :
E × E →L[] 𝕜

Derivative of the inner product.

Equations
@[simp]
theorem fderiv_inner_clm_apply (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] (p x : E × E) :
p) x = +
theorem cont_diff_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {n : ℕ∞} :
(λ (p : E × E), p.snd)
theorem cont_diff_at_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {p : E × E} {n : ℕ∞} :
(λ (p : E × E), p.snd) p
theorem differentiable_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] :
(λ (p : E × E), p.snd)
theorem cont_diff_within_at.inner (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {s : set G} {x : G} {n : ℕ∞} (hf : s x) (hg : s x) :
(λ (x : G), has_inner.inner (f x) (g x)) s x
theorem cont_diff_at.inner (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {x : G} {n : ℕ∞} (hf : f x) (hg : g x) :
(λ (x : G), has_inner.inner (f x) (g x)) x
theorem cont_diff_on.inner (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {s : set G} {n : ℕ∞} (hf : f s) (hg : g s) :
(λ (x : G), has_inner.inner (f x) (g x)) s
theorem cont_diff.inner (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {n : ℕ∞} (hf : f) (hg : g) :
(λ (x : G), has_inner.inner (f x) (g x))
theorem has_fderiv_within_at.inner (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {f' g' : G →L[] E} {s : set G} {x : G} (hf : s x) (hg : s x) :
has_fderiv_within_at (λ (t : G), has_inner.inner (f t) (g t)) (f x, g x)).comp (f'.prod g')) s x
theorem has_strict_fderiv_at.inner (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {f' g' : G →L[] E} {x : G} (hf : x) (hg : x) :
has_strict_fderiv_at (λ (t : G), has_inner.inner (f t) (g t)) (f x, g x)).comp (f'.prod g')) x
theorem has_fderiv_at.inner (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {f' g' : G →L[] E} {x : G} (hf : f' x) (hg : g' x) :
has_fderiv_at (λ (t : G), has_inner.inner (f t) (g t)) (f x, g x)).comp (f'.prod g')) x
theorem has_deriv_within_at.inner (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {f g : E} {f' g' : E} {s : set } {x : } (hf : s x) (hg : s x) :
has_deriv_within_at (λ (t : ), has_inner.inner (f t) (g t)) (has_inner.inner (f x) g' + (g x)) s x
theorem has_deriv_at.inner (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {f g : E} {f' g' : E} {x : } :
f' x g' x has_deriv_at (λ (t : ), has_inner.inner (f t) (g t)) (has_inner.inner (f x) g' + (g x)) x
theorem differentiable_within_at.inner (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {s : set G} {x : G} (hf : x) (hg : x) :
(λ (x : G), has_inner.inner (f x) (g x)) s x
theorem differentiable_at.inner (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {x : G} (hf : x) (hg : x) :
(λ (x : G), has_inner.inner (f x) (g x)) x
theorem differentiable_on.inner (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {s : set G} (hf : s) (hg : s) :
(λ (x : G), has_inner.inner (f x) (g x)) s
theorem differentiable.inner (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} (hf : f) (hg : g) :
(λ (x : G), has_inner.inner (f x) (g x))
theorem fderiv_inner_apply (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {x : G} (hf : x) (hg : x) (y : G) :
(λ (t : G), has_inner.inner (f t) (g t)) x) y = has_inner.inner (f x) ( g x) y) + has_inner.inner ( f x) y) (g x)
theorem deriv_inner_apply (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {f g : E} {x : } (hf : x) (hg : x) :
deriv (λ (t : ), has_inner.inner (f t) (g t)) x = has_inner.inner (f x) (deriv g x) + has_inner.inner (deriv f x) (g x)
theorem cont_diff_norm_sq (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {n : ℕ∞} :
(λ (x : E), x ^ 2)
theorem cont_diff.norm_sq (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f : G E} {n : ℕ∞} (hf : f) :
(λ (x : G), f x ^ 2)
theorem cont_diff_within_at.norm_sq (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f : G E} {s : set G} {x : G} {n : ℕ∞} (hf : s x) :
(λ (y : G), f y ^ 2) s x
theorem cont_diff_at.norm_sq (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f : G E} {x : G} {n : ℕ∞} (hf : f x) :
(λ (y : G), f y ^ 2) x
theorem cont_diff_at_norm (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {n : ℕ∞} {x : E} (hx : x 0) :
theorem cont_diff_at.norm (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f : G E} {x : G} {n : ℕ∞} (hf : f x) (h0 : f x 0) :
(λ (y : G), f y) x
theorem cont_diff_at.dist (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {x : G} {n : ℕ∞} (hf : f x) (hg : g x) (hne : f x g x) :
(λ (y : G), has_dist.dist (f y) (g y)) x
theorem cont_diff_within_at.norm (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f : G E} {s : set G} {x : G} {n : ℕ∞} (hf : s x) (h0 : f x 0) :
(λ (y : G), f y) s x
theorem cont_diff_within_at.dist (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {s : set G} {x : G} {n : ℕ∞} (hf : s x) (hg : s x) (hne : f x g x) :
(λ (y : G), has_dist.dist (f y) (g y)) s x
theorem cont_diff_on.norm_sq (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f : G E} {s : set G} {n : ℕ∞} (hf : f s) :
(λ (y : G), f y ^ 2) s
theorem cont_diff_on.norm (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f : G E} {s : set G} {n : ℕ∞} (hf : f s) (h0 : (x : G), x s f x 0) :
(λ (y : G), f y) s
theorem cont_diff_on.dist (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {s : set G} {n : ℕ∞} (hf : f s) (hg : g s) (hne : (x : G), x s f x g x) :
(λ (y : G), has_dist.dist (f y) (g y)) s
theorem cont_diff.norm (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f : G E} {n : ℕ∞} (hf : f) (h0 : (x : G), f x 0) :
(λ (y : G), f y)
theorem cont_diff.dist (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {n : ℕ∞} (hf : f) (hg : g) (hne : (x : G), f x g x) :
(λ (y : G), has_dist.dist (f y) (g y))
theorem has_strict_fderiv_at_norm_sq {F : Type u_3} (x : F) :
has_strict_fderiv_at (λ (x : F), x ^ 2) (bit0 ((innerSL ) x)) x
theorem differentiable_at.norm_sq (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f : G E} {x : G} (hf : x) :
(λ (y : G), f y ^ 2) x
theorem differentiable_at.norm (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f : G E} {x : G} (hf : x) (h0 : f x 0) :
(λ (y : G), f y) x
theorem differentiable_at.dist (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {x : G} (hf : x) (hg : x) (hne : f x g x) :
(λ (y : G), has_dist.dist (f y) (g y)) x
theorem differentiable.norm_sq (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f : G E} (hf : f) :
(λ (y : G), f y ^ 2)
theorem differentiable.norm (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f : G E} (hf : f) (h0 : (x : G), f x 0) :
(λ (y : G), f y)
theorem differentiable.dist (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} (hf : f) (hg : g) (hne : (x : G), f x g x) :
(λ (y : G), has_dist.dist (f y) (g y))
theorem differentiable_within_at.norm_sq (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f : G E} {s : set G} {x : G} (hf : x) :
(λ (y : G), f y ^ 2) s x
theorem differentiable_within_at.norm (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f : G E} {s : set G} {x : G} (hf : x) (h0 : f x 0) :
(λ (y : G), f y) s x
theorem differentiable_within_at.dist (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {s : set G} {x : G} (hf : x) (hg : x) (hne : f x g x) :
(λ (y : G), has_dist.dist (f y) (g y)) s x
theorem differentiable_on.norm_sq (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f : G E} {s : set G} (hf : s) :
(λ (y : G), f y ^ 2) s
theorem differentiable_on.norm (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f : G E} {s : set G} (hf : s) (h0 : (x : G), x s f x 0) :
(λ (y : G), f y) s
theorem differentiable_on.dist (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] [ E] {G : Type u_4} [ G] {f g : G E} {s : set G} (hf : s) (hg : s) (hne : (x : G), x s f x g x) :
(λ (y : G), has_dist.dist (f y) (g y)) s
theorem differentiable_within_at_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [is_R_or_C 𝕜] [ H] [fintype ι] {f : H } {t : set H} {y : H} :
y (i : ι), (λ (x : H), f x i) t y
theorem differentiable_at_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [is_R_or_C 𝕜] [ H] [fintype ι] {f : H } {y : H} :
y (i : ι), (λ (x : H), f x i) y
theorem differentiable_on_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [is_R_or_C 𝕜] [ H] [fintype ι] {f : H } {t : set H} :
t (i : ι), (λ (x : H), f x i) t
theorem differentiable_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [is_R_or_C 𝕜] [ H] [fintype ι] {f : H } :
(i : ι), (λ (x : H), f x i)
theorem has_strict_fderiv_at_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [is_R_or_C 𝕜] [ H] [fintype ι] {f : H } {f' : H →L[𝕜] } {y : H} :
y (i : ι), has_strict_fderiv_at (λ (x : H), f x i) .comp f') y
theorem has_fderiv_within_at_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [is_R_or_C 𝕜] [ H] [fintype ι] {f : H } {f' : H →L[𝕜] } {t : set H} {y : H} :
t y (i : ι), has_fderiv_within_at (λ (x : H), f x i) .comp f') t y
theorem cont_diff_within_at_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [is_R_or_C 𝕜] [ H] [fintype ι] {f : H } {t : set H} {y : H} {n : ℕ∞} :
f t y (i : ι), (λ (x : H), f x i) t y
theorem cont_diff_at_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [is_R_or_C 𝕜] [ H] [fintype ι] {f : H } {y : H} {n : ℕ∞} :
n f y (i : ι), n (λ (x : H), f x i) y
theorem cont_diff_on_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [is_R_or_C 𝕜] [ H] [fintype ι] {f : H } {t : set H} {n : ℕ∞} :
n f t (i : ι), n (λ (x : H), f x i) t
theorem cont_diff_euclidean {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [is_R_or_C 𝕜] [ H] [fintype ι] {f : H } {n : ℕ∞} :
n f (i : ι), n (λ (x : H), f x i)
theorem cont_diff_homeomorph_unit_ball {n : ℕ∞} {E : Type u_1}  :
(λ (x : E),
theorem cont_diff_on_homeomorph_unit_ball_symm {n : ℕ∞} {E : Type u_1} {f : E E} (h : (y : E) (hy : y 1), f y = (homeomorph_unit_ball.symm) y, hy⟩) :
f 1)