TileStructure.Forest.row_bound_common

lemma row_bound_common (hg : BoundedCompactSupport g) {A : Set X} (mA : MeasurableSet A) {C : ℝ≥0∞}    (hC : ∀ u ∈ t.rowDecomp j,      eLpNorm (A.indicator (adjointCarlesonSum (t u) ((𝓘 u : Set X).indicator g))) 2 ≤      C * eLpNorm ((𝓘 u : Set X).indicator g) 2) :    eLpNorm (A.indicator (adjointCarlesonRowSum t j g)) 2 ≤ C * eLpNorm g 2 := by  rw [← ENNReal.rpow_le_rpow_iff (show (0 : ℝ) < (2 : ℕ) by norm_num),    ENNReal.rpow_natCast, ENNReal.rpow_natCast]  let T (u : 𝔓 X) := adjointCarlesonSum (t u) ((𝓘 u : Set X).indicator g)  have bcsT (u : 𝔓 X) : BoundedCompactSupport (T u) :=    (hg.indicator coeGrid_measurable).adjointCarlesonSum  let AT (u : 𝔓 X) := (𝓘 u : Set X).indicator (A.indicator (T u))  have bcsAT (u : 𝔓 X) : BoundedCompactSupport (AT u) :=    ((bcsT u).indicator mA).indicator coeGrid_measurable  classical  calc    _ = eLpNorm (A.indicator (fun x ↦ ∑ u with u ∈ t.rowDecomp j,        (𝓘 u : Set X).indicator (T u) x)) 2 ^ 2 := by      unfold adjointCarlesonRowSum; congr! 5 with x u mu      rw [Finset.mem_filter_univ] at mu      rw [adjoint_tile_support2_sum (mem_forest_of_mem mu)]    _ = eLpNorm (∑ u with u ∈ t.rowDecomp j, AT u) 2 ^ 2 := by      simp_rw [← Finset.sum_apply, Finset.indicator_sum]; congr! 3 with u mu      rw [indicator_indicator, inter_comm, ← indicator_indicator]    _ ≤ ∑ u with u ∈ t.rowDecomp j, eLpNorm (AT u) 2 ^ 2 +        ∑ u with u ∈ t.rowDecomp j, ∑ v ∈ {v | v ∈ t.rowDecomp j} with u ≠ v,          ‖∫ x, AT u x * conj (AT v x)‖ₑ := by      convert BoundedCompactSupport.sq_eLpNorm_le_sums (s := {u | u ∈ t.rowDecomp j}) bcsAT with x      rw [Finset.sum_apply]    _ = ∑ u with u ∈ t.rowDecomp j, eLpNorm (AT u) 2 ^ 2 := by      conv_rhs => rw [← add_zero (Finset.sum ..)]      congr 1; refine Finset.sum_eq_zero fun u mu ↦ Finset.sum_eq_zero fun v mv ↦ ?_      rw [enorm_eq_zero]; refine integral_eq_zero_of_ae (.of_forall fun x ↦ ?_)      rw [Finset.mem_filter] at mv; obtain ⟨mv, hn⟩ := mv; rw [Finset.mem_filter_univ] at mu mv      have : (𝓘 u : Set X) ∩ (𝓘 v) = ∅ := (t.rowDecomp_𝔘_pairwiseDisjoint j mu mv hn).inter_eq      simp_rw [AT, indicator_indicator, conj_indicator, ← inter_indicator_mul]      rw [inter_inter_inter_comm, this, empty_inter, indicator_empty, Pi.zero_apply]    _ ≤ ∑ u with u ∈ t.rowDecomp j, eLpNorm (A.indicator (T u)) 2 ^ 2 := by      gcongr with u mu; exact eLpNorm_indicator_le _    _ ≤ ∑ u with u ∈ t.rowDecomp j, (C * eLpNorm ((𝓘 u : Set X).indicator g) 2) ^ 2 := by      gcongr with u mu; rw [Finset.mem_filter_univ] at mu; exact hC u mu    _ ≤ _ := by      simp_rw [mul_pow, ← Finset.mul_sum]; gcongr      apply sum_sq_eLpNorm_indicator_le_of_pairwiseDisjoint fun _ ↦ coeGrid_measurable      convert rowDecomp_𝔘_pairwiseDisjoint t j      rw [Finset.coe_filter_univ]; rfl