SourceSimultaneousCount.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The simultaneous-count proposition for the manuscript's actual scales.

theorem OAI.LipschitzHilbert.eventually_source_simultaneous_count_universal line 19

Source documentation

The lower threshold for L is independent of the finite top family. The dyadic branching parameter, enlarged width, and short-time cutoff are the original manuscript choices. No extra counting or transfer estimate is assumed.

theorem eventually_source_simultaneous_count_universal (Lip : ℝ≥0)
    (a k p t c c0 J : ℝ) (ha : 0 ≤ a) (hap : a + 1 ≤ p) (hkp : k + 1 ≤ p)
    (ht : 2 * a + p + 1 ≤ t) (hc0 : 0 ≤ c0) (hc : 4 * (c0 + 1) + 1 ≤ c) :
    ∀ᶠ L : ℝ in atTop, ∀ (u : ℝ × ℝ → ℝ), LipschitzWith Lip u →
      ∀ (ι : Type*) [Fintype ι] [DecidableEq ι], ∀ m tau : ℝ,
      Real.exp (L ^ (9 / 10 : ℝ)) ≤ m →
      m ≤ 2 * Real.exp (L ^ (9 / 10 : ℝ)) →
      0 ≤ tau → tau ≤ Real.exp (-(L ^ (97 / 100 : ℝ))) →
      ∀ (T : ι → SlopeBox) (d : ι → ℝ) (E : ι → Set (ℝ × ℝ)),
        (∀ i, (T i).length ≤ tau) →
        (∀ i, MeasurableSet (E i)) →
        (∀ i, (volume.prod volume) (E i) ≠ ∞) →
…

Mentions: OAI.LipschitzHilbert.SlopeBox

theorem OAI.LipschitzHilbert.eventually_source_simultaneous_count_uniform line 56
theorem OAI.LipschitzHilbert.eventually_source_simultaneous_count line 86