dens1_antichain_sq

lemma dens1_antichain_sq (h𝔄 : IsAntichain (· ≤ ·) 𝔄)    (hg : Measurable g) (hgG : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :    eLpNorm (adjointCarlesonSum 𝔄 g) 2 ^ 2 ≤      (C6_1_4 a * dens₁ 𝔄 ^ (8 * a ^ 4 : ℝ)⁻¹ * eLpNorm g 2 volume) ^ 2 := by  calc    _ ≤ _ := dens1_antichain_dach hg hgG    _ ≤ Tile.C6_1_5 a * 2 ^ (6 * a + 1) * ∑ p with p ∈ 𝔄,        ∫⁻ y in E p, C6_1_6 a * dens₁ 𝔄 ^ (p₆ a)⁻¹ * M14 𝔄 (q₆ a) g y * ‖g y‖ₑ := by      gcongr with p mp; rw [← lintegral_const_mul _ hg.enorm]      refine setLIntegral_mono' measurableSet_E fun x mx ↦ mul_le_mul_left ?_ _      rw [Finset.mem_filter_univ] at mp      refine dach_bound h𝔄 mp hg hgG <|        ((E_subset_𝓘.trans Grid_subset_ball).trans (ball_subset_ball ?_)) mx      change (4 : ℝ) * D ^ 𝔰 p ≤ _; gcongr; norm_num    _ = Tile.C6_1_5 a * 2 ^ (6 * a + 1) * C6_1_6 a * dens₁ 𝔄 ^ (p₆ a)⁻¹ *        ∫⁻ y in ⋃ p ∈ 𝔄, E p, M14 𝔄 (q₆ a) g y * ‖g y‖ₑ := by      rw [mul_assoc _ (C6_1_6 a : ℝ≥0∞), mul_assoc (_ * _), ← lintegral_const_mul'']; swap      · exact (measurable_maximalFunction.aemeasurable.mul          hg.enorm.aemeasurable).restrict      congr 1; simp_rw [← mul_assoc]      rw [← lintegral_biUnion_finset _ (fun _ _ ↦ measurableSet_E)]      · simp only [Finset.mem_filter, Finset.mem_univ, true_and]      · intro p mp p' mp' hn        simp_rw [Finset.coe_filter, Finset.mem_univ, true_and, setOf_mem_eq] at mp mp'        exact not_not.mp ((tile_disjointness h𝔄 mp mp').mt hn)    _ ≤ Tile.C6_1_5 a * 2 ^ (6 * a + 1) * C6_1_6 a * dens₁ 𝔄 ^ (p₆ a)⁻¹ *        ∫⁻ y, M14 𝔄 (q₆ a) g y * ‖g y‖ₑ := by gcongr; exact Measure.restrict_le_self    _ ≤ Tile.C6_1_5 a * 2 ^ (6 * a + 1) * C6_1_6 a * dens₁ 𝔄 ^ (p₆ a)⁻¹ *        (eLpNorm (M14 𝔄 (q₆ a) g) 2 * eLpNorm g 2) := by      conv_rhs => enter [2, 2]; rw [← eLpNorm_enorm]      gcongr      exact ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm inferInstance        measurable_maximalFunction.aemeasurable hg.enorm.aemeasurable    _ ≤ Tile.C6_1_5 a * 2 ^ (6 * a + 1) * C6_1_6 a * dens₁ 𝔄 ^ (p₆ a)⁻¹ *        (2 ^ (a + 2) * eLpNorm g 2 ^ 2) := by      rw [sq, ← mul_assoc (_ ^ _)]      gcongr      exact M14_bound ((bcs_of_measurable_of_le_indicator_g hg hgG).memLp _)    _ ≤ _ := by      rw [mul_pow, mul_pow]; nth_rw 5 [← ENNReal.rpow_natCast]      rw [← ENNReal.rpow_mul, show ((2 : ℕ) : ℝ) = 2⁻¹⁻¹ by norm_num, ← mul_inv,        show 8 * a ^ 4 * 2⁻¹ = p₆ a by rw [p₆]; ring, mul_mul_mul_comm, ← mul_assoc]      gcongr      simp_rw [show (2 : ℝ≥0∞) = (2 : ℝ≥0) by rfl, ← ENNReal.coe_pow, ← ENNReal.coe_mul,        ENNReal.coe_le_coe, le_C6_1_4 (four_le_a X)]