dens1_antichain

lemma dens1_antichain (h𝔄 : IsAntichain (· ≤ ·) 𝔄) (hf : Measurable f)    (hfF : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hg : Measurable g) (hgG : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :    ‖∫ x, conj (g x) * carlesonSum 𝔄 f x‖ₑ ≤      C6_1_4 a * dens₁ 𝔄 ^ (8 * a ^ 4 : ℝ)⁻¹ * eLpNorm f 2 volume * eLpNorm g 2 volume := by  have bf := bcs_of_measurable_of_le_indicator_f hf hfF  have bg := bcs_of_measurable_of_le_indicator_g hg hgG  calc    _ ≤ ∫⁻ x, ‖adjointCarlesonSum 𝔄 g x‖ₑ * ‖f x‖ₑ := by      rw [adjointCarlesonSum_adjoint bf bg]      conv_rhs => enter [2, x]; rw [← RCLike.enorm_conj, ← enorm_mul]      exact enorm_integral_le_lintegral_enorm _    _ ≤ eLpNorm (adjointCarlesonSum 𝔄 g) 2 * eLpNorm f 2 := by      conv_rhs => rw [← eLpNorm_enorm, ← eLpNorm_enorm]      exact ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm inferInstance        bg.adjointCarlesonSum.enorm.aestronglyMeasurable.aemeasurable        bf.enorm.aestronglyMeasurable.aemeasurable    _ ≤ _ := by      rw [← mul_rotate, mul_comm (eLpNorm g 2 volume)]; gcongr      grw [← ENNReal.rpow_le_rpow_iff (show (0 : ℝ) < (2 : ℕ) by norm_num),        ENNReal.rpow_natCast, ENNReal.rpow_natCast, dens1_antichain_sq h𝔄 hg hgG]