ExactGaugeComparison.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The deterministic comparison behind Corollary cor:larger-gauge in An explicit exact Hausdorff gauge for SLE (26 September 2026).

The Hausdorff measures here are the existing Measure.mkMetric constructions, so the comparison applies to arbitrary countable spatial covers. No SLE estimate is assumed in the comparison theorem: positive measure for the smaller gauge is the sole input to the non-sigma-finiteness conclusion.

lemma OAI.SLEExactGauge.logLog_inv_tendsto_atTop line 22
theorem OAI.SLEExactGauge.hFormula_div_gFormula_tendsto_zero line 30
Source documentation
The regular exact gauge is asymptotically smaller than Schramm's proposed exponent-one log-log gauge.
```
theorem hFormula_div_gFormula_tendsto_zero {κ : ℝ} (hκ : 0 < κ) :
    Tendsto (fun r => hFormula κ r / gFormula κ r) (𝓝[>] 0) (𝓝 0) := by
…
```
Mentions: OAI.SLEExactGauge.hFormula, OAI.SLEExactGauge.gFormula
theorem OAI.SLEExactGauge.gauge_ratio_tendsto_zero line 46
theorem OAI.SLEExactGauge.hausdorffGauge_le_smul_of_ratio_tendsto_zero line 55
Source documentation
A small-radius ratio estimate gives a comparison of the associated Hausdorff measures, independently of their values at large radii.
```
theorem hausdorffGauge_le_smul_of_ratio_tendsto_zero
    {h g : ℝ → ℝ} (hh : IsGauge h) (hg : IsGauge g)
    (hratio : Tendsto (fun r => h r / g r) (𝓝[>] 0) (𝓝 0))
    {c : ℝ} (hc : 0 < c) :
    hausdorffGauge h ≤ ENNReal.ofReal c • hausdorffGauge g := by
…
```
Mentions: OAI.SLEExactGauge.IsGauge, OAI.SLEExactGauge.hausdorffGauge
theorem OAI.SLEExactGauge.hausdorffGauge_eq_zero_of_larger_finite line 80
Source documentation
Finite measure for a larger gauge forces zero measure for any gauge with vanishing ratio. This statement does not require the set to be measurable.
```
theorem hausdorffGauge_eq_zero_of_larger_finite
    {h g : ℝ → ℝ} (hh : IsGauge h) (hg : IsGauge g)
    (hratio : Tendsto (fun r => h r / g r) (𝓝[>] 0) (𝓝 0))
    {E : Set ℂ} (hfinite : hausdorffGauge g E < ∞) :
    hausdorffGauge h E = 0 := by
…
```
Mentions: OAI.SLEExactGauge.IsGauge, OAI.SLEExactGauge.hausdorffGauge

theorem OAI.SLEExactGauge.not_sigmaFinite_larger_of_positive line 98

Source documentation

Positive measure for the smaller gauge prevents sigma-finiteness of the larger Hausdorff measure restricted to that set.

theorem not_sigmaFinite_larger_of_positive
    {h g : ℝ → ℝ} (hh : IsGauge h) (hg : IsGauge g)
    (hratio : Tendsto (fun r => h r / g r) (𝓝[>] 0) (𝓝 0))
    {E : Set ℂ} (hpositive : 0 < hausdorffGauge h E) :
    ¬ SigmaFinite ((hausdorffGauge g).restrict E) := by
…

Mentions: OAI.SLEExactGauge.IsGauge, OAI.SLEExactGauge.hausdorffGauge

theorem OAI.SLEExactGauge.hausdorffGauge_larger_eq_top_of_positive line 118
theorem OAI.SLEExactGauge.larger_logLog_gauge_not_sigmaFinite line 129
Source documentation
Corollary cor:larger-gauge: once the explicit exact gauge has positive measure on a set, the exponent-one gauge is not sigma-finite there.
```
theorem larger_logLog_gauge_not_sigmaFinite {κ : ℝ} (hκ : 0 < κ)
    {h g : ℝ → ℝ} (hh : IsGauge h) (hg : IsGauge g)
    (hf : HasSmallRadiusFormula h (hFormula κ))
    (gf : HasSmallRadiusFormula g (gFormula κ))
    {E : Set ℂ} (hpositive : 0 < hausdorffGauge h E) :
    ¬ SigmaFinite ((hausdorffGauge g).restrict E) :=
…
```
Mentions: OAI.SLEExactGauge.IsGauge, OAI.SLEExactGauge.HasSmallRadiusFormula, OAI.SLEExactGauge.hFormula, OAI.SLEExactGauge.gFormula, OAI.SLEExactGauge.hausdorffGauge