CanonicalDenseSections.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Measurable canonical sections for the proved conformal dense experiment. The probability estimate is transported from the actual SLE theorem; the canonical path and stopping kernels introduce no further stochastic input.

lemma OAI.SLEExactGauge.measurable_stoppedAtPath line 23
lemma OAI.SLEExactGauge.measurable_wholeSausageCharge_closedBall line 36
def OAI.SLEExactGauge.canonicalDenseEvent line 66

lemma OAI.SLEExactGauge.measurableSet_canonicalDenseEvent_random line 75

Source documentation

All geometric marked parameters may be random. In particular this applies to the product of the stopped past with a fresh driver path.

lemma measurableSet_canonicalDenseEvent_random
    {X : Type*} [MeasurableSpace X]
    (κ b v : ℝ) (m : ℕ) (Φ : C(ℝ≥0, ℝ) → C(ℝ≥0, ℂ)) (hΦ : Measurable Φ)
    (Fb : X → C(closedHalfPlane, ℂ)) (hFb : Measurable Fb)
    (u : X → ℝ) (hu : Measurable u) (w : X → ℂ) (hw : Measurable w)
    (r : X → ℝ) (hr : Measurable r) (a : X → ℂ) (ha : Measurable a)
    (Y : X → C(ℝ≥0, ℝ)) (hY : Measurable Y) :
    MeasurableSet {x | Y x ∈ canonicalDenseEvent κ Φ (Fb x) (u x) (w x)
      b (r x) m v (a x)} := by
…

Mentions: OAI.SLEExactGauge.closedHalfPlane, OAI.SLEExactGauge.canonicalDenseEvent

lemma OAI.SLEExactGauge.measurableSet_canonicalDenseEvent line 94
lemma OAI.SLEExactGauge.measurableSet_canonicalDenseEvent_product line 103
lemma OAI.SLEExactGauge.map_withDensity_comp line 117

theorem OAI.SLEExactGauge.canonical_finiteCenteredLaw_map line 129

Source documentation

The canonical density is exactly the pushforward of the original finite centered law, simultaneously for any chosen nonnegative level.

theorem canonical_finiteCenteredLaw_map
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    (κ : ℝ) (B : ℝ≥0 → Ω → ℝ)
    (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 ω))
    (u : ℝ) (hu : 0 ≤ u) (w : ℂ) :
    (finiteCenteredLaw μ κ B γ G w u).map (sourceDriverPath B hc) =
      (μ.map (sourceDriverPath B hc)).withDensity
        (fun p => canonicalFiniteDensity κ (u, w, p)) := by
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.finiteCenteredLaw, OAI.SLEExactGauge.sourceDriverPath, OAI.SLEExactGauge.canonicalFiniteDensity

theorem OAI.SLEExactGauge.Serpentine.uniform_canonical_conformal_dense_sections line 158

Source documentation

The conformal dense-experiment theorem on canonical driver space. The constants are those of the proved actual SLE theorem, with half the height margin reserved to use the finite boundary chart on the interior.

theorem uniform_canonical_conformal_dense_sections
    {Ω : Type} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (B : ℝ≥0 → Ω → ℝ) (hB : IsBrownianReal B μ)
    (hBm : Measurable (fun p : ℝ≥0 × Ω => B p.1 p.2))
    (hc : ∀ ω, Continuous (fun t => B t ω)) (hB0 : ∀ ω, B 0 ω = 0)
    (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω))
    (Φ : C(ℝ≥0, ℝ) → C(ℝ≥0, ℂ)) (hΦ : Measurable Φ)
    (hΦγ : ∀ᵐ ω ∂μ, Φ (sourceDriverPath B hc ω) = sourceTracePath γ (fun ω => (hw ω).1) ω)
    (hcompact : PublishedHalfPlaneUnivalentCompactness)
    (hboundary : PublishedFiniteLoewnerBoundaryExtension)
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.sourceDriverPath, OAI.SLEExactGauge.sourceTracePath, OAI.SLEExactGauge.PublishedHalfPlaneUnivalentCompactness, OAI.SLEExactGauge.PublishedFiniteLoewnerBoundaryExtension