DenseCandidateCover.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

The actual finite terminal-sausage candidates and missed cells in the explicit-gauge cover. All selections here are deterministic at one mesh.

abbrev OAI.SLEExactGauge.DenseCandidateIndex line 17
def OAI.SLEExactGauge.denseCandidateCenter line 19
def OAI.SLEExactGauge.denseCandidateRadius line 22
def OAI.SLEExactGauge.denseCandidateThreshold line 25
def OAI.SLEExactGauge.denseCandidateIndices line 28
def OAI.SLEExactGauge.denseFineCell line 35
def OAI.SLEExactGauge.denseMissedCell line 38
lemma OAI.SLEExactGauge.denseCandidate_mem line 46
lemma OAI.SLEExactGauge.denseCandidateRadius_pos line 56
lemma OAI.SLEExactGauge.denseCandidateRadius_le_one line 59
theorem OAI.SLEExactGauge.denseFineCell_eventually_subset_candidate line 72
Source documentation
Every fine cell is eventually contained in every candidate disk at its center throughout the exact window floor(n/3)..floor(2n/3).
```
theorem denseFineCell_eventually_subset_candidate {T : ℝ} (hT : 0 < T) :
    ∀ᶠ n : ℕ in atTop, ∀ j ∈ coverTestWindow n, ∀ ij : ℤ × ℤ,
      denseFineCell T n ij ⊆
        closedBall (denseCandidateCenter T n (ij, j)) (denseCandidateRadius T (ij, j)) := by
…
```
Mentions: OAI.SLEExactGauge.coverTestWindow, OAI.SLEExactGauge.denseFineCell, OAI.SLEExactGauge.denseCandidateCenter, OAI.SLEExactGauge.denseCandidateRadius

theorem OAI.SLEExactGauge.dense_candidates_and_missed_cover line 94

Source documentation

The missed cells are exactly the visited retained cells with no terminal candidate; this yields a pointwise cover without a random selection rule.

theorem dense_candidates_and_missed_cover
    {R T : ℝ} (hR : 0 ≤ R) (hT : 0 < T) {K : Set ℂ} (hK : K ⊆ closedBall 0 R)
    (κ b c : ℝ) :
    ∀ᶠ n : ℕ in atTop, ∀ (v : ℝ) (γ : ℝ≥0 → ℂ) z, z ∈ K ∩ range γ →
      (∃ i ∈ denseCandidateIndices R T K κ b c v n γ,
        z ∈ closedBall (denseCandidateCenter T n i) (denseCandidateRadius T i)) ∨
      ∃ ij ∈ retainedCoverGridIndex R (coverRadius T n) K,
        denseMissedCell κ T b c v n ij γ ∧ z ∈ denseFineCell T n ij := by
…

Mentions: OAI.SLEExactGauge.denseCandidateIndices, OAI.SLEExactGauge.denseCandidateCenter, OAI.SLEExactGauge.denseCandidateRadius, OAI.SLEExactGauge.retainedCoverGridIndex, OAI.SLEExactGauge.coverRadius, OAI.SLEExactGauge.denseMissedCell, OAI.SLEExactGauge.denseFineCell

lemma OAI.SLEExactGauge.denseCandidate_disk_subset line 118
def OAI.SLEExactGauge.denseCoverDiameter line 140
lemma OAI.SLEExactGauge.denseCoverDiameter_tendsto_zero line 143
lemma OAI.SLEExactGauge.denseCandidate_enlarged_diameter line 147
lemma OAI.SLEExactGauge.denseFineCell_diameter line 164
theorem OAI.SLEExactGauge.denseMissedCell_measurable line 173
lemma OAI.SLEExactGauge.extendedGauge_closedBall_le line 190

theorem OAI.SLEExactGauge.denseCandidate_eventual_gauge_charge line 209

Source documentation

The prescribed integer multiplicity pays the logarithmic correction of all selected disks, uniformly throughout the window.

