Cleanup

SardMoreira/LocalEstimates.lean

@@ -7,60 +7,47 @@ import Mathlib.MeasureTheory.Measure.Haar.OfBasis
 import Mathlib.Order.CompletePartialOrder
 import Mathlib.MeasureTheory.Integral.SetIntegral
 
+import Mathlib
+
 open scoped unitInterval Topology
-open Asymptotics Filter
+open Asymptotics Filter MeasureTheory
 
 section NormedField
 
-variable {𝕜 E F G : Type*} --[NontriviallyNormedField 𝕜]
-  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
+variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
   [NormedAddCommGroup F] [NormedSpace ℝ F]
---  [NormedAddCommGroup G] [NormedSpace 𝕜 G]
-
-
-open scoped Convex
-open MeasureTheory
 
 -- 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))
-    (hf : DifferentiableOn ℝ f [a -[ℝ] b])
+    (hf : DifferentiableOn ℝ f (segment ℝ a b))
     (hf' : ∀ t : ℝ, t ∈ I →
       ‖lineDeriv ℝ f (a + t • (b - a)) (b - a)‖ ≤ C * (t ^ r.toReal) * ‖b - a‖₊ ^ (1 + r).toReal)
     {s : Set ℝ} (hsmeas : 1 - δ ≤ (volume (I ∩ s)).toReal)
     (hs' : ∀ t : ℝ, t ∈ s → lineDeriv ℝ f (a + t • (b - a)) (b - a) = 0) :
     ‖f b - f a‖ ≤ C * δ * (‖b - a‖₊ ^ (1 + r).toReal) := by
 
   have aux₁ : volume I = 1 := sorry -- surely in mathlib
-  have asdf := calc (volume (I ∩ sᶜ)).toReal + (volume (I ∩ s)).toReal
-        _ ≤ (volume ((I ∩ sᶜ) ∪ (I ∩ s))).toReal := by
-          let asdf := MeasureTheory.measure_union_le (I ∩ sᶜ) (I ∩ s) (μ := volume)
-          have : volume (I ∩ s) < ⊤ := by
-            trans 1; swap; simp
-            rw [← aux₁]
-            have : I ∩ s ⊆ I := by exact Set.inter_subset_left
-            sorry -- let asdf := volume.mono this
-          -- similarly for the other sets, hence asdf should imply the claim
-          -- (or, better idea: see if one can choose the numbers more wisely to avoid this hassle)
-          sorry
-        _ = (volume I).toReal := by
-          congr
-          -- the following is surely in mathlib
-          have : ∀ a b c : Set ℝ, (a ∩ b) ∪ (a ∩ c) = a ∩ (b ∪ c) := by
-            intro a b c
-            ext x
-            simp
-            aesop
-          have : I ∩ sᶜ ∪ I ∩ s = (I ∩ (s ∪ sᶜ)) := by rw [Set.union_comm s]; exact this I sᶜ s
-          rw [this, Set.union_compl_self s, Set.inter_univ]
-        _ = 1 := by rw [aux₁]; simp
+  have asdf := calc (volume (I ∩ s)).toReal + (volume (I ∩ sᶜ)).toReal
+    _ ≤ (volume ((I ∩ s) ∪ (I ∩ sᶜ))).toReal := by
+      let aux := MeasureTheory.measure_union_le (I ∩ s) (I ∩ sᶜ) (μ := volume)
+      have : volume (I ∩ s) < ⊤ := by
+        trans 1; swap; simp
+        rw [← aux₁]
+        have : I ∩ s ⊆ I := Set.inter_subset_left
+        sorry -- let asdf := volume.mono this is "almost" what's needed
+      -- similarly for the other sets, hence |aux| should imply the claim
+      -- (or, better idea: see if one can choose the numbers more wisely to avoid this hassle)
+      sorry
+    _ = (volume I).toReal := by congr; simp
+    _ = 1 := by rw [aux₁]; simp
   have hscompl : (volume (I ∩ sᶜ)).toReal ≤ δ := calc (volume (I ∩ sᶜ)).toReal
     _ ≤ 1 - (volume (I ∩ s)).toReal := by linarith [asdf]
     _ ≤ 1 - (1 - δ) := by gcongr
     _ = δ := by ring
 
   calc ‖f b - f a‖
     _ = ‖∫ t in I, lineDeriv ℝ f (a + t • (b - a)) (b - a)‖ := by
-      sorry -- standard form of MVT, somewhere in mathlib
+      sorry -- standard form of MVT, surely somewhere in mathlib
 
     -- use MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae for the next few steps,
     -- move part of these steps into showing the hypothesis