OAI/Probability/SLE/Mass/CanonicalMassConstruction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SLEExactGauge.Multipoint.CanonicalMass line 15
2. theorem OAI.SLEExactGauge.Multipoint.exists_canonicalMass line 39

   Source documentation

   Proposition mass:construction of the first manuscript. The sole published input is the disk-growth consequence of Duren (1983), §2.3; all stochastic estimates and limiting arguments are proved here.

   theorem exists_canonicalMass
       {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
       {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
       (hBm : Measurable (Function.uncurry B)) (hBc : ∀ ω, Continuous (fun t => B t ω))
       (hB0 : ∀ ω, B 0 ω = 0) {κ : ℝ} (hκ : 0 < κ) (hκ8 : κ < 8)
       (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
       (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω))
       (hgrowth : PublishedDiskUnivalentGrowth) :
       Nonempty (CanonicalMass P κ B hBm γ G) := by
   …

   Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.PublishedDiskUnivalentGrowth, OAI.SLEExactGauge.Multipoint.CanonicalMass

3. theorem OAI.SLEExactGauge.RegularSLEPresentation.canonical_mass_main line 66

   Source documentation

   The canonical mass main construction for an ordinary SLE in its regular Brownian presentation, on its full-measure sample space.

   theorem RegularSLEPresentation.canonical_mass_main
       {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} {κ : ℝ}
       {γ : Ω → ℝ≥0 → ℂ} (a : RegularSLEPresentation P κ γ)
       (hκ : 0 < κ) (hκ8 : κ < 8) (hgrowth : PublishedDiskUnivalentGrowth) :
       Nonempty (Multipoint.CanonicalMass (P.comap (Subtype.val : a.samples → Ω)) κ a.B
         (measurable_uncurry_of_continuous_of_measurable a.continuous_B a.measurable_B)
         (fun ω => γ ω) a.G) :=
   …

   Mentions: OAI.SLEExactGauge.RegularSLEPresentation, OAI.SLEExactGauge.PublishedDiskUnivalentGrowth, OAI.SLEExactGauge.Multipoint.CanonicalMass