TileStructure.Forest.forest_operator_g_main

lemma forest_operator_g_main (hg : Measurable g) (h2g : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :    eLpNorm (∑ u with u ∈ t, adjointCarlesonSum (t u) g ·) 2 ^ 2 ≤    (G2_0_4 a n * eLpNorm g 2) ^ 2 := by  have bg := bcs_of_measurable_of_le_indicator_g hg h2g  let TR (j : ℕ) (x : X) := adjointCarlesonRowSum t j ((rowSupport t j).indicator g) x  have bcsrsi (j : ℕ) : BoundedCompactSupport ((t.rowSupport j).indicator g) volume :=    bg.indicator measurableSet_rowSupport  have bcsTR (j : ℕ) : BoundedCompactSupport (TR j) := by unfold TR adjointCarlesonRowSum; fun_prop  calc    _ = eLpNorm (∑ j ∈ Finset.range (2 ^ n), adjointCarlesonRowSum t j g ·) 2 ^ 2 := by      congr; ext 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 (∑ j ∈ Finset.range (2 ^ n), TR j ·) 2 ^ 2 := by      congr! 4 with x j mj; rw [adjointCarlesonRowSum_rowSupport]    _ ≤ ∑ 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), (C7_7_2_1 a n * eLpNorm ((rowSupport t j).indicator g) 2) ^ 2 +        ∑ j ∈ Finset.range (2 ^ n), ∑ j' ∈ Finset.range (2 ^ n) with j ≠ j',          C7_7_3 a n * eLpNorm ((rowSupport t j).indicator g) 2 *          eLpNorm ((rowSupport t j').indicator g) 2 := by      have nleg {j : ℕ} (x : X) : ‖(t.rowSupport j).indicator g x‖ ≤ G.indicator 1 x := by        by_cases mx : x ∈ t.rowSupport j        · rw [indicator_of_mem mx]; exact h2g x        · rw [indicator_of_notMem mx, norm_zero]; exact indicator_apply_nonneg fun _ ↦ by simp      gcongr with j mj j mj j' mj'      · simp_rw [Finset.mem_range] at mj        exact row_bound (bcsrsi j) (support_subset_of_norm_le_indicator nleg)      · simp_rw [Finset.mem_filter, Finset.mem_range] at mj mj'        exact row_correlation mj mj'.1 mj'.2 (bcsrsi j) (support_subset_of_norm_le_indicator nleg)          (bcsrsi j') (support_subset_of_norm_le_indicator nleg)    _ ≤ C7_7_2_1 a n ^ 2 *        ∑ j ∈ Finset.range (2 ^ n), eLpNorm ((rowSupport t j).indicator g) 2 ^ 2 +        C7_7_3 a n * ∑ j ∈ Finset.range (2 ^ n), ∑ j' ∈ Finset.range (2 ^ n),          eLpNorm ((rowSupport t j).indicator g) 2 *          eLpNorm ((rowSupport t j').indicator g) 2 := by      simp_rw [Finset.mul_sum, ← mul_pow, mul_assoc]      gcongr with j mj; exact Finset.filter_subset ..    _ ≤ C7_7_2_1 a n ^ 2 *        ∑ j ∈ Finset.range (2 ^ n), eLpNorm ((rowSupport t j).indicator g) 2 ^ 2 +        C7_7_3 a n * 2 ^ n *        ∑ j ∈ Finset.range (2 ^ n), eLpNorm ((rowSupport t j).indicator g) 2 ^ 2 := by      conv_lhs => enter [2, 2, 2, j]; rw [← Finset.mul_sum]      rw [← Finset.sum_mul, ← sq, mul_assoc]; gcongr      have := ENNReal.rpow_sum_le_const_mul_sum_rpow (Finset.range (2 ^ n))        (fun j ↦ eLpNorm ((t.rowSupport j).indicator g) 2 volume) one_le_two      simp_rw [show (2 : ℝ) - 1 = 1 by norm_num, ENNReal.rpow_one, Finset.card_range,        show (2 : ℝ) = (2 : ℕ) by rfl, ENNReal.rpow_natCast, Nat.cast_pow, Nat.cast_ofNat] at this      exact this    _ ≤ (C7_7_2_1 a n ^ 2 + C7_7_3 a n * 2 ^ n) * eLpNorm g 2 ^ 2 := by      rw [← add_mul]; gcongr      apply sum_sq_eLpNorm_indicator_le_of_pairwiseDisjoint fun _ ↦ measurableSet_rowSupport      rw [Finset.coe_range]; exact pairwiseDisjoint_rowSupport    _ ≤ _ := by      rw [mul_pow]; gcongr; norm_cast      rw [Nat.cast_pow, Nat.cast_ofNat]      exact le_sq_G2_0_4 (four_le_a X)