forest_operator

theorem forest_operator {n : ℕ} (𝔉 : Forest X n) {f g : X → ℂ}    (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x)    (hg : Measurable g) (h2g : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :    ‖∫ x, conj (g x) * ∑ u with u ∈ 𝔉, carlesonSum (𝔉 u) f x‖ₑ ≤    C2_0_4 a q n * (dens₂ (⋃ u ∈ 𝔉, 𝔉 u)) ^ (q⁻¹ - 2⁻¹) *    eLpNorm f 2 volume * eLpNorm g 2 volume := by  have g_part := 𝔉.forest_operator_g hf h2f hg h2g -- ^ (2 - 2 / q)  have f_part := 𝔉.forest_operator_f hf h2f hg h2g -- ^ (2 / q - 1)  rcases (q_le_two X).eq_or_lt with rfl | hq  · rw [sub_self, ENNReal.rpow_zero, mul_one, C2_0_4, C2_0_4_base]    rw [Forest.G2_0_4] at g_part; convert g_part using 6; ring  have egpos : 0 < 2 - 2 / q := by    rw [sub_pos]; nth_rw 2 [show 2 = (2 : ℝ) / 1 by norm_num]    exact div_lt_div_of_pos_left zero_lt_two zero_lt_one (one_lt_q X)  have efpos : 0 < 2 / q - 1 := by rwa [sub_pos, one_lt_div (zero_lt_one.trans (one_lt_q X))]  rw [← ENNReal.rpow_le_rpow_iff egpos] at g_part  rw [← ENNReal.rpow_le_rpow_iff efpos] at f_part  have key := mul_le_mul' g_part f_part  have esum : 2 - 2 / q + (2 / q - 1) = 1 := by ring  rw [← ENNReal.rpow_add_of_nonneg _ _ egpos.le efpos.le, esum, ENNReal.rpow_one, mul_assoc,    mul_assoc _ (eLpNorm f 2 volume), ENNReal.mul_rpow_of_nonneg _ _ egpos.le,    ENNReal.mul_rpow_of_nonneg _ _ efpos.le, mul_mul_mul_comm,    ← ENNReal.rpow_add_of_nonneg _ _ egpos.le efpos.le, esum, ENNReal.rpow_one, ← mul_assoc,    ENNReal.mul_rpow_of_nonneg _ _ efpos.le, ← mul_assoc, ← ENNReal.rpow_mul,    show 2⁻¹ * (2 / q - 1) = q⁻¹ - 2⁻¹ by ring] at key  apply key.trans; gcongr  calc    _ ≤ ((2 : ℝ≥0∞) ^ ((3 * 𝕔 + 15 + 5 * (𝕔 / 4)) * a ^ 3)) ^ (2 - 2 / q)        * (2 ^ (-(n / 2 : ℝ))) ^ (2 - 2 / q) *        (2 ^ ((3 * 𝕔 + 15 + 5 * (𝕔 / 4)) * a ^ 3)) ^ (2 / q - 1) := by      rw [Forest.G2_0_4, ENNReal.coe_mul, ENNReal.coe_pow, ENNReal.coe_rpow_of_ne_zero two_ne_zero,        Forest.C2_0_4_aux]      simp only [ENNReal.coe_ofNat]      rw [ENNReal.mul_rpow_of_nonneg _ _ egpos.le]      simp only [ENNReal.coe_pow, ENNReal.coe_ofNat]      gcongr _ * (2 ^ ?_) ^ _      · norm_num      have : 𝕔 / 2 ≤ 2 * (𝕔 / 4) + 1 := by lia      grw [this]      ring_nf      lia    _ = _ := by      rw [← mul_rotate, ← ENNReal.rpow_add_of_nonneg _ _ efpos.le egpos.le, add_comm (2/q - 1),        esum, ENNReal.rpow_one, ← ENNReal.rpow_mul, C2_0_4, C2_0_4_base, ENNReal.coe_mul,        ENNReal.coe_pow, ENNReal.coe_rpow_of_ne_zero two_ne_zero, neg_div,        show -(n / 2) * (2 - 2 / q) = -(1 - 1 / q) * n by ring]      congr; rw [sub_div, div_self (q_pos X).ne']