TileStructure.Forest.tree_projection_estimate

lemma tree_projection_estimate    (hf : BoundedCompactSupport f) (hg : BoundedCompactSupport g) (hu : u ∈ t) :    ‖∫ x, conj (g x) * carlesonSum (t u) f x‖ₑ ≤    C7_2_1 a * eLpNorm (approxOnCube (𝓙 (t u)) (‖f ·‖)) 2 volume *    eLpNorm (approxOnCube (𝓛 (t u)) (‖g ·‖)) 2 volume := by  classical  set aOC := approxOnCube (𝓛 (t u)) (‖g ·‖)  let eaOC (x : X) := ENNReal.ofReal (aOC x)  have aOC_nonneg {x : X} : 0 ≤ aOC x := approxOnCube_nonneg (fun _ ↦ norm_nonneg _)  calc ‖∫ x, conj (g x) * carlesonSum (t u) f x‖ₑ    _ ≤ ∫⁻ x, ‖conj (g x) * carlesonSum (t u) f x‖ₑ := enorm_integral_le_lintegral_enorm _    _ = ∫⁻ x in (⋃ p ∈ t u, 𝓘 p), ‖g x‖ₑ * ‖carlesonSum (t u) f x‖ₑ := by      rw [← lintegral_indicator]; swap      · exact MeasurableSet.biUnion (t u).to_countable (fun _ _ ↦ coeGrid_measurable)      simp_rw [enorm_mul, RCLike.enorm_conj]      refine lintegral_congr (fun x ↦ ?_)      by_cases hx : x ∈ ⋃ p ∈ t u, 𝓘 p      · rw [indicator_of_mem hx]      · simp only [notMem_support.mp (hx <| support_carlesonSum_subset ·), enorm_zero, mul_zero, indicator_of_notMem hx]    _ ≤ ∫⁻ x in (⋃ L ∈ 𝓛 (t u), (L : Set X)), ‖g x‖ₑ * ‖carlesonSum (t u) f x‖ₑ := by      rw [biUnion_𝓛]      refine lintegral_mono_set (fun x hx ↦ ?_)      have ⟨p, hp⟩ : ∃ p ∈ t u, x ∈ 𝓘 p := by simpa using! hx      apply mem_iUnion.mpr ⟨𝓘 p, hp.2⟩    _ = ∑ L ∈ 𝓛 (t u), ∫⁻ x in L, ‖g x‖ₑ * ‖carlesonSum (t u) f x‖ₑ := by      simp only [← mem_toFinset]      refine lintegral_biUnion_finset ?_ (fun _ _ ↦ coeGrid_measurable) _      rw [coe_toFinset]      exact pairwiseDisjoint_𝓛    _ ≤ ∑ L ∈ 𝓛 (t u), ∫⁻ x in L, ‖g x‖ₑ * (⨅ x' ∈ L, ‖cS_bound t u f x'‖ₑ) := by      gcongr ∑ L ∈ 𝓛 (t u), ?_ with L hL      refine setLIntegral_mono_ae (hg.restrict.aestronglyMeasurable.enorm.mul_const _)        (.of_forall fun x hx ↦ ?_)      gcongr      refine le_iInf₂ fun x' hx' ↦ ?_      simp only [mem_toFinset] at hL      convert! pointwise_tree_estimate hu hL hx hx' (boundedCompactSupport_eI𝒬u_mul u hf) using 1      · congr        simp_rw [mul_neg, eI𝒬u_mul, ← mul_assoc, ← exp_add, neg_add_cancel, exp_zero, one_mul]      · simp only [cS_bound, enorm_eq_self, norm_eI𝒬u_mul_eq u f]    _ = ∑ L ∈ 𝓛 (t u), ∫⁻ x in L, eaOC x * (⨅ x' ∈ L, ‖cS_bound t u f x'‖ₑ) := by      refine Finset.sum_congr rfl (fun L hL ↦ ?_)      rw [lintegral_mul_const'', lintegral_mul_const]; rotate_left      · exact ENNReal.measurable_ofReal.comp (stronglyMeasurable_approxOnCube _ _).measurable      · exact hg.restrict.aestronglyMeasurable.enorm      rw [lintegral_eq_lintegral_approxOnCube pairwiseDisjoint_𝓛 (mem_toFinset.mp hL) hg]      simp_rw [eaOC, ← Real.enorm_eq_ofReal aOC_nonneg, approxOnCube_ofReal, aOC,        Complex.enorm_real]    _ ≤ ∑ L ∈ 𝓛 (t u), ∫⁻ x in L, eaOC x * ‖cS_bound t u f x‖ₑ :=      Finset.sum_le_sum fun L hL ↦        setLIntegral_mono' coeGrid_measurable (fun x hx ↦ mul_right_mono (biInf_le _ hx))    _ = ∫⁻ x in (⋃ L ∈ 𝓛 (t u), (L : Set X)), eaOC x * ‖cS_bound t u f x‖ₑ := by      rw [← lintegral_biUnion_finset (hm := fun _ _ ↦ coeGrid_measurable)]      · simp only [mem_toFinset]      · simpa only [coe_toFinset] using pairwiseDisjoint_𝓛 (𝔖 := t u)    _ ≤ ∫⁻ (x : X), eaOC x * ‖cS_bound t u f x‖ₑ := by      nth_rewrite 2 [← setLIntegral_univ]      exact lintegral_mono_set (fun _ _ ↦ trivial)    _ ≤ eLpNorm eaOC 2 volume * eLpNorm (cS_bound t u f) 2 volume := by      have isConj : Real.HolderConjugate 2 2 := by constructor <;> norm_num      have : AEMeasurable eaOC := (stronglyMeasurable_approxOnCube _ _).aemeasurable.ennreal_ofReal      convert! ENNReal.lintegral_mul_le_Lp_mul_Lq volume isConj this aeMeasurable_cS_bound <;>        simp [eLpNorm, eLpNorm']    _ = eLpNorm (cS_bound t u f) 2 volume * eLpNorm aOC 2 volume := by      rw [mul_comm]; congr; ext; exact (Real.enorm_eq_ofReal aOC_nonneg).symm    _ ≤ _ := mul_left_mono eLpNorm_two_cS_bound_le