SerpentineNormalizedMass.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The concrete connector and serpentine instantiate the actual stopped iteration. All m² selected strip masses are present by completion, with one positive initial probability and universal one-step constants.

def OAI.SLEExactGauge.Serpentine.experimentEntry line 18
def OAI.SLEExactGauge.Serpentine.experimentSteps line 21
def OAI.SLEExactGauge.Serpentine.normalizedExperimentDisk line 23
lemma OAI.SLEExactGauge.Serpentine.retained_middle_in_normalized_disk line 26

theorem OAI.SLEExactGauge.Serpentine.uniform_serpentine_normalized_stopped_mass line 42

Source documentation

The actual normalized dense experiment, conditional only on the recorded published inputs. Completion is finite on success and all mass belongs to the stopped prefix at the prescribed common mesh.

theorem uniform_serpentine_normalized_stopped_mass
    {Ω : Type} [mΩ : MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (B : ℝ≥0 → Ω → ℝ) (hB : IsBrownianReal B μ)
    (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 ω))
    (hcompact : PublishedHalfPlaneUnivalentCompactness)
    (hboundary : PublishedFiniteLoewnerBoundaryExtension)
    (hsupport : PublishedGeometricTubeSupport μ γ)
    (hplanar : PublishedPlanarDiskOpenness)
    (hstraight : PublishedHalfPlaneCrosscutStraightening)
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.PublishedHalfPlaneUnivalentCompactness, OAI.SLEExactGauge.PublishedFiniteLoewnerBoundaryExtension, OAI.SLEExactGauge.PublishedGeometricTubeSupport, OAI.SLEExactGauge.PublishedPlanarDiskOpenness, OAI.SLEExactGauge.PublishedHalfPlaneCrosscutStraightening