SpatialExhaustion.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Removing the time and height cutoffs in the whole-trace upper bound.

def OAI.SLEExactGauge.interiorSpatialCutoff line 14
def OAI.SLEExactGauge.compactTraceCutoff line 17
lemma OAI.SLEExactGauge.interiorSpatialCutoff_isCompact line 20
lemma OAI.SLEExactGauge.interiorSpatialCutoff_subset line 25
lemma OAI.SLEExactGauge.compactTraceCutoff_monotone line 31
lemma OAI.SLEExactGauge.iUnion_compactTraceCutoff line 39
lemma OAI.SLEExactGauge.sle_compact_trace_aemeasurable line 60

theorem OAI.SLEExactGauge.whole_trace_expectation_of_compact_interior_bounds line 77

Source documentation

Exhaustion by compact interior sets in the upper Hausdorff estimate of Proposition prop:dense-cover-upper.

theorem whole_trace_expectation_of_compact_interior_bounds
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (κ : ℝ) (hκ : 0 < κ)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (h : ℝ → ℝ) (hh : IsGauge h)
    (hf : HasSmallRadiusFormula h (hFormula κ)) (R : ℝ) (C : ℝ≥0∞)
    (hcompact : ∀ (T : ℝ≥0) (K : Set ℂ), IsCompact K →
      K ⊆ upperHalfPlane ∩ closedBall 0 R →
      (∫⁻ ω, hausdorffGauge h (K ∩ (γ ω '' Icc 0 T)) ∂P) ≤ C) :
    (∫⁻ ω, hausdorffGauge h (wholeTrace (γ ω) ∩ closedBall 0 R) ∂P) ≤ C := by
…

Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.IsGauge, OAI.SLEExactGauge.HasSmallRadiusFormula, OAI.SLEExactGauge.hFormula, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.hausdorffGauge, OAI.SLEExactGauge.wholeTrace

theorem OAI.SLEExactGauge.mainConclusion_of_uniform_compact_interior_bounds line 113

Source documentation

Compact interior upper estimates imply the whole-trace upper bound.

theorem mainConclusion_of_uniform_compact_interior_bounds
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (h : ℝ → ℝ) (hh : IsGauge h)
    (hf : HasSmallRadiusFormula h (hFormula κ))
    (hcompact : ∀ R : ℝ, 0 < R → ∃ C : ℝ≥0∞, C < ∞ ∧
      ∀ (T : ℝ≥0) (K : Set ℂ), IsCompact K →
        K ⊆ upperHalfPlane ∩ closedBall 0 R →
        (∫⁻ ω, hausdorffGauge h (K ∩ (γ ω '' Icc 0 T)) ∂P) ≤ C) :
    MainConclusion P h γ := by
…