theorem denseCandidate_eventual_gauge_charge
    {κ T b c : ℝ} (hκ8 : κ < 8) (hT : 0 < T) (hb : 0 < b) (hc : 0 < c)
    {h : ℝ → ℝ} (hh : IsGauge h) (hf : HasSmallRadiusFormula h (hFormula κ)) :
    ∃ C : ℝ≥0, 0 < C ∧ ∀ᶠ n : ℕ in atTop,
      ∀ (R : ℝ) (K : Set ℂ) (v : ℝ) (γ : ℝ≥0 → ℂ) i,
        i ∈ denseCandidateIndices R T K κ b c v n γ →
        extendedGauge h (ediam (closedBall (denseCandidateCenter T n i)
          (4 * denseCandidateRadius T i))) ≤
            (C : ℝ≥0∞) * wholeSausageCharge κ γ v
              (closedBall (denseCandidateCenter T n i) (denseCandidateRadius T i)) := by
…

Mentions: OAI.SLEExactGauge.IsGauge, OAI.SLEExactGauge.HasSmallRadiusFormula, OAI.SLEExactGauge.hFormula, OAI.SLEExactGauge.denseCandidateIndices, OAI.SLEExactGauge.extendedGauge, OAI.SLEExactGauge.denseCandidateCenter, OAI.SLEExactGauge.denseCandidateRadius, OAI.SLEExactGauge.wholeSausageCharge

theorem OAI.SLEExactGauge.denseFineCell_eventual_gauge_bound line 279
Source documentation
The cost of each fine cleanup cell has the matching explicit-gauge factor, independent of the cell center.
```
theorem denseFineCell_eventual_gauge_bound
    {κ T : ℝ} (hκ8 : κ < 8) (hT : 0 < T)
    {h : ℝ → ℝ} (hh : IsGauge h) (hf : HasSmallRadiusFormula h (hFormula κ)) :
    ∃ A : ℝ, 0 < A ∧ ∀ᶠ n : ℕ in atTop, ∀ ij : ℤ × ℤ,
      extendedGauge h (ediam (denseFineCell T n ij)) ≤
        ENNReal.ofReal (A * coverRadius T n ^ dimension κ *
          (Real.log (n : ℝ)) ^ (codimension κ / 2)) := by
…
```
Mentions: OAI.SLEExactGauge.IsGauge, OAI.SLEExactGauge.HasSmallRadiusFormula, OAI.SLEExactGauge.hFormula, OAI.SLEExactGauge.extendedGauge, OAI.SLEExactGauge.denseFineCell, OAI.SLEExactGauge.coverRadius, OAI.SLEExactGauge.dimension, OAI.SLEExactGauge.codimension

theorem OAI.SLEExactGauge.dense_candidate_cover_geometry line 302

Source documentation

The six concrete geometric hypotheses of the expected-cover reduction, with one constant and one sufficiently late cutoff for every path and mesh.

theorem dense_candidate_cover_geometry
    {κ R T b c : ℝ} (hκ8 : κ < 8) (hR : 0 ≤ R) (hT : 0 < T)
    (hb : 0 < b) (hc : 0 < c) {K : Set ℂ} (hK : K ⊆ closedBall 0 R)
    {h : ℝ → ℝ} (hh : IsGauge h) (hf : HasSmallRadiusFormula h (hFormula κ)) :
    ∃ C : ℝ≥0, 0 < C ∧ ∀ᶠ n : ℕ in atTop, ∀ (v : ℝ) (γ : ℝ≥0 → ℂ),
      (∀ i ∈ denseCandidateIndices R T K κ b c v n γ, denseCandidateRadius T i ≤ R + 3) ∧
      (∀ i ∈ denseCandidateIndices R T K κ b c v n γ,
        closedBall (denseCandidateCenter T n i) (denseCandidateRadius T i) ⊆ closedBall 0 (R + 3)) ∧
      (∀ i ∈ denseCandidateIndices R T K κ b c v n γ,
        extendedGauge h (ediam (closedBall (denseCandidateCenter T n i) (4 * denseCandidateRadius T i))) ≤
          (C : ℝ≥0∞) * wholeSausageCharge κ γ v
            (closedBall (denseCandidateCenter T n i) (denseCandidateRadius T i))) ∧
…

Mentions: OAI.SLEExactGauge.IsGauge, OAI.SLEExactGauge.HasSmallRadiusFormula, OAI.SLEExactGauge.hFormula, OAI.SLEExactGauge.denseCandidateIndices, OAI.SLEExactGauge.denseCandidateRadius, OAI.SLEExactGauge.denseCandidateCenter, OAI.SLEExactGauge.extendedGauge, OAI.SLEExactGauge.wholeSausageCharge