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].
noncomputable
def
fderiv_inner_clm
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
(p : E × E) :
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]
(p x : E × E) :
⇑(fderiv_inner_clm p) x = has_inner.inner p.fst x.snd + has_inner.inner x.fst p.snd
theorem
cont_diff_inner
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{n : with_top ℕ} :
theorem
cont_diff_at_inner
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{p : E × E}
{n : with_top ℕ} :
cont_diff_at ℝ n (λ (p : E × E), has_inner.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] :
differentiable ℝ (λ (p : E × E), has_inner.inner p.fst p.snd)
theorem
cont_diff_within_at.inner
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f g : G → E}
{s : set G}
{x : G}
{n : with_top ℕ}
(hf : cont_diff_within_at ℝ n f s x)
(hg : cont_diff_within_at ℝ n g s x) :
cont_diff_within_at ℝ n (λ (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 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f g : G → E}
{x : G}
{n : with_top ℕ}
(hf : cont_diff_at ℝ n f x)
(hg : cont_diff_at ℝ n g x) :
cont_diff_at ℝ n (λ (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 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f g : G → E}
{s : set G}
{n : with_top ℕ}
(hf : cont_diff_on ℝ n f s)
(hg : cont_diff_on ℝ n g s) :
cont_diff_on ℝ n (λ (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 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f g : G → E}
{n : with_top ℕ}
(hf : cont_diff ℝ n f)
(hg : cont_diff ℝ n g) :
cont_diff ℝ n (λ (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 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ 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), has_inner.inner (f t) (g t)) ((fderiv_inner_clm (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 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f g : G → E}
{f' g' : G →L[ℝ] E}
{x : G}
(hf : has_strict_fderiv_at f f' x)
(hg : has_strict_fderiv_at g g' x) :
has_strict_fderiv_at (λ (t : G), has_inner.inner (f t) (g t)) ((fderiv_inner_clm (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 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ 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), has_inner.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]
{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 : ℝ), has_inner.inner (f t) (g t)) (has_inner.inner (f x) g' + has_inner.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]
{f g : ℝ → E}
{f' g' : E}
{x : ℝ} :
has_deriv_at f f' x → has_deriv_at g g' x → has_deriv_at (λ (t : ℝ), has_inner.inner (f t) (g t)) (has_inner.inner (f x) g' + has_inner.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]
{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), has_inner.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]
{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), has_inner.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]
{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), has_inner.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]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f g : G → E}
(hf : differentiable ℝ f)
(hg : differentiable ℝ g) :
differentiable ℝ (λ (x : G), has_inner.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]
{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), has_inner.inner (f t) (g t)) x) y = has_inner.inner (f x) (⇑(fderiv ℝ g x) y) + has_inner.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]
{f g : ℝ → E}
{x : ℝ}
(hf : differentiable_at ℝ f x)
(hg : differentiable_at ℝ g 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 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{n : with_top ℕ} :
theorem
cont_diff.norm_sq
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f : G → E}
{n : with_top ℕ}
(hf : cont_diff ℝ n f) :
theorem
cont_diff_within_at.norm_sq
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f : G → E}
{s : set G}
{x : G}
{n : with_top ℕ}
(hf : cont_diff_within_at ℝ n f s x) :
cont_diff_within_at ℝ n (λ (y : G), ∥f y∥ ^ 2) s x
theorem
cont_diff_at.norm_sq
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f : G → E}
{x : G}
{n : with_top ℕ}
(hf : cont_diff_at ℝ n f x) :
cont_diff_at ℝ n (λ (y : G), ∥f y∥ ^ 2) x
theorem
cont_diff_at_norm
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{n : with_top ℕ}
{x : E}
(hx : x ≠ 0) :
theorem
cont_diff_at.norm
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f : G → E}
{x : G}
{n : with_top ℕ}
(hf : cont_diff_at ℝ n f x)
(h0 : f x ≠ 0) :
cont_diff_at ℝ n (λ (y : G), ∥f y∥) x
theorem
cont_diff_at.dist
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f g : G → E}
{x : G}
{n : with_top ℕ}
(hf : cont_diff_at ℝ n f x)
(hg : cont_diff_at ℝ n g x)
(hne : f x ≠ g x) :
cont_diff_at ℝ n (λ (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 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f : G → E}
{s : set G}
{x : G}
{n : with_top ℕ}
(hf : cont_diff_within_at ℝ n f s x)
(h0 : f x ≠ 0) :
cont_diff_within_at ℝ n (λ (y : G), ∥f y∥) s x
theorem
cont_diff_within_at.dist
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f g : G → E}
{s : set G}
{x : G}
{n : with_top ℕ}
(hf : cont_diff_within_at ℝ n f s x)
(hg : cont_diff_within_at ℝ n g s x)
(hne : f x ≠ g x) :
cont_diff_within_at ℝ n (λ (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 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f : G → E}
{s : set G}
{n : with_top ℕ}
(hf : cont_diff_on ℝ n f s) :
cont_diff_on ℝ n (λ (y : G), ∥f y∥ ^ 2) s
theorem
cont_diff_on.norm
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f : G → E}
{s : set G}
{n : with_top ℕ}
(hf : cont_diff_on ℝ n f s)
(h0 : ∀ (x : G), x ∈ s → f x ≠ 0) :
cont_diff_on ℝ n (λ (y : G), ∥f y∥) s
theorem
cont_diff_on.dist
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f g : G → E}
{s : set G}
{n : with_top ℕ}
(hf : cont_diff_on ℝ n f s)
(hg : cont_diff_on ℝ n g s)
(hne : ∀ (x : G), x ∈ s → f x ≠ g x) :
cont_diff_on ℝ n (λ (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 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f : G → E}
{n : with_top ℕ}
(hf : cont_diff ℝ n f)
(h0 : ∀ (x : G), f x ≠ 0) :
theorem
cont_diff.dist
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ E]
{G : Type u_4}
[normed_group G]
[normed_space ℝ G]
{f g : G → E}
{n : with_top ℕ}
(hf : cont_diff ℝ n f)
(hg : cont_diff ℝ n g)
(hne : ∀ (x : G), f x ≠ g x) :
cont_diff ℝ n (λ (y : G), has_dist.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]
{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]
{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]
{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), has_dist.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]
{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]
{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]
{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), has_dist.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]
{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]
{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]
{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), 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 𝕜]
[inner_product_space 𝕜 E]
[normed_space ℝ 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]
{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 ∈ s → f 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]
{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 ∈ s → f x ≠ g x) :
differentiable_on ℝ (λ (y : G), has_dist.dist (f y) (g y)) s