Cleanup base folder (except Psi.lean) (#476)

More cleanup, this time the base folder. Main focus was to ensure all
ToMathlib elements were caught, and to fix (whitespace) style of the
statements. In some files the proofs can be further optimized as well
but IMO that does not have the priority at this moment.

The reason to omit `Psi.lean` is because it contains a lot of stuff
formalized using `norm` instead of `enorm` and it might be better to
refactor into `enorm` entirely (as the `enorm` versions are used
downstream).
And that seemed like a task better put in a separate PR.

Author: JasperMS

Carleson.lean

@@ -85,6 +85,7 @@ import Carleson.ToMathlib.RealInterpolation.LorentzInterpolation
 import Carleson.ToMathlib.RealInterpolation.Main
 import Carleson.ToMathlib.RealInterpolation.Minkowski
 import Carleson.ToMathlib.RealInterpolation.Misc
+import Carleson.ToMathlib.Topology.Algebra.Support
 import Carleson.ToMathlib.Topology.Instances.AddCircle.Defs
 import Carleson.ToMathlib.WeakType
 import Carleson.TwoSidedCarleson.Basic

Carleson/FinitaryCarleson.lean

@@ -63,8 +63,8 @@ lemma exists_Grid {x : X} (hx : x ∈ G) {s : ℤ} (hs : s ∈ (Icc (σ₁ x) (
   simpa only [mem_iUnion, exists_prop] using Grid_subset_biUnion s s_mem x_mem_topCube
 
 /-- Lemma 4.0.3 -/
-theorem tile_sum_operator {G' : Set X} {f : X → ℂ}
-    {x : X} (hx : x ∈ G \ G') : ∑ (p : 𝔓 X), carlesonOn p f x =
+theorem tile_sum_operator {G' : Set X} {f : X → ℂ} {x : X} (hx : x ∈ G \ G') :
+    ∑ (p : 𝔓 X), carlesonOn p f x =
     ∑ s ∈ Icc (σ₁ x) (σ₂ x), ∫ y, Ks s x y * f y * exp (I * (Q x y - Q x x)) := by
   classical
   rw [𝔓_biUnion, Finset.sum_biUnion]; swap
@@ -101,6 +101,7 @@ def C2_0_1 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := C2_0_2 a q
 lemma C2_0_1_pos [TileStructure Q D κ S o] : C2_0_1 a nnq > 0 := C2_0_2_pos
 
 variable (X) in
+/-- Proposition 2.0.1 -/
 theorem finitary_carleson : ∃ G', MeasurableSet G' ∧ 2 * volume G' ≤ volume G ∧
     ∀ f : X → ℂ, Measurable f → (∀ x, ‖f x‖ ≤ F.indicator 1 x) →
     ∫⁻ x in G \ G', ‖∑ s ∈ Icc (σ₁ x) (σ₂ x), ∫ y, Ks s x y * f y * exp (I * Q x y)‖ₑ ≤

Carleson/Forest.lean

@@ -11,18 +11,6 @@ variable [TileStructure Q D κ S o] {u u' p p' : 𝔓 X} {f g : Θ X}
   {C C' : Set (𝔓 X)} {x x' : X}
 
 namespace TileStructure
--- variable (X) in
--- structure Tree where
---   carrier : Set (𝔓 X)
---   nonempty : Nonempty carrier
---   ordConnected : OrdConnected carrier -- (2.0.33)
-
--- attribute [coe] Tree.carrier
--- instance : CoeTC (Tree X) (Set (𝔓 X)) where coe := Tree.carrier
--- -- instance : CoeTC (Tree X) (Finset (𝔓 X)) where coe := Tree.carrier
--- -- instance : CoeTC (Tree X) (Set (𝔓 X)) where coe p := ((p : Finset (𝔓 X)) : Set (𝔓 X))
--- instance : Membership (𝔓 X) (Tree X) := ⟨fun x p => x ∈ (p : Set _)⟩
--- instance : Preorder (Tree X) := Preorder.lift Tree.carrier
 
 variable (X) in
 /-- An `n`-forest -/

Carleson/GridStructure.lean

@@ -10,7 +10,7 @@ variable {𝕜 : Type*} [_root_.RCLike 𝕜]
 
 variable (X) in
 /-- A grid structure on `X`.
-I expect we prefer `coeGrid : Grid → Set X` over `Grid : Set (Set X)`
+We prefer `coeGrid : Grid → Set X` over `Grid : Set (Set X)`
 Note: the `s` in this paper is `-s` of Christ's paper.
 -/
 class GridStructure {A : outParam ℝ≥0} [PseudoMetricSpace X] [DoublingMeasure X A]
@@ -63,12 +63,6 @@ instance : Fintype (Grid X) := GridStructure.fintype_Grid
 instance : Coe (Grid X) (Set X) := ⟨GridStructure.coeGrid⟩
 instance : Membership X (Grid X) := ⟨fun i x ↦ x ∈ (i : Set X)⟩
 instance : PartialOrder (Grid X) := PartialOrder.lift _ GridStructure.inj
-/- These should probably not/only rarely be used. I comment them out for now,
-so that we don't accidentally use it. We can put it back if useful after all. -/
--- instance : HasSubset (Grid X) := ⟨fun i j ↦ (i : Set X) ⊆ (j : Set X)⟩
--- instance : HasSSubset (Grid X) := ⟨fun i j ↦ (i : Set X) ⊂ (j : Set X)⟩
--- @[simp] lemma Grid.subset_def : i ⊆ j ↔ (i : Set X) ⊆ (j : Set X) := .rfl
--- @[simp] lemma Grid.ssubset_def : i ⊂ j ↔ (i : Set X) ⊂ (j : Set X) := .rfl
 
 /- not sure whether these should be simp lemmas, but that might be required if we want to
   conveniently rewrite/simp with Set-lemmas -/
@@ -138,12 +132,6 @@ lemma volume_coeGrid_pos (hD : 0 < D) : 0 < volume (i : Set X) := by
 lemma volume_coeGrid_lt_top : volume (i : Set X) < ⊤ :=
   measure_lt_top_of_subset Grid_subset_ball measure_ball_ne_top
 
-/- lemma volumeNNReal_coeGrid_pos (hD : 0 < D) : 0 < volume.nnreal (i : Set X) := by
-  rw [lt_iff_le_and_ne]
-  refine ⟨zero_le _, ?_⟩
-  rw [ne_eq, eq_comm, measureNNReal_eq_zero_iff]
-  exact ne_of_gt (volume_coeGrid_pos hD) -/
-
 namespace Grid
 
 protected lemma inj : Injective (fun i : Grid X ↦ ((i : Set X), s i)) := GridStructure.inj

Carleson/HolderVanDerCorput.lean

@@ -1,4 +1,5 @@
 import Carleson.TileStructure
+import Carleson.ToMathlib.Topology.Algebra.Support
 
 /-! This should roughly contain the contents of chapter 8. -/
 
@@ -133,16 +134,16 @@ lemma integral_mul_holderApprox {R t : ℝ} (hR : 0 < R) (ht : 0 < t) (ϕ : X 
   apply ne_of_gt
   exact integral_cutoff_pos hR ht
 
--- This surely exists in mathlib; how is it named?
-lemma foo {φ : X → ℂ} (hf : ∫ x, φ x ≠ 0) : ∃ z, φ z ≠ 0 := by
-  by_contra! h
-  exact hf (by simp [h])
-
 lemma support_holderApprox_subset_aux {z : X} {R R' t : ℝ} (hR : 0 < R)
     {ϕ : X → ℂ} (hϕ : ϕ.support ⊆ ball z R') (ht : t ∈ Ioc (0 : ℝ) 1) :
     support (holderApprox R t ϕ) ⊆ ball z (R + R') := by
   intro x hx
-  choose y hy using foo (left_ne_zero_of_mul hx)
+  have : ∃ z, cutoff R t x z * ϕ z ≠ 0 := by
+    suffices ∫ y, cutoff R t x y * ϕ y ≠ 0 by
+      by_contra! h
+      exact this (by simp only [h, integral_zero])
+    apply left_ne_zero_of_mul hx
+  choose y hy using this
   have : x ∈ ball y (t * R) := by
     apply aux_8_0_4 hR ht.1
     rw [cutoff_comm]
@@ -163,19 +164,6 @@ lemma support_holderApprox_subset {z : X} {R t : ℝ} (hR : 0 < R)
   convert support_holderApprox_subset_aux hR hϕ ht using 2
   ring
 
-/- unused
-lemma tsupport_holderApprox_subset {z : X} {R t : ℝ} (hR : 0 < R)
-    {ϕ : X → ℂ} (hϕ : tsupport ϕ ⊆ ball z R) (ht : t ∈ Ioc (0 : ℝ) 1) :
-    tsupport (holderApprox R t ϕ) ⊆ ball z (2 * R) := by
-  rcases exists_pos_lt_subset_ball hR (isClosed_tsupport ϕ) hϕ with ⟨R', R'_pos, hR'⟩
-  have A : support (holderApprox R t ϕ) ⊆ ball z (R + R') :=
-    support_holderApprox_subset_aux hR ((subset_tsupport _).trans hR') ht
-  have : tsupport (holderApprox R t ϕ) ⊆ closedBall z (R + R') :=
-    (closure_mono A).trans closure_ball_subset_closedBall
-  apply this.trans (closedBall_subset_ball ?_)
-  linarith [R'_pos.2]
--/
-
 open Filter
 
 /-- Part of Lemma 8.0.1: Equation (8.0.1).
@@ -289,7 +277,7 @@ lemma norm_holderApprox_sub_le_aux {z : X} {R t : ℝ} (hR : 0 < R) (ht : 0 < t)
     ‖holderApprox R t ϕ x' - holderApprox R t ϕ x‖ ≤
       2⁻¹ * 2 ^ (4 * a) * t ^ (-1 - a : ℝ) * C * dist x x' / (2 * R) := by
   have M : (2⁻¹ * volume.real (ball x (2⁻¹ * t * R))) *
-      ‖holderApprox R t ϕ x' - holderApprox R t ϕ x‖ ≤
+        ‖holderApprox R t ϕ x' - holderApprox R t ϕ x‖ ≤
         2 * C * ∫ y, |cutoff R t x y - cutoff R t x' y| :=
     calc
       (2⁻¹ * volume.real (ball x (2⁻¹ * t * R))) * ‖holderApprox R t ϕ x' - holderApprox R t ϕ x‖
@@ -408,7 +396,7 @@ lemma norm_holderApprox_sub_le {z : X} {R t : ℝ} (hR : 0 < R) (ht : 0 < t) (h'
     {C : ℝ≥0} {ϕ : X → ℂ} (hc : Continuous ϕ) (hϕ : ϕ.support ⊆ ball z R)
     (hC : ∀ x, ‖ϕ x‖ ≤ C) {x x' : X} :
     ‖holderApprox R t ϕ x - holderApprox R t ϕ x'‖ ≤
-      2⁻¹ * 2 ^ (4 * a) * t ^ (-1 - a : ℝ) * C * dist x x' / (2 * R) := by
+    2⁻¹ * 2 ^ (4 * a) * t ^ (-1 - a : ℝ) * C * dist x x' / (2 * R) := by
   rcases lt_or_ge (dist x x') R with hx | hx
   · rw [norm_sub_rev]
     exact norm_holderApprox_sub_le_aux hR ht h't hc hϕ hC hx
@@ -444,8 +432,7 @@ lemma lipschitzWith_holderApprox {z : X} {R t : ℝ} (hR : 0 < R) (ht : 0 < t) (
   ring
 
 lemma iLipENorm_holderApprox' {z : X} {R t : ℝ} (ht : 0 < t) (h't : t ≤ 1)
-    {C : ℝ≥0} {ϕ : X → ℂ} (hc : Continuous ϕ) (hϕ : ϕ.support ⊆ ball z R)
-    (hC : ∀ x, ‖ϕ x‖ ≤ C) :
+    {C : ℝ≥0} {ϕ : X → ℂ} (hc : Continuous ϕ) (hϕ : ϕ.support ⊆ ball z R) (hC : ∀ x, ‖ϕ x‖ ≤ C) :
     iLipENorm (holderApprox R t ϕ) z (2 * R) ≤
       2 ^ (4 * a) * (ENNReal.ofReal t) ^ (-1 - a : ℝ) * C := by
   let C' : ℝ≥0 := 2 ^ (4 * a) * (t.toNNReal) ^ (-1 - a : ℝ) * C
@@ -502,19 +489,6 @@ lemma iLipENorm_holderApprox_le {z : X} {R t : ℝ} (ht : 0 < t) (h't : t ≤ 1)
 /-- The constant occurring in Proposition 2.0.5. -/
 def C2_0_5 (a : ℝ) : ℝ≥0 := 2 ^ (7 * a)
 
-section DivisionMonoid
-
-variable {α β : Type*} [TopologicalSpace α] [DivisionMonoid β]
-variable {f f' : α → β}
-
-/- PR after HasCompactMulSupport.inv' -/
-
-@[to_additive]
-theorem HasCompactMulSupport.div (hf : HasCompactMulSupport f) (hf' : HasCompactMulSupport f') :
-    HasCompactMulSupport (f / f') := hf.comp₂_left hf' (div_one 1)
-
-end DivisionMonoid
-
 --NOTE (MI) : there was a missing minus sign in the exponent.
 /-- Proposition 2.0.5. -/
 theorem holder_van_der_corput {z : X} {R : ℝ} {ϕ : X → ℂ}

Carleson/Operators.lean

@@ -36,7 +36,9 @@ def carlesonOn (p : 𝔓 X) (f : X → ℂ) : X → ℂ :=
   indicator (E p)
     fun x ↦ ∫ y, exp (I * (Q x y - Q x x)) * K x y * ψ (D ^ (- 𝔰 p) * dist x y) * f y
 
--- not used anywhere and deprecated for `AEStronglyMeasurable.carlesonOn`
+/- Deprecated for `AEStronglyMeasurable.carlesonOn`
+Used through `measurable_carlesonSum` in `Antichain.AntichainOperator` and `ForestOperator.Forests`
+with nontrivial rework in order to move from `Measurable` to `AEStronglyMeasurable`. -/
 lemma measurable_carlesonOn {p : 𝔓 X} {f : X → ℂ} (measf : Measurable f) :
     Measurable (carlesonOn p f) := by
   refine (StronglyMeasurable.integral_prod_right ?_).measurable.indicator measurableSet_E
@@ -230,7 +232,6 @@ variable [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q D κ
 /-- The definition of `Tₚ*g(x)`, defined above Lemma 7.4.1 -/
 def adjointCarleson (p : 𝔓 X) (f : X → ℂ) (x : X) : ℂ :=
   ∫ y in E p, conj (Ks (𝔰 p) y x) * exp (.I * (Q y y - Q y x)) * f y
-  -- todo: consider changing to `(E p).indicator 1 y`
 
 open scoped Classical in
 /-- The definition of `T_ℭ*g(x)`, defined at the bottom of Section 7.4 -/
@@ -461,15 +462,6 @@ lemma adjointCarlesonSum_adjoint
       exact hg.adjointCarleson.conj
     _ = _ := by congr!; rw [← Finset.sum_mul, ← map_sum]; rfl
 
-/- XXX: this version is not used, and may not be useful in general
-lemma integrable_adjointCarlesonSum' (u : 𝔓 X) {f : X → ℂ} (hf : AEStronglyMeasurable f volume)
-    (hf' : IsBounded (range f)) (hf'' : HasCompactSupport f) :
-    Integrable (adjointCarlesonSum (t.𝔗 u) f ·) := by
-  obtain ⟨M, hM⟩ := hf'.exists_norm_le
-  have : BoundedCompactSupport f :=
-    ⟨memLp_top_of_bound hf M <| by filter_upwards with x using hM _ (mem_range_self x), hf''⟩
-  exact integrable_finset_sum _ fun i hi ↦ this.adjointCarleson (p := i).integrable -/
-
 lemma integrable_adjointCarlesonSum (s : Set (𝔓 X)) {f : X → ℂ} (hf : BoundedCompactSupport f) :
     Integrable (adjointCarlesonSum s f ·) :=
   integrable_finset_sum _ fun i _ ↦ hf.adjointCarleson (p := i).integrable