some cleanup (#117)

* Open namespace `MeasureTheory` in various places
* Add `\leanok` to statements of section 7.1

CONTRIBUTING.md

@@ -33,7 +33,7 @@ Below, I will try to give a translation of some notation/conventions. We use mat
 | `Kₛ(x, y)`       | `Ks s x y`       |         |
 | `T_* f(x)`       | `nontangentialOperator K f x`       | The associated nontangential Calderon Zygmund operator |
 | `T_Q^θ f(x)`       | `linearizedNontangentialOperator Q θ K f x`       | The linearized associated nontangential Calderon Zygmund operator |
-| `T f(x)`       | `CarlesonOperator K f x` | The generalized Carleson operator        |
+| `T f(x)`       | `carlesonOperator K f x` | The generalized Carleson operator        |
 | `T_Q f(x)`       | `linearizedCarlesonOperator Q K f x` | The linearized generalized Carleson operator        |
 | `T_𝓝^θ f(x)`       | `nontangentialMaximalFunction K θ f x` |   |
 | `Tₚ f(x)`       | `carlesonOn p f x`       |         |

Carleson/AntichainOperator.lean

@@ -146,12 +146,12 @@ lemma MaximalBoundAntichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤
         /- simp only [T, indicator, if_pos hxE, mul_ite, mul_zero, ENNReal.coe_le_coe,
           ← NNReal.coe_le_coe, coe_nnnorm] -/
         /- simp only [T, indicator, if_pos hxE]
-        apply le_trans (MeasureTheory.ennnorm_integral_le_lintegral_ennnorm _)
-        apply MeasureTheory.lintegral_mono
+        apply le_trans (ennnorm_integral_le_lintegral_ennnorm _)
+        apply lintegral_mono
         intro z w -/
         simp only [carlesonOn, indicator, if_pos hxE]
-        apply le_trans (MeasureTheory.ennnorm_integral_le_lintegral_ennnorm _)
-        apply MeasureTheory.lintegral_mono
+        apply le_trans (ennnorm_integral_le_lintegral_ennnorm _)
+        apply lintegral_mono
         intro z w
         simp only [nnnorm_mul, coe_mul, some_eq_coe', Nat.cast_pow,
           Nat.cast_ofNat, zpow_neg, mul_ite, mul_zero]
@@ -194,7 +194,7 @@ lemma MaximalBoundAntichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤
     _ = (2 : ℝ≥0)^(5*a + 101*a^3) * ⨍⁻ y, ‖f y‖₊ ∂volume.restrict (ball (𝔠 p.1) (8*D ^ 𝔰 p.1)) := by
       congr 2
 
-      --apply MeasureTheory.Measure.restrict_congr_set
+      --apply Measure.restrict_congr_set
       --refine ae_eq_of_subset_of_measure_ge ?_ ?_ ?_ ?_
       --sorry
       sorry
@@ -282,7 +282,7 @@ lemma Dens2Antichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤·) (
       apply mul_le_mul_of_nonneg_right _ (zero_le _)
       have h2 : (2 : ℝ≥0∞) ^ (107 * a ^ 3) = ‖(2 : ℝ) ^ (107 * a ^ 3)‖₊ := by
         simp only [nnnorm_pow, nnnorm_two, ENNReal.coe_pow, coe_ofNat]
-      rw [h2, ← MeasureTheory.eLpNorm_const_smul]
+      rw [h2, ← eLpNorm_const_smul]
       apply eLpNorm_mono_nnnorm
       intro z
       have MB_top : MB volume (↑𝔄) 𝔠 (fun 𝔭 ↦ 8 * ↑D ^ 𝔰 𝔭) f z ≠ ⊤ := by

Carleson/Classical/CarlesonOnTheRealLine.lean

@@ -11,8 +11,6 @@ import Carleson.Classical.CarlesonOperatorReal
 import Carleson.Classical.VanDerCorput
 
 import Mathlib.Analysis.Fourier.AddCircle
-import Mathlib.MeasureTheory.Integral.IntervalIntegral
-import Mathlib.Analysis.SpecialFunctions.Integrals
 
 noncomputable section
 
@@ -596,12 +594,12 @@ lemma carlesonOperatorReal_le_carlesonOperator : T ≤ carlesonOperator K := by
 lemma rcarleson {F G : Set ℝ} (hF : MeasurableSet F) (hG : MeasurableSet G)
     (f : ℝ → ℂ) (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
     ∫⁻ x in G, T f x ≤
-    ENNReal.ofReal (C10_0_1 4 2) * (MeasureTheory.volume G) ^ (2 : ℝ)⁻¹ * (MeasureTheory.volume F) ^ (2 : ℝ)⁻¹ := by
+    ENNReal.ofReal (C10_0_1 4 2) * (volume G) ^ (2 : ℝ)⁻¹ * (volume F) ^ (2 : ℝ)⁻¹ := by
   have conj_exponents : Real.IsConjExponent 2 2 := by rw [Real.isConjExponent_iff_eq_conjExponent] <;> norm_num
   calc ∫⁻ x in G, T f x
     _ ≤ ∫⁻ x in G, carlesonOperator K f x :=
-      MeasureTheory.lintegral_mono (carlesonOperatorReal_le_carlesonOperator _)
-    _ ≤ ENNReal.ofReal (C10_0_1 4 2) * (MeasureTheory.volume G) ^ (2 : ℝ)⁻¹ * (MeasureTheory.volume F) ^ (2 : ℝ)⁻¹ :=
+      lintegral_mono (carlesonOperatorReal_le_carlesonOperator _)
+    _ ≤ ENNReal.ofReal (C10_0_1 4 2) * (volume G) ^ (2 : ℝ)⁻¹ * (volume F) ^ (2 : ℝ)⁻¹ :=
       two_sided_metric_carleson (a := 4) (by norm_num) (by simp) conj_exponents hF hG Hilbert_strong_2_2 f hmf hf
 
 end section

Carleson/Classical/CarlesonOperatorReal.lean

@@ -5,6 +5,8 @@ import Carleson.Classical.HilbertKernel
 
 noncomputable section
 
+open MeasureTheory
+
 --TODO: avoid this extra definition?
 def carlesonOperatorReal (K : ℝ → ℝ → ℂ) (f : ℝ → ℂ) (x : ℝ) : ENNReal :=
   ⨆ (n : ℤ) (r : ℝ) (_ : 0 < r) (_ : r < 1),
@@ -24,8 +26,8 @@ lemma annulus_real_eq {x r R: ℝ} (r_nonneg : 0 ≤ r) : {y | dist x y ∈ Set.
     · exact ⟨by right; linarith, by constructor <;> linarith⟩
 
 lemma annulus_real_volume {x r R : ℝ} (hr : r ∈ Set.Icc 0 R) :
-    MeasureTheory.volume {y | dist x y ∈ Set.Ioo r R} = ENNReal.ofReal (2 * (R - r)) := by
-  rw [annulus_real_eq hr.1, MeasureTheory.measure_union _ measurableSet_Ioo, Real.volume_Ioo, Real.volume_Ioo, ← ENNReal.ofReal_add (by linarith [hr.2]) (by linarith [hr.2])]
+    volume {y | dist x y ∈ Set.Ioo r R} = ENNReal.ofReal (2 * (R - r)) := by
+  rw [annulus_real_eq hr.1, measure_union _ measurableSet_Ioo, Real.volume_Ioo, Real.volume_Ioo, ← ENNReal.ofReal_add (by linarith [hr.2]) (by linarith [hr.2])]
   ring_nf
   rw [Set.disjoint_iff]
   intro y hy
@@ -72,7 +74,7 @@ lemma carlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
     congr with _
     congr with _
     congr 2
-    rw [← MeasureTheory.integral_indicator annulus_measurableSet]
+    rw [← integral_indicator annulus_measurableSet]
   rw [this]
   set Q : Set ℝ := Rat.cast '' Set.univ with Qdef
   have hQ : Dense Q ∧ Countable Q := by
@@ -108,7 +110,7 @@ lemma carlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
       · apply isOpen_Ioo
       · rw [Sdef]
         constructor <;> linarith [hr.1]
-    apply MeasureTheory.continuousAt_of_dominated _  h_bound
+    apply continuousAt_of_dominated _  h_bound
     · have F_bound_on_set :  ∀ a ∈ {y | dist x y ∈ Set.Ioo (r / 2) 1},
           ‖f a * K x a * (Complex.I * ↑n * ↑a).exp‖ ≤ B * ‖2 ^ (2 : ℝ) / (2 * (r / 2))‖ := by
         intro a ha
@@ -130,13 +132,13 @@ lemma carlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
                 exact ha.1.le
       rw [bound_def, Fdef]
       conv => pattern ‖_‖; rw [norm_indicator_eq_indicator_norm]
-      rw [MeasureTheory.integrable_indicator_iff annulus_measurableSet]
-      apply MeasureTheory.Measure.integrableOn_of_bounded
+      rw [integrable_indicator_iff annulus_measurableSet]
+      apply Measure.integrableOn_of_bounded
       · rw [annulus_real_volume (by constructor <;> linarith [hr.1, hr.2])]
         exact ENNReal.ofReal_ne_top
       · apply ((Measurable.of_uncurry_left (measurable_mul_kernel f_measurable)).norm).aestronglyMeasurable
       · --interesting part
-        rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet]
+        rw [ae_restrict_iff' annulus_measurableSet]
         simp_rw [norm_norm]
         apply Filter.Eventually.of_forall
         apply F_bound_on_set
@@ -200,8 +202,8 @@ lemma carlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
         rcases this with h | h
         · left; linarith
         · right; linarith
-      rw [MeasureTheory.ae_iff]
-      exact MeasureTheory.measure_mono_null subset_finite (Finset.measure_zero _ _)
+      rw [ae_iff]
+      exact measure_mono_null subset_finite (Finset.measure_zero _ _)
     · exact Filter.Eventually.of_forall fun r ↦ ((Measurable.of_uncurry_left
         (measurable_mul_kernel f_measurable)).indicator annulus_measurableSet).aestronglyMeasurable
   rw [this]
@@ -210,7 +212,7 @@ lemma carlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
   intro r _
   apply measurable_coe_nnreal_ennreal.comp (measurable_nnnorm.comp _)
   rw [← stronglyMeasurable_iff_measurable]
-  apply MeasureTheory.StronglyMeasurable.integral_prod_right
+  apply StronglyMeasurable.integral_prod_right
   rw [stronglyMeasurable_iff_measurable, Fdef]
   exact (measurable_mul_kernel f_measurable).indicator (measurable_dist measurableSet_Ioo)
 
@@ -252,7 +254,7 @@ lemma carlesonOperatorReal_mul {f : ℝ → ℂ} {x : ℝ} {a : ℝ} (ha : 0 < a
   apply NNReal.eq
   simp only [coe_nnnorm, NNReal.coe_mul]
   rw [← Real.norm_of_nonneg (@NNReal.zero_le_coe a.toNNReal), ← Complex.norm_real, ← norm_mul,
-    ← MeasureTheory.integral_mul_left, Real.coe_toNNReal a ha.le]
+    ← integral_mul_left, Real.coe_toNNReal a ha.le]
   congr with y
   field_simp
   rw [mul_div_cancel_left₀]

Carleson/Classical/ClassicalCarleson.lean

@@ -214,7 +214,7 @@ theorem carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Perio
     intro x
     conv => pattern S_ _ _ _; rw [partialFourierSum_periodic]
     conv => pattern f _; rw [periodic_f]
-  apply MeasureTheory.ae_restrict_of_ae_eq_of_ae_restrict MeasureTheory.Ico_ae_eq_Icc.symm
+  apply ae_restrict_of_ae_eq_of_ae_restrict Ico_ae_eq_Icc.symm
   rw [zero_add]
 
   -- Show a.e. convergence on [0,2π]