OAI/Probability/SLE/Gauge/SerpentineInitialPrefix.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A single vertical support event starts every fitted serpentine at integer front one. Its probability is independent of the marked point and of the multiplicity.

  1. def OAI.SLEExactGauge.Serpentine.initialRiseStrip line 18
  2. def OAI.SLEExactGauge.Serpentine.initialRiseTarget line 20
  3. def OAI.SLEExactGauge.Serpentine.InitialRise line 22
  4. lemma OAI.SLEExactGauge.Serpentine.initialRise_positive line 26
  5. lemma OAI.SLEExactGauge.Serpentine.initial_prefix_coordinates line 48
  6. theorem OAI.SLEExactGauge.Serpentine.initialRise_gives_goodPrefix line 69
  7. theorem OAI.SLEExactGauge.Serpentine.uniform_initial_goodPrefix_probability line 114

    Source documentation

    The same positive lower bound works for every chart which is the initial vertical strip, and for every global extension of its progress.

    theorem uniform_initial_goodPrefix_probability
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    (κ : ℝ) (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ μ)
    (hsupport : PublishedGeometricTubeSupport μ γ)
    {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) :
    ∃ q : ℝ≥0∞, 0 < q ∧ ∀ P : ℂ → ℂ, ∀ g : C(ℂ, ℝ),
      (∀ z ∈ closedRibbon, g (P z) = z.re) →
      (∀ z ∈ closedRibbon, z.re ≤ 4 → P z = Complex.I * z) →
      q ≤ μ (GoodRibbonPrefix γ (ribbonFrontStop g γ 1) P ε) := by
…

    Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.PublishedGeometricTubeSupport, OAI.SLEExactGauge.GoodRibbonPrefix, OAI.SLEExactGauge.ribbonFrontStop

  8. theorem OAI.SLEExactGauge.Serpentine.uniform_experiment_initial_goodPrefix_probability line 132