mathlib3 documentation

analysis.calculus.fderiv.prod

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) :
fderiv 𝕜 (λ (x : E), (f₁ x, f₂ x)) x = (fderiv 𝕜 f₁ x).prod (fderiv 𝕜 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)
@[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)} :
@[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
@[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)} :
@[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
@[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} :
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) :
fderiv 𝕜 (λ (x : E), (f₂ x).fst) x = (continuous_linear_map.fst 𝕜 F G).comp (fderiv 𝕜 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) :
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)
@[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)} :
@[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
@[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)} :
@[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
@[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} :
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) :
fderiv 𝕜 (λ (x : E), (f₂ x).snd) x = (continuous_linear_map.snd 𝕜 F G).comp (fderiv 𝕜 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) :
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:

@[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)