Derivative of the cartesian product of functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
For detailed documentation of the Fréchet derivative,
see the module docstring of analysis/calculus/fderiv/basic.lean.
This file contains the usual formulas (and existence assertions) for the derivative of cartesian products of functions, and functions into Pi-types.
Derivative of the cartesian product of two functions #
@[protected]
theorem
has_strict_fderiv_at.prod
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f₁ : E → F}
{f₁' : E →L[𝕜] F}
{x : E}
{f₂ : E → G}
{f₂' : E →L[𝕜] G}
(hf₁ : has_strict_fderiv_at f₁ f₁' x)
(hf₂ : has_strict_fderiv_at f₂ f₂' x) :
has_strict_fderiv_at (λ (x : E), (f₁ x, f₂ x)) (f₁'.prod f₂') x
theorem
has_fderiv_at_filter.prod
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f₁ : E → F}
{f₁' : E →L[𝕜] F}
{x : E}
{L : filter E}
{f₂ : E → G}
{f₂' : E →L[𝕜] G}
(hf₁ : has_fderiv_at_filter f₁ f₁' x L)
(hf₂ : has_fderiv_at_filter f₂ f₂' x L) :
has_fderiv_at_filter (λ (x : E), (f₁ x, f₂ x)) (f₁'.prod f₂') x L
theorem
has_fderiv_within_at.prod
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f₁ : E → F}
{f₁' : E →L[𝕜] F}
{x : E}
{s : set E}
{f₂ : E → G}
{f₂' : E →L[𝕜] G}
(hf₁ : has_fderiv_within_at f₁ f₁' s x)
(hf₂ : has_fderiv_within_at f₂ f₂' s x) :
has_fderiv_within_at (λ (x : E), (f₁ x, f₂ x)) (f₁'.prod f₂') s x
theorem
has_fderiv_at.prod
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f₁ : E → F}
{f₁' : E →L[𝕜] F}
{x : E}
{f₂ : E → G}
{f₂' : E →L[𝕜] G}
(hf₁ : has_fderiv_at f₁ f₁' x)
(hf₂ : has_fderiv_at f₂ f₂' x) :
has_fderiv_at (λ (x : E), (f₁ x, f₂ x)) (f₁'.prod f₂') x
theorem
has_fderiv_at_prod_mk_left
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(e₀ : E)
(f₀ : F) :
has_fderiv_at (λ (e : E), (e, f₀)) (continuous_linear_map.inl 𝕜 E F) e₀
theorem
has_fderiv_at_prod_mk_right
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(e₀ : E)
(f₀ : F) :
has_fderiv_at (λ (f : F), (e₀, f)) (continuous_linear_map.inr 𝕜 E F) f₀
theorem
differentiable_within_at.prod
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f₁ : E → F}
{x : E}
{s : set E}
{f₂ : E → G}
(hf₁ : differentiable_within_at 𝕜 f₁ s x)
(hf₂ : differentiable_within_at 𝕜 f₂ s x) :
differentiable_within_at 𝕜 (λ (x : E), (f₁ x, f₂ x)) s x
@[simp]
theorem
differentiable_at.prod
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f₁ : E → F}
{x : E}
{f₂ : E → G}
(hf₁ : differentiable_at 𝕜 f₁ x)
(hf₂ : differentiable_at 𝕜 f₂ x) :
differentiable_at 𝕜 (λ (x : E), (f₁ x, f₂ x)) x
theorem
differentiable_on.prod
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f₁ : E → F}
{s : set E}
{f₂ : E → G}
(hf₁ : differentiable_on 𝕜 f₁ s)
(hf₂ : differentiable_on 𝕜 f₂ s) :
differentiable_on 𝕜 (λ (x : E), (f₁ x, f₂ x)) s
@[simp]
theorem
differentiable.prod
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f₁ : E → F}
{f₂ : E → G}
(hf₁ : differentiable 𝕜 f₁)
(hf₂ : differentiable 𝕜 f₂) :
differentiable 𝕜 (λ (x : E), (f₁ x, f₂ x))
theorem
differentiable_at.fderiv_prod
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f₁ : E → F}
{x : E}
{f₂ : E → G}
(hf₁ : differentiable_at 𝕜 f₁ x)
(hf₂ : differentiable_at 𝕜 f₂ x) :
theorem
differentiable_within_at.fderiv_within_prod
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f₁ : E → F}
{x : E}
{s : set E}
{f₂ : E → G}
(hf₁ : differentiable_within_at 𝕜 f₁ s x)
(hf₂ : differentiable_within_at 𝕜 f₂ s x)
(hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (λ (x : E), (f₁ x, f₂ x)) s x = (fderiv_within 𝕜 f₁ s x).prod (fderiv_within 𝕜 f₂ s x)
theorem
has_strict_fderiv_at_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{p : E × F} :
@[protected]
theorem
has_strict_fderiv_at.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{f₂ : E → F × G}
{f₂' : E →L[𝕜] F × G}
(h : has_strict_fderiv_at f₂ f₂' x) :
has_strict_fderiv_at (λ (x : E), (f₂ x).fst) ((continuous_linear_map.fst 𝕜 F G).comp f₂') x
theorem
has_fderiv_at_filter_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{p : E × F}
{L : filter (E × F)} :
has_fderiv_at_filter prod.fst (continuous_linear_map.fst 𝕜 E F) p L
@[protected]
theorem
has_fderiv_at_filter.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{L : filter E}
{f₂ : E → F × G}
{f₂' : E →L[𝕜] F × G}
(h : has_fderiv_at_filter f₂ f₂' x L) :
has_fderiv_at_filter (λ (x : E), (f₂ x).fst) ((continuous_linear_map.fst 𝕜 F G).comp f₂') x L
theorem
has_fderiv_at_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{p : E × F} :
has_fderiv_at prod.fst (continuous_linear_map.fst 𝕜 E F) p
@[protected]
theorem
has_fderiv_at.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{f₂ : E → F × G}
{f₂' : E →L[𝕜] F × G}
(h : has_fderiv_at f₂ f₂' x) :
has_fderiv_at (λ (x : E), (f₂ x).fst) ((continuous_linear_map.fst 𝕜 F G).comp f₂') x
theorem
has_fderiv_within_at_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{p : E × F}
{s : set (E × F)} :
has_fderiv_within_at prod.fst (continuous_linear_map.fst 𝕜 E F) s p
@[protected]
theorem
has_fderiv_within_at.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{s : set E}
{f₂ : E → F × G}
{f₂' : E →L[𝕜] F × G}
(h : has_fderiv_within_at f₂ f₂' s x) :
has_fderiv_within_at (λ (x : E), (f₂ x).fst) ((continuous_linear_map.fst 𝕜 F G).comp f₂') s x
theorem
differentiable_at_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{p : E × F} :
@[protected, simp]
theorem
differentiable_at.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{f₂ : E → F × G}
(h : differentiable_at 𝕜 f₂ x) :
differentiable_at 𝕜 (λ (x : E), (f₂ x).fst) x
theorem
differentiable_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F] :
@[protected, simp]
theorem
differentiable.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f₂ : E → F × G}
(h : differentiable 𝕜 f₂) :
differentiable 𝕜 (λ (x : E), (f₂ x).fst)
theorem
differentiable_within_at_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{p : E × F}
{s : set (E × F)} :
@[protected]
theorem
differentiable_within_at.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{s : set E}
{f₂ : E → F × G}
(h : differentiable_within_at 𝕜 f₂ s x) :
differentiable_within_at 𝕜 (λ (x : E), (f₂ x).fst) s x
theorem
differentiable_on_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{s : set (E × F)} :
@[protected]
theorem
differentiable_on.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{s : set E}
{f₂ : E → F × G}
(h : differentiable_on 𝕜 f₂ s) :
differentiable_on 𝕜 (λ (x : E), (f₂ x).fst) s
theorem
fderiv_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{p : E × F} :
fderiv 𝕜 prod.fst p = continuous_linear_map.fst 𝕜 E F
theorem
fderiv.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{f₂ : E → F × G}
(h : differentiable_at 𝕜 f₂ x) :
theorem
fderiv_within_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{p : E × F}
{s : set (E × F)}
(hs : unique_diff_within_at 𝕜 s p) :
fderiv_within 𝕜 prod.fst s p = continuous_linear_map.fst 𝕜 E F
theorem
fderiv_within.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{s : set E}
{f₂ : E → F × G}
(hs : unique_diff_within_at 𝕜 s x)
(h : differentiable_within_at 𝕜 f₂ s x) :
fderiv_within 𝕜 (λ (x : E), (f₂ x).fst) s x = (continuous_linear_map.fst 𝕜 F G).comp (fderiv_within 𝕜 f₂ s x)
theorem
has_strict_fderiv_at_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{p : E × F} :
@[protected]
theorem
has_strict_fderiv_at.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{f₂ : E → F × G}
{f₂' : E →L[𝕜] F × G}
(h : has_strict_fderiv_at f₂ f₂' x) :
has_strict_fderiv_at (λ (x : E), (f₂ x).snd) ((continuous_linear_map.snd 𝕜 F G).comp f₂') x
theorem
has_fderiv_at_filter_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{p : E × F}
{L : filter (E × F)} :
has_fderiv_at_filter prod.snd (continuous_linear_map.snd 𝕜 E F) p L
@[protected]
theorem
has_fderiv_at_filter.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{L : filter E}
{f₂ : E → F × G}
{f₂' : E →L[𝕜] F × G}
(h : has_fderiv_at_filter f₂ f₂' x L) :
has_fderiv_at_filter (λ (x : E), (f₂ x).snd) ((continuous_linear_map.snd 𝕜 F G).comp f₂') x L
theorem
has_fderiv_at_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{p : E × F} :
has_fderiv_at prod.snd (continuous_linear_map.snd 𝕜 E F) p
@[protected]
theorem
has_fderiv_at.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{f₂ : E → F × G}
{f₂' : E →L[𝕜] F × G}
(h : has_fderiv_at f₂ f₂' x) :
has_fderiv_at (λ (x : E), (f₂ x).snd) ((continuous_linear_map.snd 𝕜 F G).comp f₂') x
theorem
has_fderiv_within_at_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{p : E × F}
{s : set (E × F)} :
has_fderiv_within_at prod.snd (continuous_linear_map.snd 𝕜 E F) s p
@[protected]
theorem
has_fderiv_within_at.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{s : set E}
{f₂ : E → F × G}
{f₂' : E →L[𝕜] F × G}
(h : has_fderiv_within_at f₂ f₂' s x) :
has_fderiv_within_at (λ (x : E), (f₂ x).snd) ((continuous_linear_map.snd 𝕜 F G).comp f₂') s x
theorem
differentiable_at_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{p : E × F} :
@[protected, simp]
theorem
differentiable_at.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{f₂ : E → F × G}
(h : differentiable_at 𝕜 f₂ x) :
differentiable_at 𝕜 (λ (x : E), (f₂ x).snd) x
theorem
differentiable_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F] :
@[protected, simp]
theorem
differentiable.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f₂ : E → F × G}
(h : differentiable 𝕜 f₂) :
differentiable 𝕜 (λ (x : E), (f₂ x).snd)
theorem
differentiable_within_at_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{p : E × F}
{s : set (E × F)} :
@[protected]
theorem
differentiable_within_at.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{s : set E}
{f₂ : E → F × G}
(h : differentiable_within_at 𝕜 f₂ s x) :
differentiable_within_at 𝕜 (λ (x : E), (f₂ x).snd) s x
theorem
differentiable_on_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{s : set (E × F)} :
@[protected]
theorem
differentiable_on.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{s : set E}
{f₂ : E → F × G}
(h : differentiable_on 𝕜 f₂ s) :
differentiable_on 𝕜 (λ (x : E), (f₂ x).snd) s
theorem
fderiv_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{p : E × F} :
fderiv 𝕜 prod.snd p = continuous_linear_map.snd 𝕜 E F
theorem
fderiv.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{f₂ : E → F × G}
(h : differentiable_at 𝕜 f₂ x) :
theorem
fderiv_within_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{p : E × F}
{s : set (E × F)}
(hs : unique_diff_within_at 𝕜 s p) :
fderiv_within 𝕜 prod.snd s p = continuous_linear_map.snd 𝕜 E F
theorem
fderiv_within.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{x : E}
{s : set E}
{f₂ : E → F × G}
(hs : unique_diff_within_at 𝕜 s x)
(h : differentiable_within_at 𝕜 f₂ s x) :
fderiv_within 𝕜 (λ (x : E), (f₂ x).snd) s x = (continuous_linear_map.snd 𝕜 F G).comp (fderiv_within 𝕜 f₂ s x)
@[protected]
theorem
has_strict_fderiv_at.prod_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{G' : Type u_5}
[normed_add_comm_group G']
[normed_space 𝕜 G']
{f : E → F}
{f' : E →L[𝕜] F}
{f₂ : G → G'}
{f₂' : G →L[𝕜] G'}
(p : E × G)
(hf : has_strict_fderiv_at f f' p.fst)
(hf₂ : has_strict_fderiv_at f₂ f₂' p.snd) :
has_strict_fderiv_at (prod.map f f₂) (f'.prod_map f₂') p
@[protected]
theorem
has_fderiv_at.prod_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{G' : Type u_5}
[normed_add_comm_group G']
[normed_space 𝕜 G']
{f : E → F}
{f' : E →L[𝕜] F}
{f₂ : G → G'}
{f₂' : G →L[𝕜] G'}
(p : E × G)
(hf : has_fderiv_at f f' p.fst)
(hf₂ : has_fderiv_at f₂ f₂' p.snd) :
has_fderiv_at (prod.map f f₂) (f'.prod_map f₂') p
@[protected, simp]
theorem
differentiable_at.prod_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{G' : Type u_5}
[normed_add_comm_group G']
[normed_space 𝕜 G']
{f : E → F}
{f₂ : G → G'}
(p : E × G)
(hf : differentiable_at 𝕜 f p.fst)
(hf₂ : differentiable_at 𝕜 f₂ p.snd) :
differentiable_at 𝕜 (λ (p : E × G), (f p.fst, f₂ p.snd)) p
Derivatives of functions f : E → Π i, F' i #
In this section we formulate has_*fderiv*_pi theorems as iffs, and provide two versions of each
theorem:
- the version without
'deals withφ : Π i, E → F' iandφ' : Π i, E →L[𝕜] F' iand is designed to deduce differentiability ofλ x i, φ i xfrom differentiability of eachφ i; - the version with
'deals withΦ : E → Π i, F' iandΦ' : E →L[𝕜] Π i, F' iand is designed to deduce differentiability of the componentsλ x, Φ x ifrom differentiability ofΦ.
@[simp]
theorem
has_strict_fderiv_at_pi'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{ι : Type u_6}
[fintype ι]
{F' : ι → Type u_7}
[Π (i : ι), normed_add_comm_group (F' i)]
[Π (i : ι), normed_space 𝕜 (F' i)]
{Φ : E → Π (i : ι), F' i}
{Φ' : E →L[𝕜] Π (i : ι), F' i} :
has_strict_fderiv_at Φ Φ' x ↔ ∀ (i : ι), has_strict_fderiv_at (λ (x : E), Φ x i) ((continuous_linear_map.proj i).comp Φ') x
@[simp]
theorem
has_strict_fderiv_at_pi
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{ι : Type u_6}
[fintype ι]
{F' : ι → Type u_7}
[Π (i : ι), normed_add_comm_group (F' i)]
[Π (i : ι), normed_space 𝕜 (F' i)]
{φ : Π (i : ι), E → F' i}
{φ' : Π (i : ι), E →L[𝕜] F' i} :
has_strict_fderiv_at (λ (x : E) (i : ι), φ i x) (continuous_linear_map.pi φ') x ↔ ∀ (i : ι), has_strict_fderiv_at (φ i) (φ' i) x
@[simp]
theorem
has_fderiv_at_filter_pi'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{L : filter E}
{ι : Type u_6}
[fintype ι]
{F' : ι → Type u_7}
[Π (i : ι), normed_add_comm_group (F' i)]
[Π (i : ι), normed_space 𝕜 (F' i)]
{Φ : E → Π (i : ι), F' i}
{Φ' : E →L[𝕜] Π (i : ι), F' i} :
has_fderiv_at_filter Φ Φ' x L ↔ ∀ (i : ι), has_fderiv_at_filter (λ (x : E), Φ x i) ((continuous_linear_map.proj i).comp Φ') x L
theorem
has_fderiv_at_filter_pi
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{L : filter E}
{ι : Type u_6}
[fintype ι]
{F' : ι → Type u_7}
[Π (i : ι), normed_add_comm_group (F' i)]
[Π (i : ι), normed_space 𝕜 (F' i)]
{φ : Π (i : ι), E → F' i}
{φ' : Π (i : ι), E →L[𝕜] F' i} :
has_fderiv_at_filter (λ (x : E) (i : ι), φ i x) (continuous_linear_map.pi φ') x L ↔ ∀ (i : ι), has_fderiv_at_filter (φ i) (φ' i) x L
@[simp]
theorem
has_fderiv_at_pi'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{ι : Type u_6}
[fintype ι]
{F' : ι → Type u_7}
[Π (i : ι), normed_add_comm_group (F' i)]
[Π (i : ι), normed_space 𝕜 (F' i)]
{Φ : E → Π (i : ι), F' i}
{Φ' : E →L[𝕜] Π (i : ι), F' i} :
has_fderiv_at Φ Φ' x ↔ ∀ (i : ι), has_fderiv_at (λ (x : E), Φ x i) ((continuous_linear_map.proj i).comp Φ') x
theorem
has_fderiv_at_pi
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{ι : Type u_6}
[fintype ι]
{F' : ι → Type u_7}
[Π (i : ι), normed_add_comm_group (F' i)]
[Π (i : ι), normed_space 𝕜 (F' i)]
{φ : Π (i : ι), E → F' i}
{φ' : Π (i : ι), E →L[𝕜] F' i} :
has_fderiv_at (λ (x : E) (i : ι), φ i x) (continuous_linear_map.pi φ') x ↔ ∀ (i : ι), has_fderiv_at (φ i) (φ' i) x
@[simp]
theorem
has_fderiv_within_at_pi'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{ι : Type u_6}
[fintype ι]
{F' : ι → Type u_7}
[Π (i : ι), normed_add_comm_group (F' i)]
[Π (i : ι), normed_space 𝕜 (F' i)]
{Φ : E → Π (i : ι), F' i}
{Φ' : E →L[𝕜] Π (i : ι), F' i} :
has_fderiv_within_at Φ Φ' s x ↔ ∀ (i : ι), has_fderiv_within_at (λ (x : E), Φ x i) ((continuous_linear_map.proj i).comp Φ') s x
theorem
has_fderiv_within_at_pi
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{ι : Type u_6}
[fintype ι]
{F' : ι → Type u_7}
[Π (i : ι), normed_add_comm_group (F' i)]
[Π (i : ι), normed_space 𝕜 (F' i)]
{φ : Π (i : ι), E → F' i}
{φ' : Π (i : ι), E →L[𝕜] F' i} :
has_fderiv_within_at (λ (x : E) (i : ι), φ i x) (continuous_linear_map.pi φ') s x ↔ ∀ (i : ι), has_fderiv_within_at (φ i) (φ' i) s x
@[simp]
theorem
differentiable_within_at_pi
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{ι : Type u_6}
[fintype ι]
{F' : ι → Type u_7}
[Π (i : ι), normed_add_comm_group (F' i)]
[Π (i : ι), normed_space 𝕜 (F' i)]
{Φ : E → Π (i : ι), F' i} :
differentiable_within_at 𝕜 Φ s x ↔ ∀ (i : ι), differentiable_within_at 𝕜 (λ (x : E), Φ x i) s x
@[simp]
theorem
differentiable_at_pi
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{ι : Type u_6}
[fintype ι]
{F' : ι → Type u_7}
[Π (i : ι), normed_add_comm_group (F' i)]
[Π (i : ι), normed_space 𝕜 (F' i)]
{Φ : E → Π (i : ι), F' i} :
differentiable_at 𝕜 Φ x ↔ ∀ (i : ι), differentiable_at 𝕜 (λ (x : E), Φ x i) x
theorem
differentiable_on_pi
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{s : set E}
{ι : Type u_6}
[fintype ι]
{F' : ι → Type u_7}
[Π (i : ι), normed_add_comm_group (F' i)]
[Π (i : ι), normed_space 𝕜 (F' i)]
{Φ : E → Π (i : ι), F' i} :
differentiable_on 𝕜 Φ s ↔ ∀ (i : ι), differentiable_on 𝕜 (λ (x : E), Φ x i) s
theorem
differentiable_pi
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{ι : Type u_6}
[fintype ι]
{F' : ι → Type u_7}
[Π (i : ι), normed_add_comm_group (F' i)]
[Π (i : ι), normed_space 𝕜 (F' i)]
{Φ : E → Π (i : ι), F' i} :
differentiable 𝕜 Φ ↔ ∀ (i : ι), differentiable 𝕜 (λ (x : E), Φ x i)
theorem
fderiv_within_pi
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{ι : Type u_6}
[fintype ι]
{F' : ι → Type u_7}
[Π (i : ι), normed_add_comm_group (F' i)]
[Π (i : ι), normed_space 𝕜 (F' i)]
{φ : Π (i : ι), E → F' i}
(h : ∀ (i : ι), differentiable_within_at 𝕜 (φ i) s x)
(hs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (λ (x : E) (i : ι), φ i x) s x = continuous_linear_map.pi (λ (i : ι), fderiv_within 𝕜 (φ i) s x)
theorem
fderiv_pi
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{ι : Type u_6}
[fintype ι]
{F' : ι → Type u_7}
[Π (i : ι), normed_add_comm_group (F' i)]
[Π (i : ι), normed_space 𝕜 (F' i)]
{φ : Π (i : ι), E → F' i}
(h : ∀ (i : ι), differentiable_at 𝕜 (φ i) x) :
fderiv 𝕜 (λ (x : E) (i : ι), φ i x) x = continuous_linear_map.pi (λ (i : ι), fderiv 𝕜 (φ i) x)