Antichain.stack_density

lemma stack_density (𝔄 : Set (𝔓 X)) (ϑ : Θ X) (N : ℕ) (L : Grid X) :    ∑ p ∈ 𝔄_aux 𝔄 ϑ N with 𝓘 p = L, volume (E p ∩ G) ≤      2^(a * (N + 5)) * dens₁ (𝔄 : Set (𝔓 X)) * volume (L : Set X) := by  -- Def. 6.3.17  set 𝔄' : Set (𝔓 X) := {p ∈ (𝔄_aux 𝔄 ϑ N) | 𝓘 p = L} with 𝔄'_def  have hI : ∀ {q q' : 𝔓 X} (hq : q ∈ 𝔄') (hq' : q' ∈ 𝔄'), 𝓘 q = 𝓘 q' := fun hq hq' ↦ by      simp only [𝔄'_def, 𝔄_aux] at hq hq'      rw [hq.2, hq'.2]  have heq : ∑ p ∈ (𝔄_aux 𝔄 ϑ N).toFinset with 𝓘 p = L, volume (E p ∩ G) =      ∑ p ∈ 𝔄'.toFinset, volume (E p ∩ G) := by congr; aesop  by_cases h𝔄' : 𝔄'.Nonempty  · -- Ineq. 6.3.18    have h_aux : ∀ (p : 𝔓 X) (hp : p ∈ 𝔄'.toFinset), volume (E p ∩ G) ≤        2^a * dens₁ (𝔄' : Set (𝔓 X)) * volume (L : Set X) := by      intro p hp      rw [mem_toFinset] at hp      calc volume (E p ∩ G)        _ ≤ volume (E₂ 2 p) := by          gcongr; intro x hx          refine ⟨⟨hx.1.1, hx.2⟩, ?_⟩          apply @ball_subset_ball _ instPseudoMetricSpaceWithFunctionDistance _ 1 2 (by norm_num)          exact subset_cball hx.1.2.1        _ ≤ 2^a * dens₁ (𝔄' : Set (𝔓 X)) * volume (L : Set X) := by          have hIL : 𝓘 p = L := by simp_rw [← hp.2]          have h2a : ((2 : ℝ≥0∞) ^ a)⁻¹ = 2^(-(a : ℤ)) := by            rw [← zpow_natCast, ENNReal.zpow_neg]          rw [← ENNReal.div_le_iff (ne_of_gt (hIL ▸ volume_coeGrid_pos (defaultD_pos a)))            (by finiteness), ← ENNReal.div_le_iff' (NeZero.ne (2 ^ a)) (by finiteness),            ENNReal.div_eq_inv_mul, h2a, dens₁]          refine le_iSup₂_of_le p hp ?_          refine le_iSup₂_of_le 2 le_rfl ?_          gcongr          · norm_cast          · refine le_iSup₂_of_le p (mem_lowerCubes.mpr ⟨p, hp, le_refl _⟩) ?_            refine le_iSup_of_le (le_refl _) ?_            gcongr            · simp            · rw [hIL]    let p : 𝔓 X := h𝔄'.choose    have hp : p ∈ 𝔄' := h𝔄'.choose_spec    -- Ineq. 6.3.19    have hth : ∃ (Θ' : Finset (Θ X)), Θ'.card ≤ 2^(a*(N+4)) ∧        ball_(p) ϑ (2^(N+1)) ⊆ ⋃ ϑ' ∈ Θ', ball_(p) ϑ' 0.2 := by      have hs : ball_(p) ϑ (2^(N+1)) ⊆ ball_(p) ϑ (2^(N+4)*0.2) := by        have hN4 : (2 : ℝ) ^ (N + 4) = 2 ^ (N + 1) * 2 ^ 3 := by ring        refine ball_subset_ball ?_        rw [← mul_one ((2 : ℝ)^ (N + 1) ), hN4, mul_assoc,          mul_le_mul_iff_of_pos_left (by positivity)]        norm_num      have hballs : BallsCoverBalls (WithFunctionDistance (𝔠 p) (↑D ^ 𝔰 p / 4)) (2 ^ (N + 4) * 0.2)        0.2 (defaultA a ^ (N + 4)) := ballsCoverBalls_iterate_nat      simp only [BallsCoverBalls, coveredByBalls_iff, defaultA, ← pow_mul] at hballs      obtain ⟨Θ', hΘ'_card, hΘ'_cover⟩ := hballs ϑ      exact ⟨Θ', hΘ'_card, subset_trans hs hΘ'_cover⟩    obtain ⟨Θ', hΘ'_card, hΘ'_cover⟩ := hth    have hex : ∀ (p' : 𝔓 X) (hp' : p' ∈ 𝔄'), ∃ (ϑ' : Θ X) (hϑ' : ϑ' ∈ Θ'),        𝒬 p' ∈ ball_(p) ϑ' 0.2 := fun p' hp' ↦ by      have hp'_in : 𝒬 p' ∈ ball_(p) ϑ (2 ^ (N + 1)) :=        ball_eq_of_grid_eq (hI hp hp') ▸ (lt_one_add _).trans hp'.1.2.2      have hp'_in' := hΘ'_cover hp'_in      simp only [mem_iUnion] at hp'_in'      exact hp'_in'    -- Claim 6.3.20    have hcap : ∀ (q q' : 𝔓 X) (hq : q ∈ 𝔄') (hq' : q' ∈ 𝔄') (hqq' : q ≠ q') (ϑ' : Θ X)        (hϑ' : ϑ' ∈ Θ'), ϑ' ∉ ball_(p) (𝒬 q) (0.2 : ℝ) ∩ ball_(p) (𝒬 q') (0.2 : ℝ) := by      intro q q' hq hq' hqq' ϑ' hϑ'      have hdis := disjoint_Ω hqq' (hI hq hq')      simp only [disjoint_iff, inf_eq_inter, bot_eq_empty] at hdis      intro hint      have h5 : (0.2 : ℝ) = 5⁻¹ := by norm_num      rw [h5] at hint      have hsub : ϑ' ∈ (Ω q) ∩ (Ω q') :=        mem_of_subset_of_mem (inter_subset_inter (ball_eq_of_grid_eq (hI hp hq) ▸ cball_subset)          (ball_eq_of_grid_eq (hI hp hq') ▸ cball_subset)) hint      rw [hdis] at hsub      exact hsub    have hcard : 𝔄'.toFinset.card ≤ 2^(a*(N+4)) := by      -- We only care about the restriction of f to 𝔄'      set f : 𝔓 X → Θ X := fun q ↦ if hq : q ∈ 𝔄' then (hex q hq).choose else ϑ with hf_def      refine (Finset.card_le_card_of_injOn f (fun q hq ↦ ?_) ?_).trans hΘ'_card      · simp_rw [hf_def, dif_pos (mem_toFinset.mp hq)]        exact (hex q (mem_toFinset.mp hq)).choose_spec.1      · intro q hq q' hq' hf        simp only [coe_toFinset] at hq hq'        have hfq : f q = (hex q hq).choose := by simp only [hf_def, dif_pos hq]        have hfq' : f q' = (hex q' hq').choose := by simp only [hf_def, dif_pos hq']        specialize hcap q q' hq hq'        contrapose! hcap        refine ⟨hcap, ⟨(hex q hq).choose, ⟨(hex q hq).choose_spec.1, ?_⟩⟩⟩        constructor <;> simp only [mem_ball]        · rw [dist_comm]          exact (hex q hq).choose_spec.2        · rw [dist_comm, ← hfq, hf, hfq']          exact (hex q' hq').choose_spec.2    -- Ineq. 6.3.16    calc ∑ p ∈ (𝔄_aux 𝔄 ϑ N).toFinset with 𝓘 p = L, volume (E p ∩ G)      _ = ∑ p ∈ 𝔄'.toFinset, volume (E p ∩ G) := heq      _ ≤ ∑ p ∈ 𝔄'.toFinset, 2^a * dens₁ (𝔄' : Set (𝔓 X)) * volume (L : Set X) :=        Finset.sum_le_sum h_aux      _ = 𝔄'.toFinset.card * (2^a * dens₁ (𝔄' : Set (𝔓 X)) * volume (L : Set X)) := by          rw [Finset.sum_const, nsmul_eq_mul]      _ ≤ 2 ^ (a * (N + 5)) * dens₁  (𝔄' : Set (𝔓 X)) * volume (L : Set X) := by        simp only [← mul_assoc]        gcongr        norm_cast        calc 𝔄'.toFinset.card * 2 ^ a          _ ≤ 2 ^ (a * (N + 4)) * 2 ^ a := mul_le_mul_left hcard _          _ = 2 ^ (a * (N + 5)) := by ring      _ ≤ 2 ^ (a * (N + 5)) * dens₁  (𝔄 : Set (𝔓 X)) * volume (L : Set X) := by        have hss : 𝔄' ⊆ 𝔄 := by          calc 𝔄'            _ ⊆ 𝔄_aux 𝔄 ϑ N := sep_subset _ _            _ ⊆ 𝔄 := sep_subset _ _        gcongr        exact dens₁_mono hss  · rw [heq]    have : 𝔄'.toFinset = ∅ := by      rw [Set.toFinset_eq_empty]      exact not_nonempty_iff_eq_empty.mp h𝔄'    rw [this, Finset.sum_empty]    exact zero_le