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 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 𝕜]
[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 : ℕ∞} :
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 : ℕ∞} :
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_add_comm_group G]
[normed_space ℝ G]
{f g : G → E}
{s : set G}
{x : G}
{n : ℕ∞}
(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_add_comm_group G]
[normed_space ℝ G]
{f g : G → E}
{x : G}
{n : ℕ∞}
(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_add_comm_group G]
[normed_space ℝ G]
{f g : G → E}
{s : set G}
{n : ℕ∞}
(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_add_comm_group G]
[normed_space ℝ G]
{f g : G → E}
{n : ℕ∞}
(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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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 : ℕ∞} :
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_add_comm_group G]
[normed_space ℝ G]
{f : G → E}
{n : ℕ∞}
(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_add_comm_group G]
[normed_space ℝ G]
{f : G → E}
{s : set G}
{x : G}
{n : ℕ∞}
(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_add_comm_group G]
[normed_space ℝ G]
{f : G → E}
{x : G}
{n : ℕ∞}
(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 : ℕ∞}
{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_add_comm_group G]
[normed_space ℝ G]
{f : G → E}
{x : G}
{n : ℕ∞}
(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_add_comm_group G]
[normed_space ℝ G]
{f g : G → E}
{x : G}
{n : ℕ∞}
(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_add_comm_group G]
[normed_space ℝ G]
{f : G → E}
{s : set G}
{x : G}
{n : ℕ∞}
(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_add_comm_group G]
[normed_space ℝ G]
{f g : G → E}
{s : set G}
{x : G}
{n : ℕ∞}
(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_add_comm_group G]
[normed_space ℝ G]
{f : G → E}
{s : set G}
{n : ℕ∞}
(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_add_comm_group G]
[normed_space ℝ G]
{f : G → E}
{s : set G}
{n : ℕ∞}
(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_add_comm_group G]
[normed_space ℝ G]
{f g : G → E}
{s : set G}
{n : ℕ∞}
(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_add_comm_group G]
[normed_space ℝ G]
{f : G → E}
{n : ℕ∞}
(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_add_comm_group G]
[normed_space ℝ G]
{f g : G → E}
{n : ℕ∞}
(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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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
theorem
differentiable_within_at_euclidean
{𝕜 : Type u_1}
{ι : Type u_2}
{H : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group H]
[normed_space 𝕜 H]
[fintype ι]
{f : H → euclidean_space 𝕜 ι}
{t : set H}
{y : H} :
differentiable_within_at 𝕜 f t y ↔ ∀ (i : ι), differentiable_within_at 𝕜 (λ (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 𝕜]
[normed_add_comm_group H]
[normed_space 𝕜 H]
[fintype ι]
{f : H → euclidean_space 𝕜 ι}
{y : H} :
differentiable_at 𝕜 f y ↔ ∀ (i : ι), differentiable_at 𝕜 (λ (x : H), f x i) y
theorem
differentiable_on_euclidean
{𝕜 : Type u_1}
{ι : Type u_2}
{H : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group H]
[normed_space 𝕜 H]
[fintype ι]
{f : H → euclidean_space 𝕜 ι}
{t : set H} :
differentiable_on 𝕜 f t ↔ ∀ (i : ι), differentiable_on 𝕜 (λ (x : H), f x i) t
theorem
differentiable_euclidean
{𝕜 : Type u_1}
{ι : Type u_2}
{H : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group H]
[normed_space 𝕜 H]
[fintype ι]
{f : H → euclidean_space 𝕜 ι} :
differentiable 𝕜 f ↔ ∀ (i : ι), differentiable 𝕜 (λ (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 𝕜]
[normed_add_comm_group H]
[normed_space 𝕜 H]
[fintype ι]
{f : H → euclidean_space 𝕜 ι}
{f' : H →L[𝕜] euclidean_space 𝕜 ι}
{y : H} :
has_strict_fderiv_at f f' y ↔ ∀ (i : ι), has_strict_fderiv_at (λ (x : H), f x i) ((euclidean_space.proj i).comp f') y
theorem
has_fderiv_within_at_euclidean
{𝕜 : Type u_1}
{ι : Type u_2}
{H : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group H]
[normed_space 𝕜 H]
[fintype ι]
{f : H → euclidean_space 𝕜 ι}
{f' : H →L[𝕜] euclidean_space 𝕜 ι}
{t : set H}
{y : H} :
has_fderiv_within_at f f' t y ↔ ∀ (i : ι), has_fderiv_within_at (λ (x : H), f x i) ((euclidean_space.proj 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 𝕜]
[normed_add_comm_group H]
[normed_space 𝕜 H]
[fintype ι]
{f : H → euclidean_space 𝕜 ι}
{t : set H}
{y : H}
{n : ℕ∞} :
cont_diff_within_at 𝕜 n f t y ↔ ∀ (i : ι), cont_diff_within_at 𝕜 n (λ (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 𝕜]
[normed_add_comm_group H]
[normed_space 𝕜 H]
[fintype ι]
{f : H → euclidean_space 𝕜 ι}
{y : H}
{n : ℕ∞} :
cont_diff_at 𝕜 n f y ↔ ∀ (i : ι), cont_diff_at 𝕜 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 𝕜]
[normed_add_comm_group H]
[normed_space 𝕜 H]
[fintype ι]
{f : H → euclidean_space 𝕜 ι}
{t : set H}
{n : ℕ∞} :
cont_diff_on 𝕜 n f t ↔ ∀ (i : ι), cont_diff_on 𝕜 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 𝕜]
[normed_add_comm_group H]
[normed_space 𝕜 H]
[fintype ι]
{f : H → euclidean_space 𝕜 ι}
{n : ℕ∞} :
theorem
cont_diff_homeomorph_unit_ball
{n : ℕ∞}
{E : Type u_1}
[inner_product_space ℝ E] :
cont_diff ℝ n (λ (x : E), ↑(⇑homeomorph_unit_ball x))
theorem
cont_diff_on_homeomorph_unit_ball_symm
{n : ℕ∞}
{E : Type u_1}
[inner_product_space ℝ E]
{f : E → E}
(h : ∀ (y : E) (hy : y ∈ metric.ball 0 1), f y = ⇑(homeomorph_unit_ball.symm) ⟨y, hy⟩) :
cont_diff_on ℝ n f (metric.ball 0 1)