prove adjoint_tree_control

Carleson/Classical/CarlesonOnTheRealLine.lean

@@ -559,6 +559,9 @@ instance isTwoSidedKernelHilbert : IsTwoSidedKernel 4 K where
 
 /- This verifies the assumption on the operators T_r in two-sided metric space Carleson.
    Its proof is done in Section 11.3 (The truncated Hilbert transform) and is yet to be formalized.
+
+   Note: we can simplify the proof in the blueprint by using real interpolation
+   `MeasureTheory.exists_hasStrongType_real_interpolation`.
 -/
 lemma Hilbert_strong_2_2 : ∀ r > 0, HasBoundedStrongType (CZOperator K r) 2 2 volume volume (C_Ts 4) := sorry
 

Carleson/Defs.lean

@@ -233,6 +233,10 @@ class IsOneSidedKernel (a : outParam ℕ) (K : X → X → ℂ) : Prop where
 
 export IsOneSidedKernel (measurable_K_right measurable_K_left norm_K_le_vol_inv norm_K_sub_le)
 
+lemma MeasureTheory.aestronglyMeasurable_K [IsOneSidedKernel a K] :
+    AEStronglyMeasurable (fun x : X × X ↦ K x.1 x.2) :=
+  sorry -- this probably needs to be replaced in the definition of 1-sided kernel.
+
 /-- `K` is a two-sided Calderon-Zygmund kernel
 In the formalization `K x y` is defined everywhere, even for `x = y`. The assumptions on `K` show
 that `K x x = 0`. -/
@@ -323,6 +327,7 @@ lemma ballsCoverBalls_iterate {x : X} {d R r : ℝ} (hR : 0 < R) (hr : 0 < r) :
 
 end Iterate
 
