TileStructure.Forest.density_tree_bound2

lemma density_tree_bound2    (hf : BoundedCompactSupport f) (h2f : support f ⊆ F)    (hg : BoundedCompactSupport g) (h2g : support g ⊆ G) (hu : u ∈ t) :    ‖∫ x, conj (g x) * carlesonSum (t u) f x‖ₑ ≤    C7_3_1_2 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * dens₂ (t u) ^ (2 : ℝ)⁻¹ *    eLpNorm f 2 volume * eLpNorm g 2 volume := by  have hc : eLpNorm (approxOnCube (𝓙 (t u)) (‖f ·‖)) 2 volume ≤      (C7_3_3 a * dens₂ (t u)) ^ (2 : ℝ)⁻¹ * eLpNorm f 2 volume := by    have h2f : ∀ x ∉ F, f x = 0 := fun x hx ↦ notMem_support.mp <| hx ∘ (h2f ·)    have : ∀ J ∈ 𝓙 (t u), volume (J ∩ F) ≤ C7_3_3 a * dens₂ (t u) * volume (J : Set X) :=      fun J hJ ↦ by rw [inter_comm]; apply local_dens2_tree_bound hu hJ    exact eLpNorm_approxOnCube_two_le pairwiseDisjoint_𝓙 measurableSet_F this hf h2f  apply le_trans (density_tree_bound_aux hf hg h2g hu hc)  rw [ENNReal.mul_rpow_of_nonneg _ _ (inv_pos_of_pos two_pos).le]  calc    _ = (C7_3_1_1 a) * (C7_3_3 a) ^ (2 : ℝ)⁻¹ * dens₁ ((fun x ↦ t.𝔗 x) u) ^ (2 : ℝ)⁻¹ *          dens₂ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm f 2 volume * eLpNorm g 2 volume := by ring    _ ≤ C7_3_1_2 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * dens₂ (t u) ^ (2 : ℝ)⁻¹ *        eLpNorm f 2 volume * eLpNorm g 2 volume := by      rw [C7_3_1_1, C7_3_1_2, C7_3_3, ENNReal.rpow_ofNNReal (inv_pos.mpr two_pos).le,        ← ENNReal.coe_mul, ← NNReal.rpow_mul, ← NNReal.rpow_natCast,        ← NNReal.rpow_add two_pos.ne.symm, ← NNReal.rpow_natCast,        ENNReal.coe_rpow_of_nonneg _ (by positivity), ENNReal.coe_rpow_of_nonneg _ (by positivity)]      gcongr      · norm_num      rw [← mul_le_mul_iff_left₀ zero_lt_two]      simp only [add_mul, Nat.cast_add, Nat.cast_mul, Nat.cast_pow, Nat.cast_ofNat, mul_assoc,        one_mul]      simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, inv_mul_cancel₀, mul_one]      norm_cast      ring_nf      gcongr      norm_num