dens1_antichain_dach

lemma dens1_antichain_dach (hg : Measurable g) (hgG : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :    eLpNorm (adjointCarlesonSum 𝔄 g) 2 ^ 2 ≤      Tile.C6_1_5 a * 2 ^ (6 * a + 1) * ∑ p with p ∈ 𝔄, dach 𝔄 p g * ∫⁻ y in E p, ‖g y‖ₑ := by  have bg := bcs_of_measurable_of_le_indicator_g hg hgG  calc    _ ≤ _ := dens1_antichain_rearrange bg    _ = 2 * ∑ p with p ∈ 𝔄,          ∑ p' with (p' ∈ 𝔄 ∧ 𝔰 p' ≤ 𝔰 p) ∧ (𝓘 p' : Set X) ⊆ ball (𝔠 p) (14 * D ^ 𝔰 p),            ‖∫ x, adjointCarleson p' g x * conj (adjointCarleson p g x)‖ₑ := by      congr! 2 with p mp; nth_rw 2 [← Finset.filter_filter]      refine (Finset.sum_filter_of_ne fun x mx nx ↦ ?_).symm      rw [Finset.mem_filter_univ] at mx      contrapose! nx; exact Tile.correlation_zero_of_ne_subset mx.2 nx    _ ≤ 2 * ∑ p with p ∈ 𝔄,        ∑ p' with (p' ∈ 𝔄 ∧ 𝔰 p' ≤ 𝔰 p) ∧ (𝓘 p' : Set X) ⊆ ball (𝔠 p) (14 * D ^ 𝔰 p),        Tile.C6_1_5 a * (1 + edist_(p') (𝒬 p') (𝒬 p)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) /        volume (𝓘 p : Set X) * (∫⁻ y in E p', ‖g y‖ₑ) * ∫⁻ x in E p, ‖g x‖ₑ := by      gcongr with p mp p' mp'      rw [Finset.mem_filter_univ] at mp'      exact Tile.correlation_le mp'.1.2 hg hgG    _ = 2 * Tile.C6_1_5 a * ∑ p with p ∈ 𝔄, (∫⁻ x in E p, ‖g x‖ₑ) * (volume (𝓘 p : Set X))⁻¹ *          ∑ p' with (p' ∈ 𝔄 ∧ 𝔰 p' ≤ 𝔰 p) ∧ (𝓘 p' : Set X) ⊆ ball (𝔠 p) (14 * D ^ 𝔰 p),            ∫⁻ y, (1 + edist_(p') (𝒬 p') (𝒬 p)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) *              (E p').indicator (‖g ·‖ₑ) y := by      rw [mul_assoc, Finset.mul_sum _ _ (Tile.C6_1_5 a : ℝ≥0∞)]; congr! 2 with p mp      rw [Finset.mul_sum, Finset.mul_sum]; congr! 1 with p' mp'      rw [ENNReal.div_eq_inv_mul, lintegral_const_mul _ (hg.enorm.indicator measurableSet_E),        lintegral_indicator measurableSet_E]      ring    _ ≤ 2 * Tile.C6_1_5 a * ∑ p with p ∈ 𝔄,          (∫⁻ x in E p, ‖g x‖ₑ) * (2 ^ (6 * a) * (volume (ball (𝔠 p) (14 * D ^ 𝔰 p)))⁻¹) *            ∑ p' with (p' ∈ 𝔄 ∧ 𝔰 p' ≤ 𝔰 p) ∧ (𝓘 p' : Set X) ⊆ ball (𝔠 p) (14 * D ^ 𝔰 p),              ∫⁻ y, (1 + edist_(p') (𝒬 p') (𝒬 p)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) *                (E p').indicator (‖g ·‖ₑ) y := by      gcongr with p mp      rw [← ENNReal.inv_le_inv, ENNReal.mul_inv (.inl (by positivity)) (.inl (by finiteness)),        inv_inv, inv_inv, ← ENNReal.div_eq_inv_mul]      apply ENNReal.div_le_of_le_mul'      calc        _ ≤ volume (ball (𝔠 p) (2 ^ 6 * (D ^ 𝔰 p / 4))) := by rw [← mul_comm_div]; gcongr; norm_num        _ ≤ defaultA a ^ 6 * volume (ball (𝔠 p) (D ^ 𝔰 p / 4)) :=          measure_ball_two_le_same_iterate _ _ _        _ ≤ _ := by          simp_rw [defaultA, Nat.cast_pow, Nat.cast_ofNat, pow_mul']; gcongr          exact ball_subset_Grid    _ = _ := by      conv_lhs => enter [2, 2, p]; rw [mul_comm _ (_ * _), mul_assoc, mul_assoc]      rw [← Finset.mul_sum, ← mul_assoc]; congr 1      · rw [← mul_rotate, ← pow_succ, mul_comm]      · congr! 1 with p mp; rw [mul_comm (lintegral ..), ← mul_assoc, dach]; congr 2        exact (lintegral_finsetSum _ fun p' mp' ↦          (hg.enorm.indicator measurableSet_E).const_mul _).symm