FirstHeightScaling.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The scale-independent narrow first-height probability follows from the proved equality of actual scaled trace laws and an exact tube-event scaling identity.

theorem OAI.SLEExactGauge.FirstHeightSupport.scalePath_narrowRiseEvent_iff line 21
Source documentation
Capacity scaling sends a narrow-rise event to exactly the correspondingly scaled narrow-rise event, including its finite time witness.
```
theorem scalePath_narrowRiseEvent_iff
    (p : C(ℝ≥0, ℂ)) (c : ℝ≥0) (hc : 0 < c) (B : ℝ) :
    ScaleTraceLaw.scalePath c p ∈ narrowRiseEvent ((c : ℝ) * B) ↔ p ∈ narrowRiseEvent B := by
…
```
Mentions: OAI.SLEExactGauge.ScaleTraceLaw.scalePath, OAI.SLEExactGauge.FirstHeightSupport.narrowRiseEvent

theorem OAI.SLEExactGauge.FirstHeightSupport.narrowRise_probability_scaling line 66

Source documentation

Narrow-rise probabilities for actual chordal SLE are invariant under simultaneous spatial and capacity-time scaling.

theorem narrowRise_probability_scaling
    {Ω : 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 ω))
    (c : ℝ≥0) (hcpos : 0 < c) (B : ℝ) :
    P {ω | sourceTracePath γ (fun ω => (hw ω).1) ω ∈ narrowRiseEvent ((c : ℝ) * B)} =
      P {ω | sourceTracePath γ (fun ω => (hw ω).1) ω ∈ narrowRiseEvent B} := by
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.sourceTracePath, OAI.SLEExactGauge.FirstHeightSupport.narrowRiseEvent

theorem OAI.SLEExactGauge.FirstHeightSupport.uniform_narrowFirstHeight_probability line 100

Source documentation

One fixed positive probability works for the narrow first-height event at every spatial scale. Its equality of laws has been proved above.

theorem uniform_narrowFirstHeight_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 γ) :
    ∃ q : ℝ≥0∞, 0 < q ∧ ∀ B : ℝ, 0 < B → q ≤ P {ω | NarrowFirstHeight B (γ ω)} := by
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.PublishedGeometricTubeSupport, OAI.SLEExactGauge.FirstHeightSupport.NarrowFirstHeight