From c2507d2d745a247716fda42aaf15c9ecfa21e65d Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sat, 21 Dec 2024 00:59:51 -0600
Subject: [PATCH] +1 lemma

---
 SardMoreira/ContDiffHolder.lean | 34 ++++++++++++++++++++++++++++++++-
 SardMoreira/LocalEstimates.lean | 11 +++--------
 blueprint/src/content.tex       |  2 ++
 3 files changed, 38 insertions(+), 9 deletions(-)

diff --git a/SardMoreira/ContDiffHolder.lean b/SardMoreira/ContDiffHolder.lean
index 06586cd..8475c83 100644
--- a/SardMoreira/ContDiffHolder.lean
+++ b/SardMoreira/ContDiffHolder.lean
@@ -2,7 +2,7 @@ import Mathlib.Analysis.Calculus.ContDiff.Defs
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 
 open scoped unitInterval Topology
-open Asymptotics Filter
+open Asymptotics Filter Set
 
 section NormedField
 
@@ -11,8 +11,40 @@ variable {𝕜 E F G : Type*} [NontriviallyNormedField 𝕜]
   [NormedAddCommGroup F] [NormedSpace 𝕜 F]
   [NormedAddCommGroup G] [NormedSpace 𝕜 G]
 
+theorem ContDiffOn.continuousAt_iteratedFDerivWithin {f : E → F} {s : Set E} {n : WithTop ℕ∞}
+    {k : ℕ} {a : E} (hf : ContDiffOn 𝕜 n f s) (hs : UniqueDiffOn 𝕜 s) (ha : s ∈ 𝓝 a) (hk : k ≤ n) :
+    ContinuousAt (iteratedFDerivWithin 𝕜 k f s) a :=
+  (hf.continuousOn_iteratedFDerivWithin hk hs).continuousAt ha
+
+theorem ContDiffWithinAt.continuousWithinAt_iteratedFDerivWithin
+    {f : E → F} {s : Set E} {n : WithTop ℕ∞} {k : ℕ} {a : E} (hf : ContDiffWithinAt 𝕜 n f s a)
+    (hs : UniqueDiffOn 𝕜 (insert a s)) (hk : k ≤ n) :
+    ContinuousWithinAt (iteratedFDerivWithin 𝕜 k f s) s a := by
+  rcases hf.contDiffOn' hk (by simp) with ⟨U, hUo, haU, hfU⟩
+  have H := hfU.continuousOn_iteratedFDerivWithin le_rfl (hs.inter hUo) a ⟨mem_insert _ _, haU⟩
+  rw [← continuousWithinAt_insert_self]
+  have {b t} (hb : b ∈ U) : (t ∩ U : Set E) =ᶠ[𝓝 b] t :=
+    inter_eventuallyEq_left.2 <| mem_nhds_iff.mpr ⟨U, fun _ h _ ↦ h, hUo, hb⟩
+  refine (H.congr_of_mem (fun y hy ↦ ?_) (by simpa)).congr_set (this haU)
+  rw [← iteratedFDerivWithin_insert, iteratedFDerivWithin_congr_set (this hy.2)]
+
+theorem ContDiffAt.continuousAt_iteratedFDeriv
+    {f : E → F} {n : WithTop ℕ∞} {k : ℕ} {a : E} (hf : ContDiffAt 𝕜 n f a) (hk : k ≤ n) :
+    ContinuousAt (iteratedFDeriv 𝕜 k f) a := by
+  simp only [← continuousWithinAt_univ, ← iteratedFDerivWithin_univ]
+  exact hf.contDiffWithinAt.continuousWithinAt_iteratedFDerivWithin (by simp [uniqueDiffOn_univ]) hk
+
 variable (𝕜) in
 structure ContDiffHolderAt (k : ℕ) (α : I) (f : E → F) (a : E) : Prop where
   contDiffAt : ContDiffAt 𝕜 k f a
   isBigO : (iteratedFDeriv 𝕜 k f · - iteratedFDeriv 𝕜 k f a) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ (α : ℝ)
 
+namespace ContDiffHolderAt
+
+@[simp]
+theorem zero_exponent_iff {k : ℕ} {f : E → F} {a : E} :
+    ContDiffHolderAt 𝕜 k 0 f a ↔ ContDiffAt 𝕜 k f a := by
+  refine ⟨contDiffAt, fun h ↦ ⟨h, ?_⟩⟩
+  simpa using ((h.continuousAt_iteratedFDeriv le_rfl).sub_const _).norm.isBoundedUnder_le
+
+end ContDiffHolderAt
diff --git a/SardMoreira/LocalEstimates.lean b/SardMoreira/LocalEstimates.lean
index 5547219..17ed300 100644
--- a/SardMoreira/LocalEstimates.lean
+++ b/SardMoreira/LocalEstimates.lean
@@ -21,14 +21,9 @@ variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensi
 -- lemma aux_hmeas {a b : ℝ} (h : a ≤ b) : volume (Set.Icc a b) = b - a := sorry
 
 -- XXX: is this in mathlib already?
-lemma measure_finite_of_subset {α : Type*} [MeasureSpace α] {μ : Measure α} {s t : Set α}
-    (ht : μ t < ⊤) (hst : s ⊆ t) : μ s < ⊤ := by
-  trans (μ t + 1); swap; simpa
-  suffices hyp: μ s ≤ μ t by calc
-    _ ≤ μ t := hyp
-    _ < μ t + 1 := by sorry
-  apply μ.mono hst
-
+lemma measure_finite_of_subset {α : Type*} [MeasurableSpace α] {μ : Measure α} {s t : Set α}
+    (ht : μ t < ⊤) (hst : s ⊆ t) : μ s < ⊤ :=
+  (measure_mono hst).trans_lt ht
 
 -- Lemma 8 in the blueprint: the statement might be slightly off, check carefully!
 lemma cdh_at_sub_affine_le_of_meas {f : E → F} {a b : E} {C r : NNReal} {δ : ℝ} (hδ : δ ∈ (Set.Ioo (0 : ℝ) 1))
diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex
index bd82b48..38c941d 100644
--- a/blueprint/src/content.tex
+++ b/blueprint/src/content.tex
@@ -100,6 +100,8 @@ \section{\(C^{k}\) maps with locally Hölder derivatives}
 
 \begin{lemma}%
   \label{lem:cdh-at-zero}
+  \lean{ContDiffHolderAt.zero_exponent_iff}
+  \leanok
   \uses{def:cdh-at}
   A map \(f\colon E\to F\) is \(C^{k+(0)}\) at \(a\) iff it is \(C^{k}\) at \(a\).
 \end{lemma}