More lemmas, add a missing assumption in the definition

SardMoreira/Chart.lean

@@ -1,8 +1,9 @@
 import SardMoreira.ContDiffMoreiraHolder
 import Mathlib.Analysis.Normed.Affine.Isometry
+import Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual
 
 open scoped unitInterval Topology NNReal
-open Asymptotics Filter Set Metric
+open Asymptotics Filter Set Metric Function
 
 namespace MoreiraSard
 
@@ -38,7 +39,8 @@ structure Chart (k : ℕ) (α : I) (l : Fin (k + 1)) (s U : Set (E × F)) where
   fderiv_comp_eq_zero' (i : Fin l) (f : E → (subspace i.castSucc) → ℝ) :
     ContDiffMoreiraHolderOn (k - i) α f.uncurry (holderSet i.castSucc)
       (ball 0 (radiusLeft i.castSucc) ×ˢ ball 0 (radiusRight i.castSucc)) →
-    ∀ x y, (x, y) ∈ holderSet i.succ → fderiv ℝ (f x ∘ toFunSnd i x) = 0
+    (∀ p ∈ holderSet i.castSucc, f p.1 p.2 = 0) →
+    ∀ x y, (x, y) ∈ holderSet i.succ → fderiv ℝ (f x ∘ toFunSnd i x) y = 0
 
 namespace Chart
 
@@ -90,7 +92,23 @@ theorem fderiv_comp_eq_zero (ψ : Chart k α l s U) (i : Fin l) {f : E × ψ.sub
     (hf : ContDiffMoreiraHolderOn (k - i) α f (ψ.holderSet i.castSucc) (ψ.dom i.castSucc))
     (hf₀ : ∀ x ∈ ψ.holderSet i.castSucc, f x = 0) {x : E × ψ.subspace i.succ}
     (hx : x ∈ ψ.holderSet i.succ) : fderiv ℝ (f ∘ ψ i ∘ .mk x.1) x.2 = 0 := by
-  sorry
+  suffices ∀ g : G →L[ℝ] ℝ, g.comp (fderiv ℝ (f ∘ ψ i ∘ .mk x.1) x.2) = 0 by
+    ext y
+    -- TODO: add `SeparatingDual.ext`
+    by_contra hy
+    obtain ⟨g, hg⟩ := SeparatingDual.exists_ne_zero (R := ℝ) hy
+    exact hg (DFunLike.congr_fun (this g) y)
+  intro g
+  rw [← g.fderiv, ← fderiv_comp]
+  · refine ψ.fderiv_comp_eq_zero' i (fun a b ↦ g (f (a, b))) ?_ ?_ x.1 x.2 hx
+    · exact hf.continuousLinearMap_comp g
+    · simp +contextual [hf₀]
+  · exact g.differentiableAt
+  · apply ContDiffAt.differentiableAt (n := (k - i : ℕ)) _ (by norm_cast; omega)
+    apply ((hf.contDiffOn.comp (ψ.contDiffMoreiraHolderOn i).contDiffOn _).contDiffAt _).comp
+    · refine contDiffAt_const.prod contDiffAt_id
+    · exact ψ.mapsTo_dom _
+    · exact (ψ.isOpen_dom _).mem_nhds <| ψ.holderSet_subset_dom _ hx
 
 def compUpTo (ψ : Chart k α l s U) (i : Fin (l + 1)) : E × ψ.subspace i → E × F :=
   i.induction (fun xy ↦ (xy.1, xy.2.1) + ψ.center) fun j ↦ (· ∘ ψ j)

SardMoreira/ContDiff.lean

@@ -5,8 +5,11 @@ open Asymptotics Filter Set
 
 variable {𝕜 E F G : Type*} [NontriviallyNormedField 𝕜]
   [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+  [NormedAddCommGroup G] [NormedSpace 𝕜 G]
   {f : E → F} {s : Set E} {n : WithTop ℕ∞} {k : ℕ} {a : E}
 
+protected alias UniqueDiffOn.univ := uniqueDiffOn_univ
+
 theorem ContDiffOn.continuousAt_iteratedFDerivWithin (hf : ContDiffOn 𝕜 n f s)
     (hs : UniqueDiffOn 𝕜 s) (ha : s ∈ 𝓝 a) (hk : k ≤ n) :
     ContinuousAt (iteratedFDerivWithin 𝕜 k f s) a :=
@@ -26,3 +29,23 @@ theorem ContDiffAt.differentiableAt_iteratedFDeriv (hf : ContDiffAt 𝕜 n f a)
     DifferentiableAt 𝕜 (iteratedFDeriv 𝕜 k f) a := by
   simp only [← differentiableWithinAt_univ, ← iteratedFDerivWithin_univ]
   exact hf.differentiableWithinAt_iteratedFDerivWithin hk (by simp [uniqueDiffOn_univ])
+
+/-- Generalizes `ContinuousLinearMap.iteratedFderivWithin_comp_left`
+by weakening a `ContDiffOn` assumption to `ContDiffWithinAt`.  -/
+theorem ContinuousLinearMap.iteratedFDerivWithin_comp_left' (g : F →L[𝕜] G)
+    (hf : ContDiffWithinAt 𝕜 n f s a) (hs : UniqueDiffOn 𝕜 s) (ha : a ∈ s) {i : ℕ} (hi : i ≤ n) :
+    iteratedFDerivWithin 𝕜 i (g ∘ f) s a =
+      g.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s a) := by
+  rcases hf.contDiffOn' hi (by simp) with ⟨U, hU, haU, hfU⟩
+  rw [← iteratedFDerivWithin_inter_open hU haU, ← iteratedFDerivWithin_inter_open (f := f) hU haU]
+  rw [insert_eq_of_mem ha] at hfU
+  exact .symm <| (hfU.ftaylorSeriesWithin (hs.inter hU)).continuousLinearMap_comp g
+    |>.eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter hU) ⟨ha, haU⟩
+
+/-- Generalizes `ContinuousLinearMap.iteratedFderiv_comp_left`
+by weakening a `ContDiff` assumption to `ContDiffAt`.  -/
+theorem ContinuousLinearMap.iteratedFDeriv_comp_left' (g : F →L[𝕜] G) (hf : ContDiffAt 𝕜 n f a)
+    {i : ℕ} (hi : i ≤ n) :
+    iteratedFDeriv 𝕜 i (g ∘ f) a = g.compContinuousMultilinearMap (iteratedFDeriv 𝕜 i f a) := by
+  simp only [← iteratedFDerivWithin_univ]
+  exact g.iteratedFDerivWithin_comp_left' hf.contDiffWithinAt .univ (mem_univ _) hi

