maximal_bound_antichain

lemma maximal_bound_antichain {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ ·) 𝔄)    {f : X → ℂ} (hfm : Measurable f) (x : X) :    ‖carlesonSum 𝔄 f x‖ₑ ≤ (C6_1_2 a) * maximalFunction volume 𝔄 𝔠 (fun 𝔭 ↦ 8*D ^ 𝔰 𝔭) 1 f x := by  classical  by_cases hx : ∃ (p : 𝔄), carlesonOn p f x ≠ 0  · obtain ⟨p, hpx⟩ := hx    have hDpow_pos : 0 < (D : ℝ) ^ 𝔰 p.1 := defaultD_pow_pos ..    have h8Dpow_pos : 0 < 8 * (D : ℝ) ^ 𝔰 p.1 := mul_defaultD_pow_pos _ (by linarith) _    have hxE : x ∈ E ↑p := mem_of_indicator_ne_zero hpx    have hne_p : ∀ b ∈ ({p | p ∈ 𝔄} : Finset (𝔓 X)), b ≠ ↑p → carlesonOn b f x = 0 := by      intro p' hp' hpp'      rw [Finset.mem_filter_univ] at hp'      by_contra hp'x      exact hpp' (tile_disjointness h𝔄 hp' p.2 <|        not_disjoint_iff.mpr ⟨x, mem_of_indicator_ne_zero hp'x, hxE⟩)    have hdist_cp : dist x (𝔠 p) ≤ 4*D ^ 𝔰 p.1 := le_of_lt (mem_ball.mp (Grid_subset_ball hxE.1))    have hdist_y : ∀ {y : X} (hy : Ks (𝔰 p.1) x y ≠ 0),        dist x y ∈ Icc ((D ^ ((𝔰 p.1) - 1) : ℝ) / 4) (D ^ (𝔰 p.1) / 2) := fun hy ↦      dist_mem_Icc_of_Ks_ne_zero hy    -- Ineq. 6.1.5.    have hdist_cpy : ∀ (y : X), (Ks (𝔰 p.1) x y ≠ 0) → dist (𝔠 p) y < 8*D ^ 𝔰 p.1 := fun y hy ↦      calc dist (𝔠 p) y        ≤ dist (𝔠 p) x + dist x y := dist_triangle (𝔠 p.1) x y      _ ≤ 4*D ^ 𝔰 p.1 + dist x y := by simp only [add_le_add_iff_right, dist_comm, hdist_cp]      _ ≤ 4*D ^ 𝔰 p.1 + D ^ 𝔰 p.1 /2 := by        simp only [add_le_add_iff_left, (mem_Icc.mpr (hdist_y hy)).2]      _ < 8*D ^ 𝔰 p.1 := by        rw [div_eq_inv_mul, ← add_mul]        exact mul_lt_mul_of_pos_right (by norm_num) (defaultD_pow_pos ..)    calc    _ = ‖carlesonOn p f x‖ₑ := by        have hp : ↑p ∈ ({p | p ∈ 𝔄} : Finset (𝔓 X)) := by          simp only [Finset.mem_filter, Finset.mem_univ, Subtype.coe_prop, and_self]        rw [carlesonSum, Finset.sum_eq_single_of_mem p.1 hp hne_p]    _ ≤ ∫⁻ y, ‖exp (I * (Q x y - Q x x)) * Ks (𝔰 p.1) x y * f y‖ₑ := by        rw [carlesonOn, indicator, if_pos hxE]        exact le_trans (enorm_integral_le_lintegral_enorm _) (lintegral_mono fun z ↦ le_rfl)    _ ≤ ∫⁻ y, ‖Ks (𝔰 p.1) x y * f y‖ₑ := by      simp only [enorm_mul]      exact lintegral_mono fun y ↦ (by simp [← Complex.ofReal_sub])    _ = ∫⁻ y in ball (𝔠 p) (8 * D ^ 𝔰 p.1), ‖Ks (𝔰 p.1) x y * f y‖ₑ := by        rw [setLIntegral_eq_of_support_subset]        intro y hy        simp only [enorm_mul, Function.support_mul, mem_inter_iff, Function.mem_support, ne_eq,          enorm_eq_zero] at hy        rw [mem_ball, dist_comm]        exact hdist_cpy y hy.1    _ ≤ ∫⁻ y in ball (𝔠 p) (8 * D ^ 𝔰 p.1),        2 ^ (6 * a + (𝕔 + 1) * a ^ 3) / volume (ball (𝔠 p.1) (8 * D ^ 𝔰 p.1)) * ‖f y‖ₑ := by      refine lintegral_mono fun y ↦ ?_      rw [enorm_mul]; gcongr      by_cases hy : Ks (𝔰 p.1) x y = 0      · simp only [hy, enorm_zero, zero_le]      · exact norm_Ks_le' _ hxE hy -- Composition of ineq. 6.1.6, 6.1.7, 6.1.8    _ = 2 ^ (5 * a + (𝕔 + 1) * a ^ 3 + a) *        ⨍⁻ y in ball (𝔠 p.1) (8 * D ^ 𝔰 p.1), ‖f y‖ₑ ∂volume := by      rw [lintegral_const_mul _ hfm.enorm, ENNReal.mul_comm_div, setLAverage_eq]      congr 2; ring    _ ≤ C6_1_2 a * (ball (𝔠 p.1) (8 * D ^ 𝔰 p.1)).indicator (x := x)        (fun _ ↦ ⨍⁻ y in ball (𝔠 p.1) (8 * D ^ 𝔰 p.1), ‖f y‖ₑ ∂volume) := by      simp only [indicator, mem_ball, mul_ite, mul_zero]      rw [if_pos]      · gcongr        rw [C6_1_2, add_comm (5 * a), add_assoc]; norm_cast        apply pow_le_pow_right₀ one_le_two        ring_nf        suffices 6 * a ≤ a ^ 3 by lia        linarith [sixteen_times_le_cube (four_le_a X)]      · exact lt_of_le_of_lt hdist_cp          (mul_lt_mul_of_nonneg_of_pos (by linarith) (le_refl _) (by linarith) hDpow_pos)    _ ≤ C6_1_2 a * maximalFunction volume 𝔄 𝔠 (8 * D ^ 𝔰 ·) 1 f x := by      rw [ENNReal.mul_le_mul_iff_right (C6_1_2_ne_zero a) coe_ne_top, maximalFunction,        inv_one, le_iSup_iff]      simp only [iSup_le_iff, ENNReal.rpow_one]      exact (fun _ hc ↦ hc p.1 p.2)  · simp only [ne_eq, Subtype.exists, exists_prop, not_exists, not_and, not_not] at hx    have h0 : carlesonSum 𝔄 f x = 0 :=      Finset.sum_eq_zero (fun p hp ↦ hx p ((Finset.mem_filter_univ _).mp hp))    simp [h0]