Positivity of dens'

Stream: Carleson

[Jeremy Tan]

Is this the right way to prove the following statement, and if so how can the sorry be filled? Can the statement even be proven?

lemma pos_dens'_of_mem_𝔓pos (h : p ∈ TilesAt k) (h2 : p ∈ 𝔓pos (X := X)) : 0 < dens' k {p} := by
  simp_rw [dens', mem_singleton_iff, iSup_iSup_eq_left, lt_iSup_iff]
  use 2, le_rfl, p, h, le_rfl
  simp; refine ⟨⟨?_, ?_⟩ , volume_coeGrid_lt_top.ne⟩
  · exact pos_iff_ne_zero.mp <| ENNReal.zpow_pos (by simp) (by simp) _
  · apply pos_iff_ne_zero.mp
    change 0 < volume (𝓘 p ∩ G ∩ Q ⁻¹' ball_(p) (𝒬 p) 2)
    have : (𝓘 p : Set X) ⊆ Q ⁻¹' ball_(p) (𝒬 p) 2 := by
      refine image_subset_iff.mp ?_
      have := biUnion_Ω (X := X) (i := 𝓘 p)
      simp at this
      sorry
    rw [← inter_eq_right] at this; rw [inter_comm, ← inter_assoc, this]
    rw [𝔓pos, mem_setOf] at h2; exact h2.trans_le (measure_mono inter_subset_left)

The context is that in order to prove the last sentence of the second paragraph of the proof of Lemma 5.5.1 ("it follows from (5.1.7) that there exists $n\ge k$ with $p\in\mathfrak C(k,n)$") bounds on both sides of dens' k {p} must first be established. If dens' k {p} = 0, then since the bounds in the definition of ℭ k n are both positive, p doesn't belong to ℭ k n for any n

[Jeremy Tan]

I have already proven the other side

lemma dens'_le_of_mem_𝔓pos (h : p ∈ 𝔓pos (X := X)) : dens' k {p} ≤ 2 ^ (-k : ℤ) := by

[Floris van Doorn]

From h2 you can conclude that 0 < volume (𝓘 p ∩ G ∩ Q ⁻¹' ball_(p) (𝒬 p) r) for some r (use
Metric.iUnion_ball_nat and MeasureTheory.exists_measure_pos_of_not_measure_iUnion_null)

[Floris van Doorn]

(you might want to prove example (k : ℕ) : ⋃ n ≥ k, ball x n = univ := by sorry first)

[Jeremy Tan]

@Floris van Doorn thanks, Lemma 5.5.1 is proved (but with two caveats, described in the PR): https://github.com/fpvandoorn/carleson/pull/106

[Jeremy Tan]

(deleted)

[Floris van Doorn]

I've responded in the PR. I have a proof sketch of the hole in the proof.