CanonicalImageMass.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The canonical process in a fixed conformal image. The pathwise limit event is common to all image maps and compact tests.

def OAI.SLEExactGauge.Multipoint.CanonicalMass.imageProcess line 19
lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.imageProcess_progressive line 22
lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.imageProcess_radon line 29
lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.imageProcess_paths line 35

theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.all_image_limits line 53

Source documentation

No image map changes the extraction: one event works for every map, every continuous nonnegative weight, all extended times, and all tests.

theorem all_image_limits
    (hBc : ∀ ω, Continuous (fun t => B t ω)) (hκ : 0 < κ) (hκ8 : κ < 8)
    (F : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω)) :
    ∀ᵐ ω ∂P, ∀ (D : Set ℂ) (J : upperHalfPlane ≃ₜ D)
      (w : C(upperHalfPlane,ℝ≥0)) (t : ℝ≥0∞) (f : C_c(D,ℝ)),
      Tendsto (fun n => ∫ z, f z ∂conformalMass J w
        (convexLevelMeasure κ B γ G (fun n => (n:ℝ)) C.rational.supports C.rational.weights n t ω))
        atTop (𝓝 (∫ z, f z ∂conformalMass J w (C.atTime t ω))) := by
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.Multipoint.conformalMass, OAI.SLEExactGauge.Multipoint.convexLevelMeasure