+@[fun_prop]
 lemma measurable_Q₂ : Measurable fun p : X × X ↦ Q p.1 p.2 := fun s meass ↦ by
   have : (fun p : X × X ↦ (Q p.1) p.2) ⁻¹' s = ⋃ θ ∈ Q.range, (Q ⁻¹' {θ}) ×ˢ (θ ⁻¹' s) := by
     ext ⟨x, y⟩
@@ -335,6 +340,10 @@ lemma measurable_Q₂ : Measurable fun p : X × X ↦ Q p.1 p.2 := fun s meass 
   exact Q.range.measurableSet_biUnion fun θ _ ↦
     (Q.measurableSet_fiber θ).prod (meass.preimage (map_continuous θ).measurable)
 
+@[fun_prop]
+lemma aestronglyMeasurable_Q₂ : AEStronglyMeasurable fun p : X × X ↦ Q p.1 p.2 :=
+  measurable_Q₂.aestronglyMeasurable
+
 variable (X) in
 lemma S_spec [PreProofData a q K σ₁ σ₂ F G] : ∃ n : ℕ, ∀ x, -n ≤ σ₁ x ∧ σ₂ x ≤ n := sorry
 

Carleson/Psi.lean

@@ -641,6 +641,11 @@ lemma norm_Ks_sub_Ks_le {s : ℤ} {x y y' : X} (hK : Ks s x y ≠ 0) :
   · exact norm_Ks_sub_Ks_le₀ hK h
   · exact norm_Ks_sub_Ks_le₁ hK h
 
+lemma aestronglyMeasurable_Ks {s : ℤ} : AEStronglyMeasurable (fun x : X × X ↦ Ks s x.1 x.2) := by
+  unfold Ks _root_.ψ
+  refine aestronglyMeasurable_K.mul ?_
+  fun_prop
+
 /-- The function `y ↦ Ks s x y` is integrable. -/
 lemma integrable_Ks_x {s : ℤ} {x : X} (hD : 1 < (D : ℝ)) : Integrable (Ks s x) := by
   /- Define a measurable, bounded function `K₀` that is equal to `K x` on the support of

Carleson/TileStructure.lean

@@ -321,6 +321,33 @@ lemma isAntichain_iff_disjoint (𝔄 : Set (𝔓 X)) :
     ∀ p p', p ∈ 𝔄 → p' ∈ 𝔄 → p ≠ p' →
     Disjoint (toTileLike (X := X) p).toTile (toTileLike p').toTile := sorry
 
+lemma ENNReal.rpow_le_rpow_of_nonpos {x y : ℝ≥0∞} {z : ℝ} (hz : z ≤ 0) (h : x ≤ y) :
+    y ^ z ≤ x ^ z := by
+  rw [← neg_neg z, rpow_neg y, rpow_neg x, ← inv_rpow, ← inv_rpow]
+  exact rpow_le_rpow (ENNReal.inv_le_inv.mpr h) (neg_nonneg.mpr hz)
+
+/- A rough estimate. It's also less than 2 ^ (-a) -/
+def dens₁_le_one {𝔓' : Set (𝔓 X)} : dens₁ 𝔓' ≤ 1 := by
+  conv_rhs => rw [← mul_one 1]
+  simp only [dens₁, mem_lowerClosure, iSup_exists, iSup_le_iff]
+  intros i _ j hj
+  gcongr
+  · calc
+    (j : ℝ≥0∞) ^ (-(a : ℝ)) ≤ 2 ^ (-(a : ℝ)) := by
+      apply ENNReal.rpow_le_rpow_of_nonpos
+      · simp_rw [neg_nonpos, Nat.cast_nonneg']
+      exact_mod_cast hj
+    _ ≤ 2 ^ (0 : ℝ) :=
+      ENNReal.rpow_le_rpow_of_exponent_le (by norm_num) (neg_nonpos.mpr (Nat.cast_nonneg' _))
+    _ = 1 := by norm_num
+  simp only [iSup_le_iff, and_imp]
+  intros i' _ _ _ _
+  calc
+  volume (E₂ j i') / volume (𝓘 i' : Set X) ≤ volume (𝓘 i' : Set X) / volume (𝓘 i' : Set X) := by
+    gcongr
+    apply E₂_subset
+  _ ≤ 1 := ENNReal.div_self_le_one
+
 /-! ### Stack sizes -/
 
 variable {C C' : Set (𝔓 X)} {x x' : X}

Carleson/ToMathlib/Misc.lean

@@ -208,6 +208,11 @@ namespace MeasureTheory
 variable {α : Type*} {m : MeasurableSpace α} {μ : Measure α} {s : Set α}
   {F : Type*} [NormedAddCommGroup F]
 
+attribute [fun_prop] Continuous.comp_aestronglyMeasurable
+  AEStronglyMeasurable.mul AEStronglyMeasurable.prod_mk
+attribute [gcongr] Measure.AbsolutelyContinuous.prod -- todo: also add one-sided versions for gcongr
+
+
 theorem AEStronglyMeasurable.ennreal_toReal {u : α → ℝ≥0∞} (hu : AEStronglyMeasurable u μ) :
     AEStronglyMeasurable (fun x ↦ (u x).toReal) μ := by
   refine aestronglyMeasurable_iff_aemeasurable.mpr ?_
@@ -235,8 +240,26 @@ theorem eLpNormEssSup_lt_top_of_ae_ennnorm_bound {f : α → F} {C : ℝ≥0∞}
 lemma ENNReal.nnorm_toReal {x : ℝ≥0∞} : ‖x.toReal‖₊ = x.toNNReal := by
   ext; simp [ENNReal.toReal]
 
+theorem restrict_absolutelyContinuous : μ.restrict s ≪ μ :=
+  fun s hs ↦ Measure.restrict_le_self s |>.trans hs.le |>.antisymm <| zero_le _
+
 end MeasureTheory
 
+section
+
+open MeasureTheory Bornology
+variable {E X : Type*} {p : ℝ≥0∞} [NormedAddCommGroup E] [TopologicalSpace X] [MeasurableSpace X]
+  {μ : Measure X} [IsFiniteMeasureOnCompacts μ]
+
+lemma _root_.HasCompactSupport.memℒp_of_isBounded {f : X → E} (hf : HasCompactSupport f)
+    (h2f : IsBounded (range f))
+    (h3f : AEStronglyMeasurable f μ) {p : ℝ≥0∞} : Memℒp f p μ := by
+  obtain ⟨C, hC⟩ := h2f.exists_norm_le
+  simp only [mem_range, forall_exists_index, forall_apply_eq_imp_iff] at hC
+  exact hf.memℒp_of_bound h3f C <| .of_forall hC
+
+end
+
 /-! ## `EquivalenceOn` -/
 
 /-- An equivalence relation on the set `s`. -/

blueprint/src/chapter/main.tex

@@ -5030,6 +5030,7 @@ \section{Almost orthogonality of separated trees}
 \end{lemma}
 
 \begin{proof}
+    \leanok
     This follows immediately from Minkowski's inequality, \Cref{Hardy-Littlewood} and \Cref{adjoint-tree-estimate}, using that $a \ge 4$.
 \end{proof}