TileStructure.Forest.indicator_row_bound

lemma indicator_row_bound (hg : BoundedCompactSupport g) (h2g : support g ⊆ G) :    eLpNorm (F.indicator (adjointCarlesonRowSum t j g)) 2 volume ≤    C7_7_2_2 a n * dens₂ (⋃ u ∈ t, t u) ^ (2 : ℝ)⁻¹ * eLpNorm g 2 volume := by  refine row_bound_common hg measurableSet_F fun u mu ↦ ?_  calc    _ ≤ C7_3_1_2 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * dens₂ (t u) ^ (2 : ℝ)⁻¹ *        eLpNorm ((𝓘 u : Set X).indicator g) 2 := by      apply indicator_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_2 a * (2 ^ (4 * (a : ℝ) - n + 1)) ^ (2 : ℝ)⁻¹ * dens₂ (⋃ u ∈ t, t u) ^ (2 : ℝ)⁻¹ *        eLpNorm ((𝓘 u : Set X).indicator g) 2 := by      gcongr      · exact t.dens₁_𝔗_le (mem_forest_of_mem mu)      · exact iSup_le_iSup_of_subset (subset_biUnion_of_mem (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_2 (four_le_a X)