TileStructure.Forest.btp_expansion

lemma btp_expansion (hf : BoundedCompactSupport f) :    eLpNorm (approxOnCube (𝓙₆ t u₁) (‖adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f ·‖)) 2 volume =    (∑ J ∈ (𝓙₆ t u₁).toFinset, (volume (J : Set X))⁻¹ *    (∫⁻ y in J, ‖adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f y‖ₑ) ^ 2) ^ (2 : ℝ)⁻¹ := by  have Vpos {J : Grid X} : 0 < volume (J : Set X) := volume_coeGrid_pos (defaultD_pos a)  have Vlt {J : Grid X} : volume (J : Set X) < ⊤ := volume_coeGrid_lt_top  calc    _ = (∫⁻ x, ∑ J ∈ (𝓙₆ t u₁).toFinset, (J : Set X).indicator (fun _ ↦        ‖⨍ y in J, ‖adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f y‖‖ₑ ^ 2) x) ^ (2 : ℝ)⁻¹ := by      unfold approxOnCube      simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ENNReal.ofNat_ne_top,        ENNReal.toReal_ofNat, one_div]      congr! with x; rw [ENNReal.enorm_sum_eq_sum_enorm]; swap      · refine fun J mJ ↦ indicator_nonneg (fun y my ↦ ?_) _        rw [average_eq, smul_eq_mul]        exact mul_nonneg (by positivity) (integral_nonneg fun _ ↦ norm_nonneg _)      rw [show (2 : ℝ) = (2 : ℕ) by rfl, ENNReal.rpow_natCast, filter_mem_univ_eq_toFinset]      simp_rw [enorm_indicator_eq_indicator_enorm, sum_𝓙₆_indicator_sq_eq]    _ = (∑ J ∈ (𝓙₆ t u₁).toFinset, ∫⁻ x in (J : Set X), (fun _ ↦        ‖⨍ y in J, ‖adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f y‖‖ₑ ^ 2) x) ^ (2 : ℝ)⁻¹ := by      congr 1; simp_rw [← lintegral_indicator coeGrid_measurable]      exact lintegral_finsetSum _ fun J mJ ↦ measurable_const.indicator coeGrid_measurable    _ = (∑ J ∈ (𝓙₆ t u₁).toFinset, ∫⁻ x in (J : Set X),        (⨍⁻ y in J, ‖adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f y‖ₑ ∂volume) ^ 2) ^ (2 : ℝ)⁻¹ := by      simp only [lintegral_const]; congr! with J mJ      have vn0 : volume.real (J : Set X) ≠ 0 := by        rw [measureReal_def, ENNReal.toReal_ne_zero]; exact ⟨Vpos.ne', Vlt.ne⟩      rw [setLAverage_eq, setAverage_eq, smul_eq_mul, enorm_mul, enorm_inv vn0,        ← ENNReal.div_eq_inv_mul, measureReal_def, Real.enorm_of_nonneg ENNReal.toReal_nonneg,        ENNReal.ofReal_toReal Vlt.ne]; congr      rw [integral_norm_eq_lintegral_enorm hf.aestronglyMeasurable.adjointCarlesonSum.restrict]      apply Real.enorm_toReal      rw [← lt_top_iff_ne_top, ← eLpNorm_one_eq_lintegral_enorm]      exact (hf.adjointCarlesonSum.restrict.memLp 1).2    _ = _ := by      congr! with J mJ      rw [setLIntegral_const, setLAverage_eq, ENNReal.div_eq_inv_mul, mul_pow, ← mul_rotate, sq,        ← mul_assoc, ENNReal.mul_inv_cancel Vpos.ne' Vlt.ne, one_mul]