CanonicalLowerSegments.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Compact lower bounds give positivity simultaneously on every trace segment. Only a countable compact exhaustion is used before choosing the time interval.

lemma OAI.SLEExactGauge.Multipoint.exists_compact_covering_positive_inter line 17

theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.positive_all_segments_of_compact_lower line 46

Source documentation

A countable compact lower criterion and the proved positivity of every canonical increment imply the required simultaneous segment lower bound.

theorem positive_all_segments_of_compact_lower (h : ℝ → ℝ)
    (hlower : ∀ n : ℕ, ∀ᵐ ω ∂P, ∀ E : Set ℂ, MeasurableSet E →
      0 < C.rational.terminal ω (compactCovering upperHalfPlane n ∩ Subtype.val ⁻¹' E) →
      0 < Target.hausdorff h E) :
    ∀ᵐ ω ∂P, ∀ s t : ℝ≥0, s < t →
      0 < Target.hausdorff h (γ ω '' Icc s t) := by
…

Mentions: OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.Target.hausdorff