Antichain.tile_count

lemma tile_count {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ ·) 𝔄) (ϑ : range (Q (X := X))) :    eLpNorm (fun x ↦ ∑ p with p ∈ 𝔄, (1 + edist_(p) (𝒬 p) ϑ.val) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) *      (E p).indicator 1 x * G.indicator 1 x) (ENNReal.ofReal (p₆ a)) volume ≤    C6_1_6 a * dens₁ 𝔄 ^ (p₆ a)⁻¹ * volume (⋃ p ∈ 𝔄, (𝓘 p : Set X)) ^ (p₆ a)⁻¹ := by  obtain ⟨N, 𝔄_decomp⟩ := biUnion_𝔄_aux (𝔄 := 𝔄) (ϑ := ϑ)  calc    _ = eLpNorm (∑ n ∈ Finset.range N, fun x ↦ ∑ p ∈ 𝔄_aux 𝔄 ϑ n,        (1 + edist_(p) (𝒬 p) ϑ.val) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) *        (E p).indicator 1 x * G.indicator 1 x) (ENNReal.ofReal (p₆ a)) volume := by      congr! with x; rw [Finset.sum_apply]      nth_rw 1 [filter_mem_univ_eq_toFinset, ← 𝔄_decomp,        Finset.sum_biUnion (pairwiseDisjoint_𝔄_aux.subset (subset_univ _))]    _ ≤ ∑ n ∈ Finset.range N, eLpNorm (fun x ↦ ∑ p ∈ 𝔄_aux 𝔄 ϑ n,        (1 + edist_(p) (𝒬 p) ϑ.val) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) *        (E p).indicator 1 x * G.indicator 1 x) (ENNReal.ofReal (p₆ a)) volume := by      refine eLpNorm_sum_le (fun p mp ↦ ?_) ?_      · refine Finset.aestronglyMeasurable_fun_sum _ fun p mp ↦ ?_        simp_rw [mul_assoc, ← inter_indicator_mul]        exact ((AEMeasurable.indicator (by simp)          (measurableSet_E.inter measurableSet_G)).const_mul _).aestronglyMeasurable      · grw [ENNReal.one_le_ofReal, (one_lt_p₆ (four_le_a X)).le]    _ ≤ ∑ n ∈ Finset.range N, eLpNorm (fun x ↦ ∑ p ∈ 𝔄_aux 𝔄 ϑ n,        (2 : ℝ) ^ (-n * (2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) *        (E p).indicator 1 x * G.indicator 1 x) (ENNReal.ofReal (p₆ a)) volume := by      refine Finset.sum_le_sum fun n mn ↦ eLpNorm_mono_enorm fun x ↦ ?_      rw [enorm_eq_self, ENNReal.enorm_sum_eq_sum_enorm]; swap      · refine fun p mp ↦ mul_nonneg ?_ (indicator_nonneg (by simp) _)        exact mul_nonneg (Real.rpow_nonneg zero_le_two _) (indicator_nonneg (by simp) _)      refine Finset.sum_le_sum fun p mp ↦ ?_      simp_rw [enorm_mul, enorm_indicator_eq_indicator_enorm, Pi.one_apply, enorm_one, Pi.one_def]      gcongr      rw [Real.rpow_mul zero_le_two, Real.enorm_rpow_of_nonneg (by positivity) (by positivity),        ENNReal.rpow_neg, ← ENNReal.inv_rpow]; gcongr      rw [Real.rpow_neg zero_le_two, enorm_inv (by positivity), ENNReal.inv_le_inv, edist_dist,        ← ENNReal.ofReal_one, ← ENNReal.ofReal_add zero_le_one dist_nonneg, Real.rpow_natCast,        Real.enorm_eq_ofReal (by positivity)]      apply ENNReal.ofReal_le_ofReal      simp only [𝔄_aux, mem_toFinset] at mp      exact mp.2.1    _ ≤ ∑ n ∈ Finset.range N, (2 ^ ((𝕔 + 1) * a ^ 3 - n : ℝ)) ^ (p₆ a)⁻¹ * dens₁ 𝔄 ^ (p₆ a)⁻¹ *        volume (⋃ p ∈ 𝔄, (𝓘 p : Set X)) ^ (p₆ a)⁻¹ :=      Finset.sum_le_sum fun _ _ ↦ tile_count_aux h𝔄 ϑ    _ = 2 ^ ((𝕔 + 1) * a ^ 3 / p₆ a) * (∑ n ∈ Finset.range N, (2 ^ (-(p₆ a)⁻¹)) ^ n) *        dens₁ 𝔄 ^ (p₆ a)⁻¹ * volume (⋃ p ∈ 𝔄, (𝓘 p : Set X)) ^ (p₆ a)⁻¹ := by      rw [← Finset.sum_mul, ← Finset.sum_mul, Finset.mul_sum]; congr! with n mn      rw [← ENNReal.rpow_natCast, ← ENNReal.rpow_mul, ← ENNReal.rpow_mul, neg_mul, ← div_eq_inv_mul,        ← ENNReal.rpow_add _ _ two_ne_zero ENNReal.ofNat_ne_top, ← sub_eq_add_neg, ← sub_div,        ← div_eq_mul_inv]    _ ≤ _ := by gcongr; exact le_C6_1_6 _ (four_le_a X)