lintegral_enorm_carlesonSum_le_of_isAntichain_subset_ℭ

lemma lintegral_enorm_carlesonSum_le_of_isAntichain_subset_ℭ    {f : X → ℂ} {𝔄 : Set (𝔓 X)} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (h'f : Measurable f)    (hA : IsAntichain (· ≤ ·) 𝔄) (h'A : 𝔄 ⊆ ℭ k n) :    ∫⁻ x in G \ G', ‖carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔄) f x‖ₑ    ≤ C2_0_3 a nnq * 2 ^ (a + 3) * volume G ^ (1 - q⁻¹) * volume F ^ (q⁻¹)      * 2 ^ (- ((q - 1) / (8 * a ^ 4) * n)) := by  have I : 0 ≤ q - 1 := by linarith [one_lt_q X]  have J : 0 ≤ q⁻¹ - 2⁻¹ := inv_q_sub_half_nonneg X  apply (antichain_operator_le_volume (hA.subset inter_subset_right) h'f hf sdiff_subset).trans  simp only [mul_assoc]  apply mul_le_mul_right  have : dens₁ (𝔓pos (X := X) ∩ 𝔓₁ᶜ ∩ 𝔄) ≤ 2 ^ (4 * a - n + 1 : ℝ) :=    dens1_le (inter_subset_right.trans h'A)  have : dens₂ (𝔓pos (X := X) ∩ 𝔓₁ᶜ ∩ 𝔄) ≤ 2 ^ (2 * a + 5) * volume F / volume G := by    rw [dens₂_eq_biSup_dens₂]    simp only [iSup_le_iff]    intro p hp    have : ¬ (𝓘 p : Set X) ⊆ G₁ := by      have W := hp.1.1      contrapose! W      have : ↑(𝓘 p) ∩ G ∩ G'ᶜ = ∅ := by        simp only [G', compl_union]        apply eq_empty_of_subset_empty        intro x hx        exact (hx.2.1.1 (W hx.1.1)).elim      simp only [𝔓pos, mem_setOf_eq, this, measure_empty, lt_self_iff_false, not_false_eq_true]    contrapose! this    have : p ∈ highDensityTiles := mem_preimage.mp this    apply subset_biUnion_of_mem this  calc  dens₁ (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔄) ^ ((q - 1) / (8 * ↑a ^ 4)) *    (dens₂ (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔄) ^ (q⁻¹ - 2⁻¹) * (volume F ^ (1 / 2 : ℝ) * volume G ^ (1 / 2 : ℝ)))  _ ≤ (2 ^ (4 * a - n + 1 : ℝ)) ^ ((q - 1) / (8 * ↑a ^ 4)) *    ((2 ^ (2 * a + 5) * volume F / volume G) ^ (q⁻¹ - 2⁻¹)      * ((volume F ^ (1 / 2 : ℝ) * volume G ^ (1 / 2 : ℝ)))) := by gcongr  _ = (2 ^ ((4 * a + 1) * (q - 1) / (8 * ↑a ^ 4)) * 2 ^ (- ((q - 1) / (8 * ↑a ^ 4) * n))) *    ((2 ^ ((2 * a + 5) * (q⁻¹ - 2⁻¹)) * volume F ^ (q⁻¹ - 2⁻¹) / volume G ^ (q⁻¹ - 2⁻¹))      * ((volume F ^ (1 / 2 : ℝ) * volume G ^ (1 / 2 : ℝ)))) := by    rw [ENNReal.div_rpow_of_nonneg _ _ J, ENNReal.mul_rpow_of_nonneg _ _ J,      ← ENNReal.rpow_natCast, ← ENNReal.rpow_mul, ← ENNReal.rpow_mul,      ← ENNReal.rpow_add _ _ (NeZero.ne 2) ENNReal.ofNat_ne_top]    congr    · ring    · simp  _ = 2 ^ ((4 * a + 1) * (q - 1) / (8 * ↑a ^ 4)) * 2 ^ ((2 * a + 5) * (q⁻¹ - 2⁻¹)) *      (volume G ^ (1 - q⁻¹) * (volume F ^ q⁻¹ * 2 ^ (- ((q - 1) / (8 * ↑a ^ 4) * n)))) := by    rcases eq_or_ne (volume G) 0 with vG | vG    · have : 0 < 1 - q⁻¹ := by rw [sub_pos, inv_lt_one_iff₀]; exact .inr (one_lt_q X)      rw [vG, ENNReal.zero_rpow_of_pos (show 0 < (1 / 2 : ℝ) by positivity),        ENNReal.zero_rpow_of_pos this]      simp only [zero_mul, mul_zero]    · have IF : (volume F) ^ (q⁻¹) = (volume F) ^ ((q ⁻¹ - 2⁻¹) + 2⁻¹) := by congr; abel      have IG : (volume G) ^ (1 - q⁻¹) = (volume G) ^ (2⁻¹ - (q⁻¹ - 2⁻¹)) := by        congr 1        simp only [sub_sub_eq_add_sub, sub_left_inj]        norm_num      rw [IF, IG, ENNReal.rpow_sub (2⁻¹) _ vG volume_G_ne_top,        ENNReal.rpow_add_of_nonneg (x := volume F) _ _ (inv_q_sub_half_nonneg X) (by norm_num),        ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul]      ring_nf  _ ≤ 2 ^ ((2 : ℝ)⁻¹ + (a + 5/2)) *      (volume G ^ (1 - q⁻¹) * (volume F ^ q⁻¹ * 2 ^ (- ((q - 1) / (8 * ↑a ^ 4) * n)))) := by    rw [← ENNReal.rpow_add _ _ (NeZero.ne 2) ENNReal.ofNat_ne_top]    have : (4 : ℝ) ≤ a := mod_cast (four_le_a X)    gcongr    · exact one_le_two    · calc      (4 * a + 1) * (q - 1) / (8 * a ^ 4 : ℝ)      _ ≤ (4 * a + a) * (2 - 1) / (8 * a ^ 4) := by         gcongr         · norm_cast           linarith [four_le_a X]         · exact q_le_two X      _ = 5 / (8 * a ^ 3) := by field_simp; norm_num      _ ≤ 5 / (8 * (4 : ℝ) ^ 3) := by gcongr      _ ≤ 2⁻¹ := by norm_num    · calc      (2 * ↑a + 5) * (q⁻¹ - 2⁻¹)      _ ≤ (2 * ↑a + 5) * (1⁻¹ - 2⁻¹) := by gcongr; exact (one_lt_q X).le      _ = a + 5/2 := by ring  _ = 2 ^ (a + 3) *      (volume G ^ (1 - q⁻¹) * (volume F ^ q⁻¹ * 2 ^ (- ((q - 1) / (8 * ↑a ^ 4) * n)))) := by    congr 1    rw [← ENNReal.rpow_natCast]    congr    simp    ring