dens2_antichain

lemma dens2_antichain {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ ·) 𝔄)    {f : X → ℂ} (hfF : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hf : Measurable f)    {g : X → ℂ} (hgG : ∀ x, ‖g x‖ ≤ G.indicator 1 x) (hg : Measurable g) :    ‖∫ x, ((starRingEnd ℂ) (g x)) * carlesonSum 𝔄 f x‖ₑ ≤      (C6_1_3 a nnq) * (dens₂ (𝔄 : Set (𝔓 X))) ^ ((nnqt : ℝ)⁻¹ - 2⁻¹) *        eLpNorm f 2 * eLpNorm g 2 := by  have bf := bcs_of_measurable_of_le_indicator_f hf hfF  have bg := bcs_of_measurable_of_le_indicator_g hg hgG  apply le_trans <| enorm_integral_le_lintegral_enorm _  simp_rw [enorm_mul]  let p' := ((qt X)⁻¹ - 2⁻¹)⁻¹  have hp'_inv : p'⁻¹ = 2⁻¹ * q⁻¹ := by simp only [p', inv_inv, qt, inv_nnqt_eq]; simp  have hpp : (p X).HolderConjugate p' := by    refine Real.holderConjugate_iff.mpr ⟨one_lt_p X, ?_⟩    rw [hp'_inv, inv_p_eq X, div_eq_mul_inv, inv_qt_eq]    ring  let C2_0_6' := C2_0_6 (defaultA a) (p X).toNNReal 2  have := eLpNorm_𝓜_le_eLpNorm_𝓜p_mul 𝔄 hf hfF hpp  have := eLpNorm_𝓜p_le 𝔄 <| bf.memLp 2  calc    _ ≤ eLpNorm g 2 * eLpNorm (carlesonSum 𝔄 f) 2 := by      simpa [RCLike.enorm_conj, ← eLpNorm_enorm] using lintegral_mul_le_eLpNorm_mul_eLqNorm        inferInstance bg.enorm.aestronglyMeasurable.aemeasurable          bf.carlesonSum.enorm.aestronglyMeasurable.aemeasurable    _ ≤ eLpNorm g 2 * (C6_1_2 a * eLpNorm (𝓜 𝔄 f) 2) := by      gcongr      exact eLpNorm_le_mul_eLpNorm_of_ae_le_mul'        (ae_of_all _ <| fun x ↦ maximal_bound_antichain h𝔄 hf x) 2    _ ≤ eLpNorm g 2 * (C6_1_2 a * ((dens₂ 𝔄) ^ (p'⁻¹) * eLpNorm (𝓜p 𝔄 (p X) f) 2)) := by gcongr    _ ≤ eLpNorm g 2 * (C6_1_2 a * ((dens₂ 𝔄) ^ (p'⁻¹) * (C2_0_6' * eLpNorm f 2))) := by gcongr    _ = (C6_1_2 a * C2_0_6') * (dens₂ 𝔄) ^ (p'⁻¹) * eLpNorm f 2 * eLpNorm g 2 := by ring    _ ≤ _ := by      gcongr ?_ * ?_ * eLpNorm f 2 _ * eLpNorm g 2 _      · exact_mod_cast const_check      · rw [hp'_inv, inv_nnqt_eq]; simp