SardMoreira/ContDiffMoreiraHolder.lean

@@ -93,11 +93,24 @@ theorem prodMk {k : ℕ} {α : I} {f : E → F} {g : E → G} {a : E}
   contDiffAt := hf.contDiffAt.prod hg.contDiffAt
   isBigO := sorry
 
+-- See `YK-moreira` branch in Mathlib
 theorem comp {g : F → G} {f : E → F} {a : E} {k : ℕ} {α : I}
     (hg : ContDiffMoreiraHolderAt k α g (f a)) (hf : ContDiffMoreiraHolderAt k α f a) (hk : k ≠ 0) :
     ContDiffMoreiraHolderAt k α (g ∘ f) a :=
   sorry
 
+theorem continuousLinearMap_comp {f : E → F} {a : E} {k : ℕ} {α : I}
+    (hf : ContDiffMoreiraHolderAt k α f a) (g : F →L[ℝ] G) :
+    ContDiffMoreiraHolderAt k α (g ∘ f) a where
+  contDiffAt := g.contDiff.contDiffAt.comp a hf.contDiffAt
+  isBigO := by
+    refine .trans (.of_bound ‖g‖ ?_) hf.isBigO
+    refine (hf.contDiffAt.eventually (by simp)).mono fun x hx ↦ ?_
+    rw [g.iteratedFDeriv_comp_left' hx le_rfl, g.iteratedFDeriv_comp_left' hf.contDiffAt le_rfl]
+    -- TODO: add `ContinuousLinearMap.compContinuousMultilinearMap_sub`
+    convert g.norm_compContinuousMultilinearMap_le _
+    ext; simp
+
 end ContDiffMoreiraHolderAt
 
 structure ContDiffMoreiraHolderOn (k : ℕ) (α : I) (f : E → F) (s U : Set E) : Prop where
@@ -156,4 +169,10 @@ theorem comp {g : F → G} {t V : Set F} (hg : ContDiffMoreiraHolderOn k α g t
   isBigO _a ha := ((hg.contDiffMoreiraHolderAt <| hst ha).comp
     (hf.contDiffMoreiraHolderAt ha) hk).isBigO
 
+theorem continuousLinearMap_comp (hf : ContDiffMoreiraHolderOn k α f s U) (g : F →L[ℝ] G) :
+    ContDiffMoreiraHolderOn k α (g ∘ f) s U where
+  __ := hf
+  contDiffOn := g.contDiff.comp_contDiffOn hf.contDiffOn
+  isBigO _a ha := ((hf.contDiffMoreiraHolderAt ha).continuousLinearMap_comp g).isBigO
+
 end ContDiffMoreiraHolderOn