TileStructure.Forest.row_bound

lemma row_bound (hg : BoundedCompactSupport g) (h2g : support g ⊆ G) :    eLpNorm (adjointCarlesonRowSum t j g) 2 volume ≤ C7_7_2_1 a n * eLpNorm g 2 volume := by  rw [← indicator_univ (t.adjointCarlesonRowSum j g)]  refine row_bound_common hg MeasurableSet.univ fun u mu ↦ ?_  rw [indicator_univ]  calc    _ ≤ C7_3_1_1 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm ((𝓘 u : Set X).indicator g) 2 := by      apply adjoint_tree_estimate (hg.indicator coeGrid_measurable)      · rw [support_indicator]; exact inter_subset_right.trans h2g      · exact mem_forest_of_mem mu    _ ≤ C7_3_1_1 a * (2 ^ (4 * (a : ℝ) - n + 1)) ^ (2 : ℝ)⁻¹ *        eLpNorm ((𝓘 u : Set X).indicator g) 2 := by      gcongr; exact t.dens₁_𝔗_le (mem_forest_of_mem mu)    _ ≤ _ := by      gcongr      rw [show (2 : ℝ≥0∞) = (2 : ℝ≥0) by rfl, ← ENNReal.coe_rpow_of_ne_zero two_ne_zero,        ← ENNReal.coe_rpow_of_nonneg _ (by norm_num), ← ENNReal.coe_mul, ENNReal.coe_le_coe]      exact le_C7_7_2_1 (four_le_a X)