DenseVisitNumerics.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The actual logarithmic choice of dense-visit multiplicity and the linear test window used in the explicit gauge cover.

def OAI.SLEExactGauge.coverMultiplicity line 15
def OAI.SLEExactGauge.coverTestWindow line 18
theorem OAI.SLEExactGauge.coverTestWindow_card_lower line 20
theorem OAI.SLEExactGauge.coverTestWindow_card_real_lower line 24
theorem OAI.SLEExactGauge.coverMultiplicity_upper line 32
theorem OAI.SLEExactGauge.coverMultiplicity_eventually_lower line 36
theorem OAI.SLEExactGauge.coverMultiplicity_eventually_ge line 47
theorem OAI.SLEExactGauge.coverMultiplicity_mass_lower line 57
Source documentation
The mass created by the prescribed integer multiplicity is at least the logarithmic correction of the explicit gauge.
```
theorem coverMultiplicity_mass_lower {c p : ℝ} (hc : 0 < c) (hp : 0 ≤ p) :
    ∀ᶠ n : ℕ in atTop,
      (c / 2) ^ p * (Real.log (n : ℝ)) ^ (p / 2) ≤
        (coverMultiplicity c n : ℝ) ^ p := by
…
```
Mentions: OAI.SLEExactGauge.coverMultiplicity

theorem OAI.SLEExactGauge.denseVisit_probability_eventually_lower line 74

Source documentation

A fixed dense-visit probability becomes at least n^(-1/2) at the logarithmic multiplicity. The prefactor is retained, rather than discarded.

theorem denseVisit_probability_eventually_lower
    {a C c : ℝ} (ha : 0 < a) (hC : 0 ≤ C) (hc : 0 < c)
    (hsmall : C * c ^ 2 ≤ 1 / 4) :
    ∀ᶠ n : ℕ in atTop,
      1 / Real.sqrt (n : ℝ) ≤
        a * Real.exp (-C * (coverMultiplicity c n : ℝ) ^ 2) := by
…

Mentions: OAI.SLEExactGauge.coverMultiplicity