TileStructure.Forest.forest_operator_f_main

lemma forest_operator_f_main (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :    eLpNorm (fun x ↦ G.indicator (∑ u with u ∈ t, carlesonSum (t u) f ·) x) 2 volume ^ 2 ≤    (C2_0_4_aux a      * dens₂ (⋃ u ∈ t, t u) ^ (2 : ℝ)⁻¹ * eLpNorm f 2 volume) ^ 2 := by  have bf := bcs_of_measurable_of_le_indicator_f hf h2f  let TR (j : ℕ) (x : X) := G.indicator ((rowSupport t j).indicator (carlesonRowSum t j f)) x  have bcsTR (j : ℕ) : BoundedCompactSupport (TR j) :=    ((BoundedCompactSupport.finset_sum fun _ _ ↦ bf.carlesonSum).indicator      measurableSet_rowSupport).indicator measurableSet_G  calc    _ = eLpNorm (fun x ↦ G.indicator 1 x *        ∑ u with u ∈ t, carlesonSum (t u) f x) 2 volume ^ 2 := by      congr! 3 with x; rw [indicator_eq_indicator_one_mul]    _ = eLpNorm (fun x ↦ G.indicator 1 x *        ∑ j ∈ Finset.range (2 ^ n), carlesonRowSum t j f x) 2 volume ^ 2 := by      congr! with x      have dc : ({u | u ∈ t} : Finset _) =          (Finset.range (2 ^ n)).biUnion (fun j ↦ {u | u ∈ rowDecomp t j}) := by        rw [← Finset.toFinset_coe ({u | u ∈ t} : Finset _),          ← Finset.toFinset_coe (Finset.biUnion ..), toFinset_inj]        simp_rw [Finset.coe_biUnion, Finset.coe_range, mem_Iio, Finset.coe_filter_univ]        exact biUnion_rowDecomp.symm      rw [dc, Finset.sum_biUnion]; swap      · rw [Finset.coe_range]; intro j mj j' mj' hn        simp_rw [← Finset.disjoint_coe, Finset.coe_filter_univ]        exact pairwiseDisjoint_rowDecomp mj mj' hn      rfl    _ = eLpNorm (fun x ↦ ∑ j ∈ Finset.range (2 ^ n), TR j x) 2 ^ 2 := by      congr! 3 with x; rw [Finset.mul_sum]; congr! 2 with j mj      unfold TR; nth_rw 1 [carlesonRowSum_rowSupport, ← indicator_eq_indicator_one_mul]    _ ≤ ∑ j ∈ Finset.range (2 ^ n), eLpNorm (TR j) 2 ^ 2 +        ∑ j ∈ Finset.range (2 ^ n), ∑ j' ∈ Finset.range (2 ^ n) with j ≠ j',        ‖∫ x, TR j x * conj (TR j' x)‖ₑ := by      convert BoundedCompactSupport.sq_eLpNorm_le_sums bcsTR    _ = ∑ j ∈ Finset.range (2 ^ n), eLpNorm (TR j) 2 ^ 2 := by      conv_rhs => rw [← add_zero (Finset.sum ..)]      congr 1; refine Finset.sum_eq_zero fun j mj ↦ Finset.sum_eq_zero fun j' mj' ↦ ?_      rw [enorm_eq_zero]; refine integral_eq_zero_of_ae (.of_forall fun x ↦ ?_)      simp only [Finset.mem_filter, Finset.mem_range] at mj mj'      have : rowSupport t j ∩ rowSupport t j' = ∅ :=        (pairwiseDisjoint_rowSupport mj mj'.1 mj'.2).inter_eq      simp_rw [TR, indicator_indicator, conj_indicator, ← inter_indicator_mul]      rw [inter_inter_inter_comm, this, inter_empty, indicator_empty, Pi.zero_apply]    _ ≤ ∑ j ∈ Finset.range (2 ^ n), eLpNorm (G.indicator (carlesonRowSum t j f) ·) 2 ^ 2 := by      gcongr with j mj; refine eLpNorm_mono_enorm fun x ↦ ?_      unfold TR      rw [indicator_eq_indicator_one_mul, indicator_eq_indicator_one_mul (rowSupport t j),        ← mul_assoc, mul_comm (G.indicator 1 x), mul_assoc, ← indicator_eq_indicator_one_mul]      nth_rw 2 [← one_mul ‖_‖ₑ]; rw [enorm_mul]; gcongr      by_cases hx : x ∈ rowSupport t j      · simp [indicator_of_mem hx]      · simp [indicator_of_notMem hx]    _ ≤ ∑ j ∈ Finset.range (2 ^ n),        (C7_7_2_2 a n * dens₂ (⋃ u ∈ t, t u) ^ (2 : ℝ)⁻¹ * eLpNorm f 2) ^ 2 := by      gcongr with j      exact forest_operator_f_inner hf h2f    _ = _ := by      rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul, Nat.cast_pow, Nat.cast_ofNat,        ← ENNReal.rpow_natCast, ← div_mul_cancel₀ (n : ℝ) (show ((2 : ℕ) : ℝ) ≠ 0 by norm_num),        ENNReal.rpow_mul, ENNReal.rpow_natCast, ← mul_pow]      congr 1; simp_rw [← mul_assoc]      rw [C7_7_2_2, ENNReal.coe_mul, ENNReal.coe_rpow_of_ne_zero two_ne_zero, ENNReal.coe_ofNat,        mul_comm _ (2 ^ (-(n / 2 : ℝ))), ← mul_assoc,        ← ENNReal.rpow_add _ _ two_ne_zero ENNReal.ofNat_ne_top, Nat.cast_ofNat, ← sub_eq_add_neg]      simp only [sub_self, ENNReal.rpow_zero, ENNReal.coe_pow, ENNReal.coe_ofNat, one_mul,        C2_0_4_aux]