LevelRadonSupport.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Actual past support of every convex-tail Radon limit. Compact tests separated from the past trace vanish at all sufficiently high levels.

lemma OAI.SLEExactGauge.Multipoint.level_density_eventually_zero_on_compact line 18
lemma OAI.SLEExactGauge.Multipoint.halfPlane_level_test_eventually_zero_off_past line 48

lemma OAI.SLEExactGauge.Multipoint.convex_level_test_eventually_zero_off_past line 78

Source documentation

Every compact test away from the actual past vanishes on every late convex tail. The coefficients may be arbitrary: no normalization is used.

lemma convex_level_test_eventually_zero_off_past
    {Ω : Type*} {κ : ℝ} {B : ℝ≥0 → Ω → ℝ}
    {γ : Ω → ℝ≥0 → ℂ} {G F : Ω → ℝ≥0 → ℂ → ℂ} (ω : Ω)
    (hBc : Continuous (fun s => B s ω))
    (hw : IsCapacityTwoWitness (fun s => Real.sqrt κ * B s ω) (γ ω) (G ω) (F ω))
    (t : ℝ≥0) (f : C_c(upperHalfPlane,ℝ))
    (hf : ∀ z ∈ tsupport f, (z : ℂ) ∉ γ ω '' Icc 0 t)
    (u : ℕ → ℝ) (hu : Tendsto u atTop atTop)
    (s : ℕ → Finset ℕ) (w : ℕ → ℕ → ℝ) :
    ∀ᶠ n in atTop, ∫ z, f z ∂convexLevelMeasure κ B γ G u s w n t ω = 0 := by
…

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

theorem OAI.SLEExactGauge.Multipoint.convex_level_radon_limit_carried_by_past line 117

Source documentation

Any vague limit of the actual convex level measures at a finite time is carried by the actual trace up to that time.

theorem convex_level_radon_limit_carried_by_past
    {Ω : Type*} {κ : ℝ} {B : ℝ≥0 → Ω → ℝ}
    {γ : Ω → ℝ≥0 → ℂ} {G F : Ω → ℝ≥0 → ℂ → ℂ} (ω : Ω)
    (hBc : Continuous (fun s => B s ω))
    (hw : IsCapacityTwoWitness (fun s => Real.sqrt κ * B s ω) (γ ω) (G ω) (F ω))
    (t : ℝ≥0) (u : ℕ → ℝ) (hu : Tendsto u atTop atTop)
    (s : ℕ → Finset ℕ) (w : ℕ → ℕ → ℝ) (ν : Measure upperHalfPlane) [ν.Regular]
    (hlim : ∀ f : C_c(upperHalfPlane,ℝ),
      Tendsto (fun n => ∫ z, f z ∂convexLevelMeasure κ B γ G u s w n t ω)
        atTop (𝓝 (∫ z, f z ∂ν))) :
    ν {z : upperHalfPlane | (z : ℂ) ∉ γ ω '' Icc 0 t} = 0 := by
…

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

theorem OAI.SLEExactGauge.Multipoint.convex_level_radon_limit_zero_at_zero line 134

theorem OAI.SLEExactGauge.Multipoint.ae_common_level_radon_limits_carried_by_past line 160

Source documentation

The support conclusion holds simultaneously for the prescribed countable list of finite times on the same vague-convergence event.

theorem ae_common_level_radon_limits_carried_by_past
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    {κ : ℝ} {B : ℝ≥0 → Ω → ℝ}
    {γ : Ω → ℝ≥0 → ℂ} {G F : Ω → ℝ≥0 → ℂ → ℂ}
    (hBc : ∀ ω, Continuous (fun s => B s ω))
    (hw : ∀ ω, IsCapacityTwoWitness
      (fun s => Real.sqrt κ * B s ω) (γ ω) (G ω) (F ω))
    (t : ℕ → ℝ≥0) (u : ℕ → ℝ) (hu : Tendsto u atTop atTop)
    (s : ℕ → Finset ℕ) (w : ℕ → ℕ → ℝ) (ν : ℕ → Ω → Measure upperHalfPlane)
    (hν : ∀ j ω, (ν j ω).Regular)
    (hlim : ∀ᵐ ω ∂P, ∀ j (f : C_c(upperHalfPlane,ℝ)),
      Tendsto (fun n => ∫ z, f z ∂convexLevelMeasure κ B γ G u s w n (t j) ω)
…

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

lemma OAI.SLEExactGauge.Multipoint.past_inter_surviving_subset_segment line 180

theorem OAI.SLEExactGauge.Multipoint.increment_le_restrict_trace_segment line 191

Source documentation

A positive increment dominated by the past mass and by the remaining mass is carried by the new segment. This is the deterministic consequence of past support and the conditional-kernel future support.

theorem increment_le_restrict_trace_segment
    (γ : ℝ≥0 → ℂ) (s t : ℝ≥0) (η μpast μfuture ν : Measure upperHalfPlane)
    (hηpast : η ≤ μpast) (hηfuture : η ≤ μfuture) (hην : η ≤ ν)
    (hpast : μpast {z : upperHalfPlane | (z : ℂ) ∉ γ '' Icc 0 t} = 0)
    (hfuture : μfuture {z : upperHalfPlane | (z : ℂ) ∉ survivingDomain γ s} = 0) :
    η ≤ ν.restrict {z : upperHalfPlane | (z : ℂ) ∈ γ '' Icc s t} := by
…

Mentions: OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.survivingDomain