Antichain operator

theorem antichain_operator' {A : Set X} (h𝔄 : IsAntichain (· ≤ ·) 𝔄)    (hf : Measurable f) (hfF : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hA : A ⊆ G) :    ∫⁻ x in A, ‖carlesonSum 𝔄 f x‖ₑ ≤    C2_0_3 a nnq * dens₁ 𝔄 ^ ((q - 1) / (8 * a ^ 4)) * dens₂ 𝔄 ^ (q⁻¹ - 2⁻¹) *    eLpNorm f 2 volume * volume G ^ (1/2 : ℝ) := by  have I (x : ℝ) : x / x ≤ 1 := by    rcases eq_or_ne x 0 with rfl | hx    · simp    · simp [hx]  apply (lintegral_mono_set hA).trans  /- This follows from the other version by taking for the test function `g` the argument of  the sum to be controlled. -/  have bf := bcs_of_measurable_of_le_indicator_f hf hfF  rw [← enorm_integral_starRingEnd_mul_eq_lintegral_enorm bf.carlesonSum.restrict.integrable]  rw [← integral_indicator measurableSet_G]  simp_rw [indicator_mul_left, ← Function.comp_def,    Set.indicator_comp_of_zero (g := starRingEnd ℂ) (by simp)]  apply (antichain_operator h𝔄 hf hfF    (((measurable_carlesonSum hf).div (measurable_ofReal.comp (measurable_carlesonSum hf).norm)      ).indicator measurableSet_G)    (fun _ ↦ by simp [indicator]; split_ifs <;> simp [I])).trans  gcongr  calc  _ ≤ eLpNorm (G.indicator (fun x ↦ 1) : X → ℝ) 2 volume :=    eLpNorm_mono (fun x ↦ by simp only [indicator]; split_ifs <;> simp [I])  _ ≤ _ := by    rw [eLpNorm_indicator_const measurableSet_G (by norm_num) (by norm_num)]    simp