LargerGaugeMain.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The larger-gauge corollary in the introduction of the explicit-gauge paper.

theorem OAI.SLEExactGauge.larger_gauge_not_sigmaFinite_on_all_segments line 18

Source documentation

On one event, every positive-time compact SLE segment has non-sigma-finite Hausdorff measure for Schramm's proposed exponent-one log-log gauge, by comparison with the explicit gauge's positive Hausdorff measure.

theorem larger_gauge_not_sigmaFinite_on_all_segments
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (h g : ℝ → ℝ) (hh : IsGauge h) (hg : IsGauge g)
    (hf : HasSmallRadiusFormula h (hFormula κ))
    (gf : HasSmallRadiusFormula g (gFormula κ)) :
    ∀ᵐ ω ∂P, ∀ s t : ℝ≥0, 0 < s → s < t →
      ¬ SigmaFinite ((hausdorffGauge g).restrict (segment (γ ω) s t)) := by
…

Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.IsGauge, OAI.SLEExactGauge.HasSmallRadiusFormula, OAI.SLEExactGauge.hFormula, OAI.SLEExactGauge.gFormula, OAI.SLEExactGauge.hausdorffGauge

theorem OAI.SLEExactGauge.larger_gauge_infinite_on_all_segments line 33

Source documentation

The same simultaneous event gives infinite total larger-gauge measure.

theorem larger_gauge_infinite_on_all_segments
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (h g : ℝ → ℝ) (hh : IsGauge h) (hg : IsGauge g)
    (hf : HasSmallRadiusFormula h (hFormula κ))
    (gf : HasSmallRadiusFormula g (gFormula κ)) :
    ∀ᵐ ω ∂P, ∀ s t : ℝ≥0, 0 < s → s < t →
      hausdorffGauge g (segment (γ ω) s t) = ∞ := by
…

theorem OAI.SLEExactGauge.schramm_gauge_not_sigmaFinite_on_all_segments line 50

Source documentation

The paper's larger-gauge corollary with deterministic gauges constructed in Lean, so no existence or completion hypothesis remains.

theorem schramm_gauge_not_sigmaFinite_on_all_segments
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P) :
    ∀ᵐ ω ∂P, ∀ s t : ℝ≥0, 0 < s → s < t →
      ¬ SigmaFinite ((hausdorffGauge (schrammGauge κ)).restrict
        (segment (γ ω) s t)) :=
…

Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.hausdorffGauge, OAI.SLEExactGauge.schrammGauge

theorem OAI.SLEExactGauge.schramm_gauge_infinite_on_all_segments line 63

Source documentation

Infinite total measure for the concrete exponent-one log-log gauge.

theorem schramm_gauge_infinite_on_all_segments
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P) :
    ∀ᵐ ω ∂P, ∀ s t : ℝ≥0, 0 < s → s < t →
      hausdorffGauge (schrammGauge κ) (segment (γ ω) s t) = ∞ :=
…

Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.hausdorffGauge, OAI.SLEExactGauge.schrammGauge