Antichain operator

theorem antichain_operator (h𝔄 : IsAntichain (· ≤ ·) 𝔄) (hf : Measurable f)    (hf1 : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hg : Measurable g) (hg1 : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :    ‖∫ x, conj (g x) * carlesonSum 𝔄 f x‖ₑ ≤      C2_0_3 a nnq * dens₁ 𝔄 ^ ((q - 1) / (8 * a ^ 4)) * dens₂ 𝔄 ^ (q⁻¹ - 2⁻¹) *        eLpNorm f 2 volume * eLpNorm g 2 volume := by  have hq : (nnq : ℝ) = q := rfl  have h21 : (2 : ℝ) - 1 = 1 := by norm_cast  have h21' : (2 : ℝ≥0) - 1 = 1 := by norm_cast  -- Eq. 6.1.47  have heq : (nnqt⁻¹ - 2⁻¹) * (2 - q) = q⁻¹ - 2⁻¹ := by    have hq0 : q ≠ 0 := by rw [← hq, NNReal.coe_ne_zero]; exact (nnq_pos _).ne'    simp only [inv_div, NNReal.coe_div, NNReal.coe_add, hq, NNReal.coe_one, NNReal.coe_mul,      NNReal.coe_ofNat]    calc      _ = ((q + 1) / (2 * q) - q / (2 * q)) * (2 - q) := by        congr; nth_rewrite 1 [inv_eq_one_div, ← one_mul q, mul_div_mul_right 1 2 hq0]; rfl      _ = q⁻¹ - 2⁻¹ := by ring_nf; simp [hq0]  push_cast at heq  by_cases hq2 : q = 2  · have hnnq2 : nnq = 2 := by simp only [← NNReal.coe_inj, NNReal.coe_ofNat, ← hq2]; rfl    simp only [hq2, h21, one_div, sub_self, ENNReal.rpow_zero, mul_one]    apply (dens1_antichain h𝔄 hf hf1 hg hg1).trans    gcongr    simp only [C6_1_4, C2_0_3, hnnq2, h21', div_one, le_refl]  · have hq2' : 0 < 2 - q :=      sub_pos.mpr (lt_of_le_of_ne (NNReal.coe_le_coe.mpr (nnq_mem_Ioc X).2) hq2)    -- Take the (2-q)-th power of 6.1.11    have h2 := dens2_antichain h𝔄 hf1 hf hg1 hg    rw [← ENNReal.rpow_le_rpow_iff hq2'] at h2    simp only [mul_assoc] at h2    rw [ENNReal.mul_rpow_of_nonneg _ _ hq2'.le, ENNReal.mul_rpow_of_nonneg _ _ hq2'.le,      ← ENNReal.rpow_mul (dens₂ 𝔄), heq] at h2    -- Take and the (q-1)-th power of 6.1.22    have h1 := dens1_antichain h𝔄 hf hf1 hg hg1    have h1q : 0 < q - 1 := sub_pos.mpr (NNReal.coe_lt_coe.mpr (nnq_mem_Ioc X).1)    rw [← ENNReal.rpow_le_rpow_iff h1q] at h1    simp only [mul_assoc] at h1    rw [ENNReal.mul_rpow_of_nonneg _ _ h1q.le, ENNReal.mul_rpow_of_nonneg _ _ h1q.le,      ← ENNReal.rpow_mul (dens₁ 𝔄)] at h1    calc      _ = ‖∫ x, conj (g x) * carlesonSum 𝔄 f x‖ₑ ^ (q - 1) *          ‖∫ x, conj (g x) * carlesonSum 𝔄 f x‖ₑ ^ (2 - q) := by        rw [← ENNReal.rpow_add_of_nonneg _ _ h1q.le hq2'.le, sub_add_sub_cancel', h21,          ENNReal.rpow_one]      _ ≤ (C6_1_4 a ^ (q - 1) * (dens₁ 𝔄 ^ ((8 * ↑a ^ 4)⁻¹ * (q - 1)) *            (eLpNorm f 2 volume * eLpNorm g 2 volume) ^ (q - 1))) *          (C6_1_3 a nnq ^ (2 - q) * (dens₂ 𝔄 ^ (q⁻¹ - 2⁻¹) *            (eLpNorm f 2 volume * eLpNorm g 2 volume) ^ (2 - q))) :=        mul_le_mul h1 h2 (by positivity) (by positivity)      _ = (C6_1_4 a ^ (q - 1) * C6_1_3 a nnq ^ (2 - q)) *            dens₁ 𝔄 ^ ((8 * ↑a ^ 4)⁻¹ * (q - 1)) * dens₂ 𝔄 ^ (q⁻¹ - 2⁻¹) *          ((eLpNorm f 2 volume * eLpNorm g 2 volume) ^ (q - 1) *            (eLpNorm f 2 volume * eLpNorm g 2 volume) ^ (2 - q)) := by ring      _ = (C6_1_4 a ^ (q - 1) * C6_1_3 a nnq ^ (2 - q)) *            dens₁ 𝔄 ^ ((q - 1) / (8 * ↑a ^ 4)) * dens₂ 𝔄 ^ (q⁻¹ - 2⁻¹) *          eLpNorm f 2 volume * eLpNorm g 2 volume := by        have hnorm : ((eLpNorm f 2 volume * eLpNorm g 2 volume) ^ (q - 1) *            (eLpNorm f 2 volume * eLpNorm g 2 volume) ^ (2 - q)) =            eLpNorm f 2 volume * eLpNorm g 2 volume := by          rw [← ENNReal.rpow_add_of_nonneg _ _ h1q.le hq2'.le, sub_add_sub_cancel', h21,            ENNReal.rpow_one]        rw [div_eq_inv_mul, hnorm]        ring      _ ≤ _ := by        gcongr        simp only [C6_1_4, C6_1_3, ENNReal.coe_mul, C2_0_3]        exact ineq_aux_2_0_3 X