ExperimentChangeOfLaw.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The finite centered law pays a uniform cost for an actual successful experiment whose marked-point angle stays positive. Its finite completion stop is used before the conformal-radius cutoff.

lemma OAI.SLEExactGauge.greenDensity_lower_of_angle line 16

theorem OAI.SLEExactGauge.finiteCenteredLaw_experiment_lower_bound line 53

Source documentation

An event observed at a finite experiment stop transfers to the finite radius law using its actual Green density there.

theorem finiteCenteredLaw_experiment_lower_bound
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (hBm : Measurable (fun p : ℝ≥0 × Ω => B p.1 p.2))
    (hBc : ∀ ω, Continuous (fun t => B t ω)) (hB0 : ∀ ω, B 0 ω = 0)
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ᵐ ω ∂P, IsCapacityTwoWitness
      (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω))
    (z : ℂ) (hz : z ∈ upperHalfPlane) (u : ℝ) (hu : 0 ≤ u)
    (σ : Ω → ℝ≥0)
    (hσ : IsStoppingTime (Filtration.natural B
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.upperHalfPlane