UniformFrontPassage.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The uniform quantifier step for actual front passages. A compactness argument need only produce an eventual positive success probability along one strictly increasing subsequence of each vanishing-mesh sequence.

theorem OAI.SLEExactGauge.uniform_passage_threshold_of_subsequences line 18

Source documentation

The diagonal obstruction to a uniform passage estimate persists along all subsequences, so compactness need only control one of them.

theorem uniform_passage_threshold_of_subsequences
    {A : Type*} (p : A → ℝ → ℝ → ℝ≥0∞)
    (hmono : ∀ a v, Antitone (p a v))
    (hsequence : ∀ (a : ℕ → A) (v : ℕ → ℝ), (∀ n, 0 < v n) →
      Tendsto v atTop (𝓝 0) →
      ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∃ c : ℝ, 0 < c ∧ ∃ q : ℝ≥0∞, 0 < q ∧
        ∀ᶠ n in atTop, q ≤ p (a (φ n)) (v (φ n)) c) :
    ∃ q c v₀ : ℝ, 0 < q ∧ 0 < c ∧ 0 < v₀ ∧
      ∀ a : A, ∀ v : ℝ, 0 < v → v < v₀ → ENNReal.ofReal q ≤ p a v c := by
…

theorem OAI.SLEExactGauge.FirstFrontPassage.lt_before_firstFrontTime line 56
Source documentation
Before an attained first hit, a continuous coordinate that started below the front remains strictly below it.
```
theorem lt_before_firstFrontTime
    (x : ℝ≥0 → ℝ) (q : ℝ) (τ : ℝ≥0)
    (hτ : firstFrontTime x q = (τ : WithTop ℝ≥0))
    (hc : ContinuousOn x (Icc 0 τ)) (hstart : x 0 < q)
    (t : ℝ≥0) (ht : t < τ) : x t < q := by
…
```
Mentions: OAI.SLEExactGauge.FirstFrontPassage.firstFrontTime

theorem OAI.SLEExactGauge.PassageSuccess.frontSuccess_source_prefix line 78

Source documentation

The open-envelope success event gives exactly the strict pre-front containment used by the manuscript. The front point itself is specified separately by its attained coordinate and terminal offset.

theorem frontSuccess_source_prefix
    {Ω : Type*} (η : ℕ → Ω → ℝ≥0 → ℂ) (p : ℕ → ℂ → ℝ)
    (σ : Ω → ℝ≥0) (V : ℕ → Set ℂ) (a : ℕ → ℂ) (ε : ℝ) (n : ℕ)
    (ω : Ω) (hω : ω ∈ FrontSuccess η p σ V a ε n)
    (hc : ContinuousOn (fun t => p n (η n ω t))
      (Icc 0 (frontTime (fun t => p n (η n ω t)) 1)))
    (hstart : p n (η n ω 0) < 1) :
    MapsTo (η n ω) (Ico 0 (frontTime (fun t => p n (η n ω t)) 1))
      (V n ∩ {z | p n z < 1}) ∧
    p n (η n ω (frontTime (fun t => p n (η n ω t)) 1)) = 1 ∧
    ‖η n ω (frontTime (fun t => p n (η n ω t)) 1) - a n‖ < ε / 4 := by
…

Mentions: OAI.SLEExactGauge.PassageSuccess.FrontSuccess

def OAI.SLEExactGauge.PassageSuccess.frontPassageProbability line 97

Source documentation

Probability of the concrete full-prefix front success and its physical sausage mass. The index records an admissible physical configuration.

def frontPassageProbability
    {A Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (η : A → Ω → ℝ≥0 → ℂ) (p : A → ℂ → ℝ) (σ : A → Ω → ℝ≥0)
    (V : A → Set ℂ) (a : A → ℂ) (ε : A → ℝ) (κ : ℝ) (R : A → Set ℂ)
    (d : A) (v c : ℝ) : ℝ≥0∞ :=
…

theorem OAI.SLEExactGauge.PassageSuccess.frontPassageProbability_antitone line 109

Source documentation

Increasing the required mass only decreases the concrete passage probability; no probability or measurability assumption is needed here.

theorem frontPassageProbability_antitone
    {A Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (η : A → Ω → ℝ≥0 → ℂ) (p : A → ℂ → ℝ) (σ : A → Ω → ℝ≥0)
    (V : A → Set ℂ) (a : A → ℂ) (ε : A → ℝ) (κ : ℝ) (R : A → Set ℂ)
    (d : A) (v : ℝ) : Antitone (frontPassageProbability P η p σ V a ε κ R d v) := by
…

Mentions: OAI.SLEExactGauge.PassageSuccess.frontPassageProbability

theorem OAI.SLEExactGauge.PassageSuccess.frontPassageProbability_mono_start line 122

Source documentation

A later retained starting point gives a subset of the full passage success-and-mass event. This removes the auxiliary first-height stop from the final one-step conclusion.

theorem frontPassageProbability_mono_start
    {A Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (η : A → Ω → ℝ≥0 → ℂ) (p : A → ℂ → ℝ) (σ₁ σ₂ : A → Ω → ℝ≥0)
    (V : A → Set ℂ) (a : A → ℂ) (ε : A → ℝ) (κ : ℝ) (R : A → Set ℂ)
    (d : A) (v c : ℝ) (hσ : ∀ ω, σ₁ d ω ≤ σ₂ d ω) :
    frontPassageProbability P η p σ₂ V a ε κ R d v c ≤
      frontPassageProbability P η p σ₁ V a ε κ R d v c := by
…

Mentions: OAI.SLEExactGauge.PassageSuccess.frontPassageProbability

theorem OAI.SLEExactGauge.PassageSuccess.frontPassageProbability_le_from_zero line 135

theorem OAI.SLEExactGauge.PassageSuccess.uniform_frontPassage_probability_of_subsequences line 147

Source documentation

Once actual conformal compactness and the sequence passage theorem supply the subsequential estimate, the full uniform passage constants follow for the original concrete success-and-mass event.

theorem uniform_frontPassage_probability_of_subsequences
    {A Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (η : A → Ω → ℝ≥0 → ℂ) (p : A → ℂ → ℝ) (σ : A → Ω → ℝ≥0)
    (V : A → Set ℂ) (a : A → ℂ) (ε : A → ℝ) (κ : ℝ) (R : A → Set ℂ)
    (hsequence : ∀ (d : ℕ → A) (v : ℕ → ℝ), (∀ n, 0 < v n) →
      Tendsto v atTop (𝓝 0) →
      ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∃ c q : ℝ, 0 < c ∧ 0 < q ∧
        ∀ᶠ n in atTop, ENNReal.ofReal q ≤
          frontPassageProbability P η p σ V a ε κ R (d (φ n)) (v (φ n)) c) :
    ∃ q c v₀ : ℝ, 0 < q ∧ 0 < c ∧ 0 < v₀ ∧
      ∀ d : A, ∀ v : ℝ, 0 < v → v < v₀ → ENNReal.ofReal q ≤
        frontPassageProbability P η p σ V a ε κ R d v c := by
…

Mentions: OAI.SLEExactGauge.PassageSuccess.frontPassageProbability