CompactTubeProbability.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A finite-cover argument makes individual tube probabilities uniform on a compact family of routes. No quantitative support estimate is assumed.

theorem OAI.SLEExactGauge.finite_positive_lower_bound line 15

theorem OAI.SLEExactGauge.compact_tube_probability_lower_bound line 31

Source documentation

Pointwise positivity on half-radius balls gives one positive lower bound for full-radius balls centered anywhere in a compact set.

theorem compact_tube_probability_lower_bound
    {X : Type*} [PseudoMetricSpace X] [MeasurableSpace X]
    (P : Measure X) (K : Set X) (hK : IsCompact K) {ε : ℝ} (hε : 0 < ε)
    (hpositive : ∀ x ∈ K, 0 < P (ball x (ε / 2))) :
    ∃ q : ℝ≥0∞, 0 < q ∧ ∀ x ∈ K, q ≤ P (ball x ε) := by
…

theorem OAI.SLEExactGauge.CompactRouteTubes.uniform_tube_probability_of_based_support line 60

Source documentation

The usual pointwise full-support statement for continuous paths based at zero is enough for a uniform tube probability over all routes with a fixed speed bound. Arzela--Ascoli and a finite cover supply the uniformity.

theorem uniform_tube_probability_of_based_support
    (P : Measure (unitInterval →ᵇ ℂ)) (C : ℝ≥0) {ε : ℝ} (hε : 0 < ε)
    (hsupport : ∀ f : unitInterval →ᵇ ℂ, f 0 = 0 → ∀ r : ℝ, 0 < r →
      0 < P (ball f r)) :
    ∃ q : ℝ≥0∞, 0 < q ∧ ∀ f : unitInterval →ᵇ ℂ,
      LipschitzWith C f → f 0 = 0 →
      q ≤ P {g | ∀ t : unitInterval, dist (g t) (f t) < ε} := by
…