OAI/Probability/SLE/Geometry/FirstHeightBounded.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SLEExactGauge.FirstHeightSupport.narrowRiseBy line 17
2. theorem OAI.SLEExactGauge.FirstHeightSupport.isOpen_narrowRiseBy line 21
3. theorem OAI.SLEExactGauge.FirstHeightSupport.measurableSet_narrowRiseBy line 34
4. theorem OAI.SLEExactGauge.FirstHeightSupport.narrowRiseEvent_eq_iUnion line 37
5. theorem OAI.SLEExactGauge.FirstHeightSupport.scalePath_narrowRiseBy_iff line 48
6. theorem OAI.SLEExactGauge.FirstHeightSupport.narrowRiseBy_probability_scaling line 92
7. theorem OAI.SLEExactGauge.FirstHeightSupport.uniform_bounded_narrowRise_probability line 128

   Source documentation

   The uniform probability can be realized before a deterministic multiple of the square of the spatial scale.

   theorem uniform_bounded_narrowRise_probability
       {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
       (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
       (B₀ : ℝ≥0 → Ω → ℝ) (hB₀ : IsBrownianReal B₀ P)
       (hm : ∀ t, Measurable (B₀ t)) (hc : ∀ ω, Continuous (fun t => B₀ t ω))
       (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
       (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B₀ t ω) (γ ω) (G ω) (F ω))
       (hpublished : PublishedGeometricTubeSupport P γ) :
       ∃ T₀ : ℝ≥0, 0 < T₀ ∧ ∃ q : ℝ≥0∞, 0 < q ∧ ∀ c : ℝ≥0, 0 < c →
         q ≤ P {ω | sourceTracePath γ (fun ω => (hw ω).1) ω ∈
           narrowRiseBy (c : ℝ) (T₀ * c ^ 2)} := by
   …

   Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.PublishedGeometricTubeSupport, OAI.SLEExactGauge.sourceTracePath, OAI.SLEExactGauge.FirstHeightSupport.narrowRiseBy

8. def OAI.SLEExactGauge.FirstHeightSupport.stoppedTracePath line 158

   Source documentation

   Stop a continuous trace at a finite stopping time, retaining a continuous path on the common nonnegative-time domain.

   def stoppedTracePath {Ω : Type*} (γ : Ω → ℝ≥0 → ℂ) (hc : ∀ ω, Continuous (γ ω))
       (σ : Ω → ℝ≥0) (ω : Ω) : C(ℝ≥0, ℂ) :=
   …

9. theorem OAI.SLEExactGauge.FirstHeightSupport.stoppedTracePath_measurable line 163

   Source documentation

   Every coordinate of this path is already measurable in the stopped past.

   theorem stoppedTracePath_measurable
       {Ω : Type*} [m : MeasurableSpace Ω] (ℱ : Filtration ℝ≥0 m)
       (γ : Ω → ℝ≥0 → ℂ) (ha : Adapted ℱ (fun t ω => γ ω t))
       (hc : ∀ ω, Continuous (γ ω)) (σ : Ω → ℝ≥0)
       (hσ : IsStoppingTime ℱ (fun ω => (σ ω : WithTop ℝ≥0))) :
       Measurable[hσ.measurableSpace] (stoppedTracePath γ hc σ) := by
   …

   Mentions: OAI.SLEExactGauge.FirstHeightSupport.stoppedTracePath

10. def OAI.SLEExactGauge.FirstHeightSupport.stoppedNarrowCertificate line 183

    Source documentation

    This concrete certificate depends only on the stopped trace. Its height and horizontal-strip conditions can therefore be tested in the stopped past.

    def stoppedNarrowCertificate {Ω : Type*} (γ : Ω → ℝ≥0 → ℂ) (σ : Ω → ℝ≥0)
        (B : ℝ) (T : ℝ≥0) : Set Ω :=
    …

11. theorem OAI.SLEExactGauge.FirstHeightSupport.stoppedNarrowCertificate_measurable line 188
12. def OAI.SLEExactGauge.FirstHeightSupport.boundedFirstHeightTime line 209

    Source documentation

    Finite first-height clock, stopped at the prescribed deterministic bound.

    def boundedFirstHeightTime (γ : ℝ≥0 → ℂ) (B : ℝ) (T : ℝ≥0) : ℝ≥0 :=
    …

13. theorem OAI.SLEExactGauge.FirstHeightSupport.boundedFirstHeightTime_coe line 212
14. theorem OAI.SLEExactGauge.FirstHeightSupport.boundedFirstHeightTime_le line 221
15. theorem OAI.SLEExactGauge.FirstHeightSupport.boundedFirstHeightTime_isStoppingTime line 227
16. theorem OAI.SLEExactGauge.FirstHeightSupport.narrowRiseBy_gives_bounded_certificate line 237

    Source documentation

    A bounded supported rise supplies a narrow certificate at the actual first-height clock.

    theorem narrowRiseBy_gives_bounded_certificate
        {B : ℝ} (hB : 0 < B) (p : C(ℝ≥0, ℂ)) (hp0 : p 0 = 0)
        {T : ℝ≥0} (hp : p ∈ narrowRiseBy B T) :
        let σ := boundedFirstHeightTime p B T
    …

    Mentions: OAI.SLEExactGauge.FirstHeightSupport.narrowRiseBy, OAI.SLEExactGauge.FirstHeightSupport.boundedFirstHeightTime

17. theorem OAI.SLEExactGauge.FirstHeightSupport.bounded_certificate_geometry line 257

    Source documentation

    Every measurable bounded certificate gives the full first-height geometry, including strict freshness and rectangle containment.

    theorem bounded_certificate_geometry
        (p : C(ℝ≥0, ℂ)) (hp0 : p 0 = 0) (hpH : ∀ t, 0 ≤ (p t).im)
        {B : ℝ} (hB : 0 < B) (T : ℝ≥0)
        (hcert : let σ := boundedFirstHeightTime p B T
    …

    Mentions: OAI.SLEExactGauge.FirstHeightSupport.boundedFirstHeightTime

18. theorem OAI.SLEExactGauge.FirstHeightSupport.bounded_certificate_gives_first_height line 310
19. theorem OAI.SLEExactGauge.FirstHeightSupport.uniform_boundedFirstHeight_probability line 321

    Source documentation

    Uniform bounded first-height probability in the form of a concrete stopped-past event.

    theorem uniform_boundedFirstHeight_probability
        {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
        (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
        (B₀ : ℝ≥0 → Ω → ℝ) (hB₀ : IsBrownianReal B₀ P)
        (hm : ∀ t, Measurable (B₀ t)) (hc : ∀ ω, Continuous (fun t => B₀ t ω))
        (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
        (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B₀ t ω) (γ ω) (G ω) (F ω))
        (hpublished : PublishedGeometricTubeSupport P γ) :
        ∃ T₀ : ℝ≥0, 0 < T₀ ∧ ∃ q : ℝ≥0∞, 0 < q ∧ ∀ c : ℝ≥0, 0 < c →
          q ≤ P (stoppedNarrowCertificate γ
            (fun ω => boundedFirstHeightTime (γ ω) c (T₀ * c ^ 2)) c (T₀ * c ^ 2)) := by
    …

    Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.PublishedGeometricTubeSupport, OAI.SLEExactGauge.FirstHeightSupport.stoppedNarrowCertificate, OAI.SLEExactGauge.FirstHeightSupport.boundedFirstHeightTime

20. theorem OAI.SLEExactGauge.FirstHeightSupport.boundedFirstHeight_certificate_measurable line 342

    Source documentation

    The event in the uniform probability theorem is measurable at its bounded first-height stopping time.

    theorem boundedFirstHeight_certificate_measurable
        {Ω : Type*} [m : MeasurableSpace Ω] (ℱ : Filtration ℝ≥0 m)
        (γ : Ω → ℝ≥0 → ℂ) (ha : Adapted ℱ (fun t ω => γ ω t))
        (hc : ∀ ω, Continuous (γ ω)) (B : ℝ) (T : ℝ≥0) :
        MeasurableSet[(boundedFirstHeightTime_isStoppingTime ℱ γ ha hc B T).measurableSpace]
          (stoppedNarrowCertificate γ (fun ω => boundedFirstHeightTime (γ ω) B T) B T) :=
    …

    Mentions: OAI.SLEExactGauge.FirstHeightSupport.boundedFirstHeightTime_isStoppingTime, OAI.SLEExactGauge.FirstHeightSupport.stoppedNarrowCertificate, OAI.SLEExactGauge.FirstHeightSupport.boundedFirstHeightTime

21. theorem OAI.SLEExactGauge.FirstHeightSupport.boundedFirstHeight_certificate_measurable_at_first line 354

    Source documentation

    The same event is measurable in the full first-height past, as used in the manuscript's conditional continuation argument.

    theorem boundedFirstHeight_certificate_measurable_at_first
        {Ω : Type*} [m : MeasurableSpace Ω] (ℱ : Filtration ℝ≥0 m)
        (γ : Ω → ℝ≥0 → ℂ) (ha : Adapted ℱ (fun t ω => γ ω t))
        (hc : ∀ ω, Continuous (γ ω)) (B : ℝ) (T : ℝ≥0) :
        MeasurableSet[(firstHeightTime_isStoppingTime ℱ γ ha hc (B / 4)).measurableSpace]
          (stoppedNarrowCertificate γ (fun ω => boundedFirstHeightTime (γ ω) B T) B T) := by
    …

    Mentions: OAI.SLEExactGauge.FirstHeightSupport.firstHeightTime_isStoppingTime, OAI.SLEExactGauge.FirstHeightSupport.stoppedNarrowCertificate, OAI.SLEExactGauge.FirstHeightSupport.boundedFirstHeightTime