diff --git a/src/analysis/calculus/deriv.lean b/src/analysis/calculus/deriv.lean index f98df022dd32d..42a18f0d06331 100644 --- a/src/analysis/calculus/deriv.lean +++ b/src/analysis/calculus/deriv.lean @@ -981,8 +981,7 @@ variables {fβ‚‚ : π•œ β†’ G} {fβ‚‚' : G} lemma has_deriv_at_filter.prod (hf₁ : has_deriv_at_filter f₁ f₁' x L) (hfβ‚‚ : has_deriv_at_filter fβ‚‚ fβ‚‚' x L) : has_deriv_at_filter (Ξ» x, (f₁ x, fβ‚‚ x)) (f₁', fβ‚‚') x L := -show has_fderiv_at_filter _ _ _ _, -by convert has_fderiv_at_filter.prod hf₁ hfβ‚‚ +hf₁.prod hfβ‚‚ lemma has_deriv_within_at.prod (hf₁ : has_deriv_within_at f₁ f₁' s x) (hfβ‚‚ : has_deriv_within_at fβ‚‚ fβ‚‚' s x) : @@ -993,6 +992,11 @@ lemma has_deriv_at.prod (hf₁ : has_deriv_at f₁ f₁' x) (hfβ‚‚ : has_deriv_a has_deriv_at (Ξ» x, (f₁ x, fβ‚‚ x)) (f₁', fβ‚‚') x := hf₁.prod hfβ‚‚ +lemma has_strict_deriv_at.prod (hf₁ : has_strict_deriv_at f₁ f₁' x) + (hfβ‚‚ : has_strict_deriv_at fβ‚‚ fβ‚‚' x) : + has_strict_deriv_at (Ξ» x, (f₁ x, fβ‚‚ x)) (f₁', fβ‚‚') x := +hf₁.prod hfβ‚‚ + end cartesian_product section composition @@ -1177,57 +1181,47 @@ end composition section composition_vector /-! ### Derivative of the composition of a function between vector spaces and a function on `π•œ` -/ +open continuous_linear_map + variables {l : F β†’ E} {l' : F β†’L[π•œ] E} variable (x) /-- The composition `l ∘ f` where `l : F β†’ E` and `f : π•œ β†’ F`, has a derivative within a set equal to the FrΓ©chet derivative of `l` applied to the derivative of `f`. -/ theorem has_fderiv_within_at.comp_has_deriv_within_at {t : set F} - (hl : has_fderiv_within_at l l' t (f x)) (hf : has_deriv_within_at f f' s x) (hst : s βŠ† f ⁻¹' t) : - has_deriv_within_at (l ∘ f) (l' (f')) s x := -begin - rw has_deriv_within_at_iff_has_fderiv_within_at, - convert has_fderiv_within_at.comp x hl hf hst, - ext, - simp -end + (hl : has_fderiv_within_at l l' t (f x)) (hf : has_deriv_within_at f f' s x) + (hst : maps_to f s t) : + has_deriv_within_at (l ∘ f) (l' f') s x := +by simpa only [one_apply, one_smul, smul_right_apply, coe_comp', (∘)] + using (hl.comp x hf.has_fderiv_within_at hst).has_deriv_within_at + +theorem has_fderiv_at.comp_has_deriv_within_at + (hl : has_fderiv_at l l' (f x)) (hf : has_deriv_within_at f f' s x) : + has_deriv_within_at (l ∘ f) (l' f') s x := +hl.has_fderiv_within_at.comp_has_deriv_within_at x hf (maps_to_univ _ _) /-- The composition `l ∘ f` where `l : F β†’ E` and `f : π•œ β†’ F`, has a derivative equal to the FrΓ©chet derivative of `l` applied to the derivative of `f`. -/ -theorem has_fderiv_at.comp_has_deriv_at - (hl : has_fderiv_at l l' (f x)) (hf : has_deriv_at f f' x) : - has_deriv_at (l ∘ f) (l' (f')) x := -begin - rw has_deriv_at_iff_has_fderiv_at, - convert has_fderiv_at.comp x hl hf, - ext, - simp -end +theorem has_fderiv_at.comp_has_deriv_at (hl : has_fderiv_at l l' (f x)) (hf : has_deriv_at f f' x) : + has_deriv_at (l ∘ f) (l' f') x := +has_deriv_within_at_univ.mp $ hl.comp_has_deriv_within_at x hf.has_deriv_within_at -theorem has_fderiv_at.comp_has_deriv_within_at - (hl : has_fderiv_at l l' (f x)) (hf : has_deriv_within_at f f' s x) : - has_deriv_within_at (l ∘ f) (l' (f')) s x := -begin - rw ← has_fderiv_within_at_univ at hl, - exact has_fderiv_within_at.comp_has_deriv_within_at x hl hf subset_preimage_univ -end +theorem has_strict_fderiv_at.comp_has_strict_deriv_at + (hl : has_strict_fderiv_at l l' (f x)) (hf : has_strict_deriv_at f f' x) : + has_strict_deriv_at (l ∘ f) (l' f') x := +by simpa only [one_apply, one_smul, smul_right_apply, coe_comp', (∘)] + using (hl.comp x hf.has_strict_fderiv_at).has_strict_deriv_at lemma fderiv_within.comp_deriv_within {t : set F} (hl : differentiable_within_at π•œ l t (f x)) (hf : differentiable_within_at π•œ f s x) - (hs : s βŠ† f ⁻¹' t) (hxs : unique_diff_within_at π•œ s x) : + (hs : maps_to f s t) (hxs : unique_diff_within_at π•œ s x) : deriv_within (l ∘ f) s x = (fderiv_within π•œ l t (f x) : F β†’ E) (deriv_within f s x) := -begin - apply has_deriv_within_at.deriv_within _ hxs, - exact (hl.has_fderiv_within_at).comp_has_deriv_within_at x (hf.has_deriv_within_at) hs -end +(hl.has_fderiv_within_at.comp_has_deriv_within_at x hf.has_deriv_within_at hs).deriv_within hxs lemma fderiv.comp_deriv (hl : differentiable_at π•œ l (f x)) (hf : differentiable_at π•œ f x) : deriv (l ∘ f) x = (fderiv π•œ l (f x) : F β†’ E) (deriv f x) := -begin - apply has_deriv_at.deriv _, - exact (hl.has_fderiv_at).comp_has_deriv_at x (hf.has_deriv_at) -end +(hl.has_fderiv_at.comp_has_deriv_at x hf.has_deriv_at).deriv end composition_vector diff --git a/src/analysis/calculus/fderiv.lean b/src/analysis/calculus/fderiv.lean index d7aea69808316..0c195447017da 100644 --- a/src/analysis/calculus/fderiv.lean +++ b/src/analysis/calculus/fderiv.lean @@ -1253,7 +1253,7 @@ section fst variables {fβ‚‚ : E β†’ F Γ— G} {fβ‚‚' : E β†’L[π•œ] F Γ— G} {p : E Γ— F} -lemma has_strict_fderiv_at_fst : has_strict_fderiv_at (fst π•œ E F) (fst π•œ E F) p := +lemma has_strict_fderiv_at_fst : has_strict_fderiv_at (@prod.fst E F) (fst π•œ E F) p := (fst π•œ E F).has_strict_fderiv_at protected lemma has_strict_fderiv_at.fst (h : has_strict_fderiv_at fβ‚‚ fβ‚‚' x) : @@ -1261,14 +1261,14 @@ protected lemma has_strict_fderiv_at.fst (h : has_strict_fderiv_at fβ‚‚ fβ‚‚' x) has_strict_fderiv_at_fst.comp x h lemma has_fderiv_at_filter_fst {L : filter (E Γ— F)} : - has_fderiv_at_filter (fst π•œ E F) (fst π•œ E F) p L := + has_fderiv_at_filter (@prod.fst E F) (fst π•œ E F) p L := (fst π•œ E F).has_fderiv_at_filter protected lemma has_fderiv_at_filter.fst (h : has_fderiv_at_filter fβ‚‚ fβ‚‚' x L) : has_fderiv_at_filter (Ξ» x, (fβ‚‚ x).1) ((fst π•œ F G).comp fβ‚‚') x L := has_fderiv_at_filter_fst.comp x h -lemma has_fderiv_at_fst : has_fderiv_at (fst π•œ E F) (fst π•œ E F) p := +lemma has_fderiv_at_fst : has_fderiv_at (@prod.fst E F) (fst π•œ E F) p := has_fderiv_at_filter_fst protected lemma has_fderiv_at.fst (h : has_fderiv_at fβ‚‚ fβ‚‚' x) : @@ -1276,7 +1276,7 @@ protected lemma has_fderiv_at.fst (h : has_fderiv_at fβ‚‚ fβ‚‚' x) : h.fst lemma has_fderiv_within_at_fst {s : set (E Γ— F)} : - has_fderiv_within_at (fst π•œ E F) (fst π•œ E F) s p := + has_fderiv_within_at (@prod.fst E F) (fst π•œ E F) s p := has_fderiv_at_filter_fst protected lemma has_fderiv_within_at.fst (h : has_fderiv_within_at fβ‚‚ fβ‚‚' s x) : @@ -1331,7 +1331,7 @@ section snd variables {fβ‚‚ : E β†’ F Γ— G} {fβ‚‚' : E β†’L[π•œ] F Γ— G} {p : E Γ— F} -lemma has_strict_fderiv_at_snd : has_strict_fderiv_at (snd π•œ E F) (snd π•œ E F) p := +lemma has_strict_fderiv_at_snd : has_strict_fderiv_at (@prod.snd E F) (snd π•œ E F) p := (snd π•œ E F).has_strict_fderiv_at protected lemma has_strict_fderiv_at.snd (h : has_strict_fderiv_at fβ‚‚ fβ‚‚' x) : @@ -1339,14 +1339,14 @@ protected lemma has_strict_fderiv_at.snd (h : has_strict_fderiv_at fβ‚‚ fβ‚‚' x) has_strict_fderiv_at_snd.comp x h lemma has_fderiv_at_filter_snd {L : filter (E Γ— F)} : - has_fderiv_at_filter (snd π•œ E F) (snd π•œ E F) p L := + has_fderiv_at_filter (@prod.snd E F) (snd π•œ E F) p L := (snd π•œ E F).has_fderiv_at_filter protected lemma has_fderiv_at_filter.snd (h : has_fderiv_at_filter fβ‚‚ fβ‚‚' x L) : has_fderiv_at_filter (Ξ» x, (fβ‚‚ x).2) ((snd π•œ F G).comp fβ‚‚') x L := has_fderiv_at_filter_snd.comp x h -lemma has_fderiv_at_snd : has_fderiv_at (snd π•œ E F) (snd π•œ E F) p := +lemma has_fderiv_at_snd : has_fderiv_at (@prod.snd E F) (snd π•œ E F) p := has_fderiv_at_filter_snd protected lemma has_fderiv_at.snd (h : has_fderiv_at fβ‚‚ fβ‚‚' x) : @@ -1354,7 +1354,7 @@ protected lemma has_fderiv_at.snd (h : has_fderiv_at fβ‚‚ fβ‚‚' x) : h.snd lemma has_fderiv_within_at_snd {s : set (E Γ— F)} : - has_fderiv_within_at (snd π•œ E F) (snd π•œ E F) s p := + has_fderiv_within_at (@prod.snd E F) (snd π•œ E F) s p := has_fderiv_at_filter_snd protected lemma has_fderiv_within_at.snd (h : has_fderiv_within_at fβ‚‚ fβ‚‚' s x) : @@ -1409,16 +1409,14 @@ section prod_map variables {fβ‚‚ : G β†’ G'} {fβ‚‚' : G β†’L[π•œ] G'} {y : G} (p : E Γ— G) --- TODO (Lean 3.8): use `prod.map f fβ‚‚`` - protected theorem has_strict_fderiv_at.prod_map (hf : has_strict_fderiv_at f f' p.1) (hfβ‚‚ : has_strict_fderiv_at fβ‚‚ fβ‚‚' p.2) : - has_strict_fderiv_at (Ξ» p : E Γ— G, (f p.1, fβ‚‚ p.2)) (f'.prod_map fβ‚‚') p := + has_strict_fderiv_at (prod.map f fβ‚‚) (f'.prod_map fβ‚‚') p := (hf.comp p has_strict_fderiv_at_fst).prod (hfβ‚‚.comp p has_strict_fderiv_at_snd) protected theorem has_fderiv_at.prod_map (hf : has_fderiv_at f f' p.1) (hfβ‚‚ : has_fderiv_at fβ‚‚ fβ‚‚' p.2) : - has_fderiv_at (Ξ» p : E Γ— G, (f p.1, fβ‚‚ p.2)) (f'.prod_map fβ‚‚') p := + has_fderiv_at (prod.map f fβ‚‚) (f'.prod_map fβ‚‚') p := (hf.comp p has_fderiv_at_fst).prod (hfβ‚‚.comp p has_fderiv_at_snd) @[simp] protected theorem differentiable_at.prod_map (hf : differentiable_at π•œ f p.1)