feat(geometry/manifold/mfderiv): more arithmetic (#17793)

fpvandoorn · fpvandoorn · commit f93c11933efb · 2023-01-25T19:38:11.000Z
* generalize most arithmetic from normed algebra to normed space
* add some arithmetic with `mfderiv`
* redefine `mfderiv` (and variants) to use `if` instead of dependent `if`.
diff --git a/src/geometry/manifold/cont_mdiff_mfderiv.lean b/src/geometry/manifold/cont_mdiff_mfderiv.lean
@@ -206,7 +206,7 @@ begin
   { apply cont_diff_on.prod B _,
     apply C.congr (λp hp, _),
     simp only with mfld_simps at hp,
-    simp only [mfderiv_within, hf.mdifferentiable_on one_le_n _ hp.2, hp.1, dif_pos]
+    simp only [mfderiv_within, hf.mdifferentiable_on one_le_n _ hp.2, hp.1, if_pos]
       with mfld_simps },
   have D : cont_diff_on 𝕜 m (λ x,
     (fderiv_within 𝕜 (I' ∘ f ∘ I.symm) (I.symm ⁻¹' s ∩ range I) x))
@@ -633,7 +633,7 @@ begin
     { exact model_with_corners.unique_diff_at_image I },
     { exact differentiable_at_id'.prod (differentiable_at_const _) } },
   simp only [tangent_bundle.zero_section, tangent_map, mfderiv,
-    A, dif_pos, chart_at, basic_smooth_vector_bundle_core.chart,
+    A, if_pos, chart_at, basic_smooth_vector_bundle_core.chart,
     basic_smooth_vector_bundle_core.to_vector_bundle_core, tangent_bundle_core,
     function.comp, continuous_linear_map.map_zero] with mfld_simps,
   rw ← fderiv_within_inter N (I.unique_diff (I ((chart_at H x) x)) (set.mem_range_self _)) at B,
diff --git a/src/geometry/manifold/mfderiv.lean b/src/geometry/manifold/mfderiv.lean
@@ -280,7 +280,7 @@ derivative of `f` at `x` within `s`, as a continuous linear map from the tangent
 tangent space at `f x`. -/
 def mfderiv_within (f : M → M') (s : set M) (x : M) :
   tangent_space I x →L[𝕜] tangent_space I' (f x) :=
-if h : mdifferentiable_within_at I I' f s x then
+if mdifferentiable_within_at I I' f s x then
 (fderiv_within 𝕜 (written_in_ext_chart_at I I' x f) ((ext_chart_at I x).symm ⁻¹' s ∩ range I)
   ((ext_chart_at I x) x) : _)
 else 0
@@ -289,7 +289,7 @@ else 0
 `f` at `x`, as a continuous linear map from the tangent space at `x` to the tangent space at
 `f x`. -/
 def mfderiv (f : M → M') (x : M) : tangent_space I x →L[𝕜] tangent_space I' (f x) :=
-if h : mdifferentiable_at I I' f x then
+if mdifferentiable_at I I' f x then
 (fderiv_within 𝕜 (written_in_ext_chart_at I I' x f : E → E') (range I)
   ((ext_chart_at I x) x) : _)
 else 0
@@ -431,11 +431,11 @@ lemma mdifferentiable_within_at_iff_of_mem_source
 
 lemma mfderiv_within_zero_of_not_mdifferentiable_within_at
   (h : ¬ mdifferentiable_within_at I I' f s x) : mfderiv_within I I' f s x = 0 :=
-by simp only [mfderiv_within, h, dif_neg, not_false_iff]
+by simp only [mfderiv_within, h, if_neg, not_false_iff]
 
 lemma mfderiv_zero_of_not_mdifferentiable_at
   (h : ¬ mdifferentiable_at I I' f x) : mfderiv I I' f x = 0 :=
-by simp only [mfderiv, h, dif_neg, not_false_iff]
+by simp only [mfderiv, h, if_neg, not_false_iff]
 
 theorem has_mfderiv_within_at.mono (h : has_mfderiv_within_at I I' f t x f') (hst : s ⊆ t) :
   has_mfderiv_within_at I I' f s x f' :=
@@ -504,28 +504,28 @@ lemma mdifferentiable_within_at.has_mfderiv_within_at (h : mdifferentiable_withi
   has_mfderiv_within_at I I' f s x (mfderiv_within I I' f s x) :=
 begin
   refine ⟨h.1, _⟩,
-  simp only [mfderiv_within, h, dif_pos] with mfld_simps,
+  simp only [mfderiv_within, h, if_pos] with mfld_simps,
   exact differentiable_within_at.has_fderiv_within_at h.2
 end
 
 lemma mdifferentiable_within_at.mfderiv_within (h : mdifferentiable_within_at I I' f s x) :
   (mfderiv_within I I' f s x) =
   fderiv_within 𝕜 (written_in_ext_chart_at I I' x f : _) ((ext_chart_at I x).symm ⁻¹' s ∩ range I)
   ((ext_chart_at I x) x) :=
-by simp only [mfderiv_within, h, dif_pos]
+by simp only [mfderiv_within, h, if_pos]
 
 lemma mdifferentiable_at.has_mfderiv_at (h : mdifferentiable_at I I' f x) :
   has_mfderiv_at I I' f x (mfderiv I I' f x) :=
 begin
   refine ⟨h.1, _⟩,
-  simp only [mfderiv, h, dif_pos] with mfld_simps,
+  simp only [mfderiv, h, if_pos] with mfld_simps,
   exact differentiable_within_at.has_fderiv_within_at h.2
 end
 
 lemma mdifferentiable_at.mfderiv (h : mdifferentiable_at I I' f x) :
   (mfderiv I I' f x) =
   fderiv_within 𝕜 (written_in_ext_chart_at I I' x f : _) (range I) ((ext_chart_at I x) x) :=
-by simp only [mfderiv, h, dif_pos]
+by simp only [mfderiv, h, if_pos]
 
 lemma has_mfderiv_at.mfderiv (h : has_mfderiv_at I I' f x f') :
   mfderiv I I' f x = f' :=
@@ -778,7 +778,7 @@ begin
   by_cases h : mdifferentiable_within_at I I' f s x,
   { exact ((h.has_mfderiv_within_at).congr_of_eventually_eq hL hx).mfderiv_within hs },
   { unfold mfderiv_within,
-    rw [dif_neg h, dif_neg],
+    rw [if_neg h, if_neg],
     rwa ← hL.mdifferentiable_within_at_iff I I' hx }
 end
 
@@ -1037,8 +1037,8 @@ alias mdifferentiable_iff_differentiable ↔
   mfderiv_within (𝓘(𝕜, E)) (𝓘(𝕜, E')) f s x = fderiv_within 𝕜 f s x :=
 begin
   by_cases h : mdifferentiable_within_at (𝓘(𝕜, E)) (𝓘(𝕜, E')) f s x,
-  { simp only [mfderiv_within, h, dif_pos] with mfld_simps },
-  { simp only [mfderiv_within, h, dif_neg, not_false_iff],
+  { simp only [mfderiv_within, h, if_pos] with mfld_simps },
+  { simp only [mfderiv_within, h, if_neg, not_false_iff],
     rw [mdifferentiable_within_at_iff_differentiable_within_at] at h,
     exact (fderiv_within_zero_of_not_differentiable_within_at h).symm }
 end
@@ -1236,10 +1236,8 @@ Note that in the in `has_mfderiv_at` lemmas there is an abuse of the defeq betwe
 canonical, but in this case (the tangent space of a vector space) it is canonical.
  -/
 
-variables { z : M} {F' : Type*} [normed_comm_ring F'] [normed_algebra 𝕜 F']
-{f g : M → E'} {p q : M → F'} {I}
-{f' g' : tangent_space I z →L[𝕜] E'}
-{p' q' : tangent_space I z →L[𝕜] F'}
+section group
+variables {I} {z : M} {f g : M → E'} {f' g' : tangent_space I z →L[𝕜] E'}
 
 lemma has_mfderiv_at.add (hf : has_mfderiv_at I 𝓘(𝕜, E') f z f')
   (hg : has_mfderiv_at I 𝓘(𝕜, E') g z g') : has_mfderiv_at I 𝓘(𝕜, E') (f + g) z (f' + g') :=
@@ -1253,18 +1251,11 @@ lemma mdifferentiable.add (hf : mdifferentiable I 𝓘(𝕜, E') f) (hg : mdiffe
   mdifferentiable I 𝓘(𝕜, E') (f + g) :=
 λ x, (hf x).add (hg x)
 
-lemma has_mfderiv_at.mul (hp : has_mfderiv_at I 𝓘(𝕜, F') p z p')
-  (hq : has_mfderiv_at I 𝓘(𝕜, F') q z q') :
-  has_mfderiv_at I 𝓘(𝕜, F') (p * q) z (p z • q' + q z • p' : E →L[𝕜] F') :=
-⟨hp.1.mul hq.1, by simpa only with mfld_simps using hp.2.mul hq.2⟩
-
-lemma mdifferentiable_at.mul (hp : mdifferentiable_at I 𝓘(𝕜, F') p z)
-  (hq : mdifferentiable_at I 𝓘(𝕜, F') q z) : mdifferentiable_at I 𝓘(𝕜, F') (p * q) z :=
-(hp.has_mfderiv_at.mul hq.has_mfderiv_at).mdifferentiable_at
-
-lemma mdifferentiable.mul {f g : M → F'} (hf : mdifferentiable I 𝓘(𝕜, F') f)
-  (hg : mdifferentiable I 𝓘(𝕜, F') g) : mdifferentiable I 𝓘(𝕜, F') (f * g) :=
-λ x, (hf x).mul (hg x)
+lemma mfderiv_add (hf : mdifferentiable_at I 𝓘(𝕜, E') f z)
+  (hg : mdifferentiable_at I 𝓘(𝕜, E') g z) :
+  (mfderiv I 𝓘(𝕜, E') (f + g) z : tangent_space I z →L[𝕜] E') =
+  (mfderiv I 𝓘(𝕜, E') f z + mfderiv I 𝓘(𝕜, E') g z : tangent_space I z →L[𝕜] E') :=
+(hf.has_mfderiv_at.add hg.has_mfderiv_at).mfderiv
 
 lemma has_mfderiv_at.const_smul (hf : has_mfderiv_at I 𝓘(𝕜, E') f z f') (s : 𝕜) :
    has_mfderiv_at I 𝓘(𝕜, E') (s • f) z (s • f') :=
@@ -1274,22 +1265,45 @@ lemma mdifferentiable_at.const_smul (hf : mdifferentiable_at I 𝓘(𝕜, E') f
   mdifferentiable_at I 𝓘(𝕜, E') (s • f) z :=
 (hf.has_mfderiv_at.const_smul s).mdifferentiable_at
 
-lemma mdifferentiable.const_smul {f : M → E'} (s : 𝕜) (hf : mdifferentiable I 𝓘(𝕜, E') f) :
+lemma mdifferentiable.const_smul (s : 𝕜) (hf : mdifferentiable I 𝓘(𝕜, E') f) :
   mdifferentiable I 𝓘(𝕜, E') (s • f) :=
 λ x, (hf x).const_smul s
 
+lemma const_smul_mfderiv (hf : mdifferentiable_at I 𝓘(𝕜, E') f z) (s : 𝕜) :
+  (mfderiv I 𝓘(𝕜, E') (s • f) z : tangent_space I z →L[𝕜] E') =
+  (s • mfderiv I 𝓘(𝕜, E') f z : tangent_space I z →L[𝕜] E') :=
+(hf.has_mfderiv_at.const_smul s).mfderiv
+
 lemma has_mfderiv_at.neg (hf : has_mfderiv_at I 𝓘(𝕜, E') f z f') :
    has_mfderiv_at I 𝓘(𝕜, E') (-f) z (-f') :=
 ⟨hf.1.neg, hf.2.neg⟩
 
+lemma has_mfderiv_at_neg :
+  has_mfderiv_at I 𝓘(𝕜, E') (-f) z (-f') ↔ has_mfderiv_at I 𝓘(𝕜, E') f z f' :=
+⟨λ hf, by { convert hf.neg; rw [neg_neg] }, λ hf, hf.neg⟩
+
 lemma mdifferentiable_at.neg (hf : mdifferentiable_at I 𝓘(𝕜, E') f z) :
   mdifferentiable_at I 𝓘(𝕜, E') (-f) z :=
 hf.has_mfderiv_at.neg.mdifferentiable_at
 
-lemma mdifferentiable.neg {f : M → E'} (hf : mdifferentiable I 𝓘(𝕜, E') f) :
+lemma mdifferentiable_at_neg :
+  mdifferentiable_at I 𝓘(𝕜, E') (-f) z ↔ mdifferentiable_at I 𝓘(𝕜, E') f z :=
+⟨λ hf, by { convert hf.neg; rw [neg_neg] }, λ hf, hf.neg⟩
+
+lemma mdifferentiable.neg (hf : mdifferentiable I 𝓘(𝕜, E') f) :
   mdifferentiable I 𝓘(𝕜, E') (-f) :=
 λ x, (hf x).neg
 
+lemma mfderiv_neg (f : M → E') (x : M) :
+  (mfderiv I 𝓘(𝕜, E') (-f) x : tangent_space I x →L[𝕜] E') =
+  (- mfderiv I 𝓘(𝕜, E') f x : tangent_space I x →L[𝕜] E') :=
+begin
+  simp_rw [mfderiv],
+  by_cases hf : mdifferentiable_at I 𝓘(𝕜, E') f x,
+  { exact hf.has_mfderiv_at.neg.mfderiv },
+  { rw [if_neg hf], rw [← mdifferentiable_at_neg] at hf, rw [if_neg hf, neg_zero] },
+end
+
 lemma has_mfderiv_at.sub (hf : has_mfderiv_at I 𝓘(𝕜, E') f z f')
   (hg : has_mfderiv_at I 𝓘(𝕜, E') g z g') : has_mfderiv_at I 𝓘(𝕜, E') (f - g) z (f'- g') :=
 ⟨hf.1.sub hg.1, hf.2.sub hg.2⟩
@@ -1298,10 +1312,67 @@ lemma mdifferentiable_at.sub (hf : mdifferentiable_at I 𝓘(𝕜, E') f z)
   (hg : mdifferentiable_at I 𝓘(𝕜, E') g z) : mdifferentiable_at I 𝓘(𝕜, E') (f - g) z :=
 (hf.has_mfderiv_at.sub hg.has_mfderiv_at).mdifferentiable_at
 
-lemma mdifferentiable.sub {f : M → E'} (hf : mdifferentiable I 𝓘(𝕜, E') f)
+lemma mdifferentiable.sub (hf : mdifferentiable I 𝓘(𝕜, E') f)
   (hg : mdifferentiable I 𝓘(𝕜, E') g)  : mdifferentiable I 𝓘(𝕜, E') (f - g) :=
 λ x, (hf x).sub (hg x)
 
+lemma mfderiv_sub (hf : mdifferentiable_at I 𝓘(𝕜, E') f z)
+  (hg : mdifferentiable_at I 𝓘(𝕜, E') g z) :
+  (mfderiv I 𝓘(𝕜, E') (f - g) z : tangent_space I z →L[𝕜] E') =
+  (mfderiv I 𝓘(𝕜, E') f z - mfderiv I 𝓘(𝕜, E') g z : tangent_space I z →L[𝕜] E') :=
+(hf.has_mfderiv_at.sub hg.has_mfderiv_at).mfderiv
+
+end group
+
+section algebra_over_ring
+variables {I} {z : M} {F' : Type*} [normed_ring F'] [normed_algebra 𝕜 F']
+  {p q : M → F'} {p' q' : tangent_space I z →L[𝕜] F'}
+
+lemma has_mfderiv_within_at.mul' (hp : has_mfderiv_within_at I 𝓘(𝕜, F') p s z p')
+  (hq : has_mfderiv_within_at I 𝓘(𝕜, F') q s z q') :
+  has_mfderiv_within_at I 𝓘(𝕜, F') (p * q) s z (p z • q' + p'.smul_right (q z) : E →L[𝕜] F') :=
+⟨hp.1.mul hq.1, by simpa only with mfld_simps using hp.2.mul' hq.2⟩
+
+lemma has_mfderiv_at.mul' (hp : has_mfderiv_at I 𝓘(𝕜, F') p z p')
+  (hq : has_mfderiv_at I 𝓘(𝕜, F') q z q') :
+  has_mfderiv_at I 𝓘(𝕜, F') (p * q) z (p z • q' + p'.smul_right (q z) : E →L[𝕜] F') :=
+has_mfderiv_within_at_univ.mp $ hp.has_mfderiv_within_at.mul' hq.has_mfderiv_within_at
+
+lemma mdifferentiable_within_at.mul (hp : mdifferentiable_within_at I 𝓘(𝕜, F') p s z)
+  (hq : mdifferentiable_within_at I 𝓘(𝕜, F') q s z) :
+  mdifferentiable_within_at I 𝓘(𝕜, F') (p * q) s z :=
+(hp.has_mfderiv_within_at.mul' hq.has_mfderiv_within_at).mdifferentiable_within_at
+
+lemma mdifferentiable_at.mul (hp : mdifferentiable_at I 𝓘(𝕜, F') p z)
+  (hq : mdifferentiable_at I 𝓘(𝕜, F') q z) : mdifferentiable_at I 𝓘(𝕜, F') (p * q) z :=
+(hp.has_mfderiv_at.mul' hq.has_mfderiv_at).mdifferentiable_at
+
+lemma mdifferentiable_on.mul (hp : mdifferentiable_on I 𝓘(𝕜, F') p s)
+  (hq : mdifferentiable_on I 𝓘(𝕜, F') q s) : mdifferentiable_on I 𝓘(𝕜, F') (p * q) s :=
+λ x hx, (hp x hx).mul $ hq x hx
+
+lemma mdifferentiable.mul (hp : mdifferentiable I 𝓘(𝕜, F') p)
+  (hq : mdifferentiable I 𝓘(𝕜, F') q) : mdifferentiable I 𝓘(𝕜, F') (p * q) :=
+λ x, (hp x).mul (hq x)
+
+end algebra_over_ring
+
+section algebra_over_comm_ring
+variables {I} {z : M} {F' : Type*} [normed_comm_ring F'] [normed_algebra 𝕜 F']
+  {p q : M → F'} {p' q' : tangent_space I z →L[𝕜] F'}
+
+lemma has_mfderiv_within_at.mul (hp : has_mfderiv_within_at I 𝓘(𝕜, F') p s z p')
+  (hq : has_mfderiv_within_at I 𝓘(𝕜, F') q s z q') :
+  has_mfderiv_within_at I 𝓘(𝕜, F') (p * q) s z (p z • q' + q z • p' : E →L[𝕜] F') :=
+by { convert hp.mul' hq, ext z, apply mul_comm }
+
+lemma has_mfderiv_at.mul (hp : has_mfderiv_at I 𝓘(𝕜, F') p z p')
+  (hq : has_mfderiv_at I 𝓘(𝕜, F') q z q') :
+  has_mfderiv_at I 𝓘(𝕜, F') (p * q) z (p z • q' + q z • p' : E →L[𝕜] F') :=
+has_mfderiv_within_at_univ.mp $ hp.has_mfderiv_within_at.mul hq.has_mfderiv_within_at
+
+end algebra_over_comm_ring
+
 end arithmetic
 
 namespace model_with_corners
