ActualExplicitMain.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The explicit-gauge main theorem for a regular Brownian-driven Loewner presentation, conditional on the precise published inputs used in the geometric and stochastic construction.

lemma OAI.SLEExactGauge.compact_upperHalfPlane_height_lower_bound line 21
theorem OAI.SLEExactGauge.regular_driver_gauge_mainConclusion line 31

theorem OAI.SLEExactGauge.regular_driver_explicit_mainConclusion line 74

Source documentation

The regular-driver form of the explicit exact-gauge result. The same conclusion includes finite expected measure in every bounded disk.

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

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