ActualExplicitTransfer.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Passage from a regular presentation to an arbitrary ordinary SLE. The subtype restriction preserves the published geometric support input, and whole-trace expectations transfer through its measure-preserving map.

def OAI.SLEExactGauge.sourceBasedDriverPath line 20

Source documentation

The same continuous Brownian path, retaining its pointwise zero start.

def sourceBasedDriverPath {Ω : Type*} (B : ℝ≥0 → Ω → ℝ)
    (hc : ∀ ω, Continuous (fun t => B t ω)) (h0 : ∀ ω, B 0 ω = 0)
    (ω : Ω) : Driver where
…

lemma OAI.SLEExactGauge.sourceBasedDriverPath_measurable line 26

theorem OAI.SLEExactGauge.sourceBasedDriverLaw_isWiener line 36

Source documentation

An ordinary regular presentation supplies the based Wiener law needed by the two-dimensional Brownian support input.

theorem sourceBasedDriverLaw_isWiener
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
    (B : ℝ≥0 → Ω → ℝ) (hB : IsBrownianReal B P)
    (hm : ∀ t, Measurable (B t))
    (hc : ∀ ω, Continuous (fun t => B t ω)) (h0 : ∀ ω, B 0 ω = 0) :
    IsWiener (P.map (sourceBasedDriverPath B hc h0)) := by
…

Mentions: OAI.SLEExactGauge.sourceBasedDriverPath

theorem OAI.SLEExactGauge.RegularSLEPresentation.geometric_support line 50
theorem OAI.SLEExactGauge.ordinary_explicit_main_of_regular_presentation line 68
def OAI.SLEExactGauge.ordinaryRegularPresentation line 106
Source documentation
A fixed choice is used only to state the precise canonical-driver law on which the Rohde--Schramm trace-generation input is needed.
```
def ordinaryRegularPresentation
    {Ω : Type} [MeasurableSpace Ω] {P : Measure Ω} {κ : ℝ}
    {γ : Ω → ℝ≥0 → ℂ} (hSLE : IsOrdinaryChordalSLE κ γ P) :
    RegularSLEPresentation P κ γ := Classical.choice (exists_regular_sle_presentation hSLE)
```
Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.RegularSLEPresentation, OAI.SLEExactGauge.exists_regular_sle_presentation
def OAI.SLEExactGauge.ordinaryRegularDriverLaw line 111
theorem OAI.SLEExactGauge.ordinary_explicit_mainConclusion line 119
Source documentation
The explicit exact-gauge main conclusion for any ordinary chordal SLE, conditional on the same eight published inputs as the regular theorem.
```
theorem ordinary_explicit_mainConclusion
    {Ω : Type} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (htrace : PublishedTraceGeneration (ordinaryRegularDriverLaw hSLE) κ (fun t p => p t))
    (hcompact : PublishedHalfPlaneUnivalentCompactness)
    (hboundary : PublishedFiniteLoewnerBoundaryExtension)
    (hsupport : PublishedGeometricTubeSupport P γ)
    (hplanar : PublishedPlanarDiskOpenness)
    (hstraight : PublishedHalfPlaneCrosscutStraightening)
    (hexit : PublishedHalfPlaneConformalExitLaw)
    (hwiener : PublishedPlanarWienerUnitSupport)
…
```
Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.PublishedTraceGeneration, OAI.SLEExactGauge.ordinaryRegularDriverLaw, OAI.SLEExactGauge.PublishedHalfPlaneUnivalentCompactness, OAI.SLEExactGauge.PublishedFiniteLoewnerBoundaryExtension, OAI.SLEExactGauge.PublishedGeometricTubeSupport, OAI.SLEExactGauge.PublishedPlanarDiskOpenness, OAI.SLEExactGauge.PublishedHalfPlaneCrosscutStraightening, OAI.SLEExactGauge.PublishedHalfPlaneConformalExitLaw, OAI.SLEExactGauge.PublishedPlanarWienerUnitSupport
theorem OAI.SLEExactGauge.ordinary_explicit_mainConclusion_of_published_inputs line 139
Source documentation
The final ordinary-SLE theorem has no auxiliary Wiener-law assumption: that law is constructed from the chosen regular Brownian presentation.
```
theorem ordinary_explicit_mainConclusion_of_published_inputs
    {Ω : Type} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (htrace : PublishedTraceGeneration (ordinaryRegularDriverLaw hSLE) κ (fun t p => p t))
    (hcompact : PublishedHalfPlaneUnivalentCompactness)
    (hboundary : PublishedFiniteLoewnerBoundaryExtension)
    (hsupport : PublishedGeometricTubeSupport P γ)
    (hplanar : PublishedPlanarDiskOpenness)
    (hstraight : PublishedHalfPlaneCrosscutStraightening)
    (hexit : PublishedHalfPlaneConformalExitLaw)
    (hwiener : PublishedPlanarWienerUnitSupport) :
…
```
Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.PublishedTraceGeneration, OAI.SLEExactGauge.ordinaryRegularDriverLaw, OAI.SLEExactGauge.PublishedHalfPlaneUnivalentCompactness, OAI.SLEExactGauge.PublishedFiniteLoewnerBoundaryExtension, OAI.SLEExactGauge.PublishedGeometricTubeSupport, OAI.SLEExactGauge.PublishedPlanarDiskOpenness, OAI.SLEExactGauge.PublishedHalfPlaneCrosscutStraightening, OAI.SLEExactGauge.PublishedHalfPlaneConformalExitLaw, OAI.SLEExactGauge.PublishedPlanarWienerUnitSupport