OAI/Probability/SLE/Mass/StoppedConformalPassageMass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Retained sausage mass before the actual passage stop. The physical curve may include boundary visits; only its retained interior interval is identified with the conformal image. All mass is charged to the prescribed stopped segment, rather than to later portions of the whole trace.

  1. def OAI.SLEExactGauge.segmentSausageCharge line 16
  2. theorem OAI.SLEExactGauge.sourceSausageSet_mono_interval line 20
  3. theorem OAI.SLEExactGauge.sourceSausageSet_congr_interval line 26
  4. theorem OAI.SLEExactGauge.segmentSausageCharge_mono line 34
  5. theorem OAI.SLEExactGauge.compact_conformal_stopped_passage_mass line 44

    Source documentation

    The finite-list conformal transfer charges only the actual stopped physical passage. Its values at parameter-boundary times can be supplied by the boundary-safe restart theorem.

    theorem compact_conformal_stopped_passage_mass
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (Fₙ : ℕ → ℂ → ℂ) (F : ℂ → ℂ)
    (hFn : ∀ n, DifferentiableOn ℂ (Fₙ n) upperHalfPlane)
    (hinj : ∀ n, InjOn (Fₙ n) upperHalfPlane)
    (hF : DifferentiableOn ℂ F upperHalfPlane)
    (hne : ∀ z ∈ upperHalfPlane, deriv F z ≠ 0)
    (hconv : TendstoLocallyUniformlyOn Fₙ F atTop upperHalfPlane)
    (K : Set ℂ) (hK : IsCompact K) (hKn : K.Nonempty) (hKH : K ⊆ upperHalfPlane)
    (R : Set ℂ) (hR : IsOpen R) (himage : F '' K ⊆ R)
…

    Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.upperHalfPlane

  6. theorem OAI.SLEExactGauge.compact_conformal_stopped_passage_mass_ae line 97

    Source documentation

    Almost-sure chart identities suffice; exceptional restart paths are removed without changing the probabilities of the retained events.

    theorem compact_conformal_stopped_passage_mass_ae
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (Fₙ : ℕ → ℂ → ℂ) (F : ℂ → ℂ)
    (hFn : ∀ n, DifferentiableOn ℂ (Fₙ n) upperHalfPlane)
    (hinj : ∀ n, InjOn (Fₙ n) upperHalfPlane)
    (hF : DifferentiableOn ℂ F upperHalfPlane)
    (hne : ∀ z ∈ upperHalfPlane, deriv F z ≠ 0)
    (hconv : TendstoLocallyUniformlyOn Fₙ F atTop upperHalfPlane)
    (K : Set ℂ) (hK : IsCompact K) (hKn : K.Nonempty) (hKH : K ⊆ upperHalfPlane)
    (R : Set ℂ) (hR : IsOpen R) (himage : F '' K ⊆ R)
…

    Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.upperHalfPlane

  7. theorem OAI.SLEExactGauge.countable_compact_conformal_stopped_passage_mass line 143

    Source documentation

    Countable compact/time certificates are extracted before choosing the common mesh. The selected intervals lie before the actual passage stop.

    theorem countable_compact_conformal_stopped_passage_mass
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (Fₙ : ℕ → ℂ → ℂ) (F : ℂ → ℂ)
    (hFn : ∀ n, DifferentiableOn ℂ (Fₙ n) upperHalfPlane)
    (hinj : ∀ n, InjOn (Fₙ n) upperHalfPlane)
    (hF : DifferentiableOn ℂ F upperHalfPlane)
    (hne : ∀ z ∈ upperHalfPlane, deriv F z ≠ 0)
    (hconv : TendstoLocallyUniformlyOn Fₙ F atTop upperHalfPlane)
    (K : ℕ → Set ℂ) (hK : ∀ i, IsCompact (K i)) (hKH : ∀ i, K i ⊆ upperHalfPlane)
    (R : Set ℂ) (hR : IsOpen R) (himage : ∀ i, F '' K i ⊆ R)
…

    Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.upperHalfPlane