BoundaryNull.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Real-boundary cleanup in the all-time upper Hausdorff estimate.

theorem OAI.SLEExactGauge.hFormula_div_rpow_tendsto_zero line 14
Source documentation
The log-log correction is smaller than every power lost from dimension.
```
theorem hFormula_div_rpow_tendsto_zero {κ s : ℝ}
    (hκ : 0 < κ) (hs : s < dimension κ) :
    Tendsto (fun r => hFormula κ r / r ^ s) (𝓝[>] 0) (𝓝 0) := by
…
```
Mentions: OAI.SLEExactGauge.dimension, OAI.SLEExactGauge.hFormula
theorem OAI.SLEExactGauge.hausdorffGauge_le_hausdorffMeasure_of_power_bound line 33
Source documentation
An eventual power bound compares the diameter-defined gauge measure with ordinary Hausdorff measure.
```
theorem hausdorffGauge_le_hausdorffMeasure_of_power_bound
    {h : ℝ → ℝ} (hh : IsGauge h) {s : ℝ} (hs : 0 ≤ s)
    (hb : ∀ᶠ r in 𝓝[>] (0 : ℝ), h r ≤ r ^ s) :
    hausdorffGauge h ≤ (Measure.hausdorffMeasure s : Measure ℂ) := by
…
```
Mentions: OAI.SLEExactGauge.IsGauge, OAI.SLEExactGauge.hausdorffGauge
theorem OAI.SLEExactGauge.explicit_gauge_real_axis_null line 56
Source documentation
Every continuous completion of the explicit gauge gives zero measure to the entire real axis, hence also to its trace points in any bounded disk.
```
theorem explicit_gauge_real_axis_null {κ : ℝ} (hκ : 0 < κ)
    {h : ℝ → ℝ} (hh : IsGauge h)
    (hf : HasSmallRadiusFormula h (hFormula κ)) :
    hausdorffGauge h (range ((↑) : ℝ → ℂ)) = 0 := by
…
```
Mentions: OAI.SLEExactGauge.IsGauge, OAI.SLEExactGauge.HasSmallRadiusFormula, OAI.SLEExactGauge.hFormula, OAI.SLEExactGauge.hausdorffGauge