mathlib documentation

analysis.inner_product_space.calculus

Derivative of the inner product #

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] and [is_scalar_tower ℝ 𝕜 E]. In both interesting cases 𝕜 = ℝ and 𝕜 = ℂ we have these instances.

def fderiv_inner_clm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 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 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] (p x : E × E) :
theorem times_cont_diff_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {n : with_top } :
times_cont_diff n (λ (p : E × E), inner p.fst p.snd)
theorem times_cont_diff_at_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {p : E × E} {n : with_top } :
times_cont_diff_at n (λ (p : E × E), inner p.fst p.snd) p
theorem differentiable_inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] :
differentiable (λ (p : E × E), inner p.fst p.snd)
theorem times_cont_diff_within_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {s : set G} {x : G} {n : with_top } (hf : times_cont_diff_within_at n f s x) (hg : times_cont_diff_within_at n g s x) :
times_cont_diff_within_at n (λ (x : G), inner (f x) (g x)) s x
theorem times_cont_diff_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {x : G} {n : with_top } (hf : times_cont_diff_at n f x) (hg : times_cont_diff_at n g x) :
times_cont_diff_at n (λ (x : G), inner (f x) (g x)) x
theorem times_cont_diff_on.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {s : set G} {n : with_top } (hf : times_cont_diff_on n f s) (hg : times_cont_diff_on n g s) :
times_cont_diff_on n (λ (x : G), inner (f x) (g x)) s
theorem times_cont_diff.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {n : with_top } (hf : times_cont_diff n f) (hg : times_cont_diff n g) :
times_cont_diff n (λ (x : G), inner (f x) (g x))
theorem has_fderiv_within_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {f' g' : G →L[] E} {s : set G} {x : G} (hf : has_fderiv_within_at f f' s x) (hg : has_fderiv_within_at g g' s x) :
has_fderiv_within_at (λ (t : G), inner (f t) (g t)) ((fderiv_inner_clm (f x, g x)).comp (f'.prod g')) s x
theorem has_fderiv_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {f' g' : G →L[] E} {x : G} (hf : has_fderiv_at f f' x) (hg : has_fderiv_at g g' x) :
has_fderiv_at (λ (t : G), inner (f t) (g t)) ((fderiv_inner_clm (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 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {f g : → E} {f' g' : E} {s : set } {x : } (hf : has_deriv_within_at f f' s x) (hg : has_deriv_within_at g g' s x) :
has_deriv_within_at (λ (t : ), inner (f t) (g t)) (inner (f x) g' + inner f' (g x)) s x
theorem has_deriv_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {f g : → E} {f' g' : E} {x : } :
has_deriv_at f f' xhas_deriv_at g g' xhas_deriv_at (λ (t : ), inner (f t) (g t)) (inner (f x) g' + inner f' (g x)) x
theorem differentiable_within_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {s : set G} {x : G} (hf : differentiable_within_at f s x) (hg : differentiable_within_at g s x) :
differentiable_within_at (λ (x : G), inner (f x) (g x)) s x
theorem differentiable_at.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {x : G} (hf : differentiable_at f x) (hg : differentiable_at g x) :
differentiable_at (λ (x : G), inner (f x) (g x)) x
theorem differentiable_on.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {s : set G} (hf : differentiable_on f s) (hg : differentiable_on g s) :
differentiable_on (λ (x : G), inner (f x) (g x)) s
theorem differentiable.inner {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} (hf : differentiable f) (hg : differentiable g) :
differentiable (λ (x : G), inner (f x) (g x))
theorem fderiv_inner_apply {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {x : G} (hf : differentiable_at f x) (hg : differentiable_at g x) (y : G) :
(fderiv (λ (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} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {f g : → E} {x : } (hf : differentiable_at f x) (hg : differentiable_at g x) :
deriv (λ (t : ), inner (f t) (g t)) x = inner (f x) (deriv g x) + inner (deriv f x) (g x)
theorem times_cont_diff_norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {n : with_top } :
times_cont_diff n (λ (x : E), x ^ 2)
theorem times_cont_diff.norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f : G → E} {n : with_top } (hf : times_cont_diff n f) :
times_cont_diff n (λ (x : G), f x ^ 2)
theorem times_cont_diff_within_at.norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f : G → E} {s : set G} {x : G} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (y : G), f y ^ 2) s x
theorem times_cont_diff_at.norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f : G → E} {x : G} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (y : G), f y ^ 2) x
theorem times_cont_diff_at_norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {n : with_top } {x : E} (hx : x 0) :
theorem times_cont_diff_at.norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f : G → E} {x : G} {n : with_top } (hf : times_cont_diff_at n f x) (h0 : f x 0) :
times_cont_diff_at n (λ (y : G), f y) x
theorem times_cont_diff_at.dist {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {x : G} {n : with_top } (hf : times_cont_diff_at n f x) (hg : times_cont_diff_at n g x) (hne : f x g x) :
times_cont_diff_at n (λ (y : G), dist (f y) (g y)) x
theorem times_cont_diff_within_at.norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f : G → E} {s : set G} {x : G} {n : with_top } (hf : times_cont_diff_within_at n f s x) (h0 : f x 0) :
times_cont_diff_within_at n (λ (y : G), f y) s x
theorem times_cont_diff_within_at.dist {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {s : set G} {x : G} {n : with_top } (hf : times_cont_diff_within_at n f s x) (hg : times_cont_diff_within_at n g s x) (hne : f x g x) :
times_cont_diff_within_at n (λ (y : G), dist (f y) (g y)) s x
theorem times_cont_diff_on.norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f : G → E} {s : set G} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (y : G), f y ^ 2) s
theorem times_cont_diff_on.norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f : G → E} {s : set G} {n : with_top } (hf : times_cont_diff_on n f s) (h0 : ∀ (x : G), x sf x 0) :
times_cont_diff_on n (λ (y : G), f y) s
theorem times_cont_diff_on.dist {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {s : set G} {n : with_top } (hf : times_cont_diff_on n f s) (hg : times_cont_diff_on n g s) (hne : ∀ (x : G), x sf x g x) :
times_cont_diff_on n (λ (y : G), dist (f y) (g y)) s
theorem times_cont_diff.norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f : G → E} {n : with_top } (hf : times_cont_diff n f) (h0 : ∀ (x : G), f x 0) :
times_cont_diff n (λ (y : G), f y)
theorem times_cont_diff.dist {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {n : with_top } (hf : times_cont_diff n f) (hg : times_cont_diff n g) (hne : ∀ (x : G), f x g x) :
times_cont_diff n (λ (y : G), dist (f y) (g y))
theorem differentiable_at.norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f : G → E} {x : G} (hf : differentiable_at f x) :
differentiable_at (λ (y : G), f y ^ 2) x
theorem differentiable_at.norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f : G → E} {x : G} (hf : differentiable_at f x) (h0 : f x 0) :
differentiable_at (λ (y : G), f y) x
theorem differentiable_at.dist {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {x : G} (hf : differentiable_at f x) (hg : differentiable_at g x) (hne : f x g x) :
differentiable_at (λ (y : G), dist (f y) (g y)) x
theorem differentiable.norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f : G → E} (hf : differentiable f) :
differentiable (λ (y : G), f y ^ 2)
theorem differentiable.norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f : G → E} (hf : differentiable f) (h0 : ∀ (x : G), f x 0) :
differentiable (λ (y : G), f y)
theorem differentiable.dist {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} (hf : differentiable f) (hg : differentiable g) (hne : ∀ (x : G), f x g x) :
differentiable (λ (y : G), dist (f y) (g y))
theorem differentiable_within_at.norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f : G → E} {s : set G} {x : G} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (y : G), f y ^ 2) s x
theorem differentiable_within_at.norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f : G → E} {s : set G} {x : G} (hf : differentiable_within_at f s x) (h0 : f x 0) :
differentiable_within_at (λ (y : G), f y) s x
theorem differentiable_within_at.dist {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {s : set G} {x : G} (hf : differentiable_within_at f s x) (hg : differentiable_within_at g s x) (hne : f x g x) :
differentiable_within_at (λ (y : G), dist (f y) (g y)) s x
theorem differentiable_on.norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f : G → E} {s : set G} (hf : differentiable_on f s) :
differentiable_on (λ (y : G), f y ^ 2) s
theorem differentiable_on.norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f : G → E} {s : set G} (hf : differentiable_on f s) (h0 : ∀ (x : G), x sf x 0) :
differentiable_on (λ (y : G), f y) s
theorem differentiable_on.dist {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [normed_space E] [is_scalar_tower 𝕜 E] {G : Type u_4} [normed_group G] [normed_space G] {f g : G → E} {s : set G} (hf : differentiable_on f s) (hg : differentiable_on g s) (hne : ∀ (x : G), x sf x g x) :
differentiable_on (λ (y : G), dist (f y) (g y)) s