MassCompensatorMesh.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The deterministic quadratic-error estimate for the prescribed dyadic potential compensator. A finite terminal limit controls the growing horizon.

lemma OAI.SLEExactGauge.mass_path_uniformContinuous line 18
Source documentation
A continuous mass path with a finite terminal limit is uniformly continuous even though the compensator mesh horizon grows to infinity.
```
lemma mass_path_uniformContinuous (A : ℝ≥0 → ℝ) (L : ℝ)
    (hc : Continuous A) (hl : Tendsto A atTop (𝓝 L)) : UniformContinuous A := by
…
```
def OAI.SLEExactGauge.compensatorMeshTime line 23
lemma OAI.SLEExactGauge.compensatorMeshTime_zero line 26
lemma OAI.SLEExactGauge.compensatorMeshTime_mono line 29
lemma OAI.SLEExactGauge.compensatorMeshTime_dist line 33
lemma OAI.SLEExactGauge.compensatorMeshTime_small_increments line 41
def OAI.SLEExactGauge.compensatorQuadraticError line 57
lemma OAI.SLEExactGauge.compensatorQuadraticError_nonneg line 61
lemma OAI.SLEExactGauge.compensatorQuadraticError_le line 65
lemma OAI.SLEExactGauge.compensatorQuadraticError_le_terminal_sq line 87
theorem OAI.SLEExactGauge.compensatorQuadraticError_tendsto_zero line 99
Source documentation
The accumulated squared mass increments vanish for the exact growing horizon and dyadic mesh used by the paper's potential formula.
```
theorem compensatorQuadraticError_tendsto_zero (A : ℝ≥0 → ℝ) (L : ℝ)
    (hm : Monotone A) (h0 : A 0=0) (hc : Continuous A)
    (hl : Tendsto A atTop (𝓝 L)) (hb : ∀ t, A t ≤ L) :
    Tendsto (compensatorQuadraticError A) atTop (𝓝 0) := by
…
```
Mentions: OAI.SLEExactGauge.compensatorQuadraticError

theorem OAI.SLEExactGauge.compensatorQuadraticError_mean_tendsto_zero line 118

Source documentation

Dominated convergence for the exact quadratic mesh error; the bound requires only the second terminal moment, not a uniform time horizon.

theorem compensatorQuadraticError_mean_tendsto_zero
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (A : ℝ≥0 → Ω → ℝ) (L : Ω → ℝ)
    (hA : ∀ t, Measurable (A t)) (hL : Integrable (fun ω => L ω^2) P)
    (hp : ∀ᵐ ω ∂P, Monotone (fun t => A t ω) ∧ A 0 ω=0 ∧
      Continuous (fun t => A t ω) ∧ Tendsto (fun t => A t ω) atTop (𝓝 (L ω)) ∧
      ∀ t, A t ω ≤ L ω) :
    Tendsto (fun n => ∫ ω, compensatorQuadraticError (fun t => A t ω) n ∂P)
      atTop (𝓝 0) := by
…

Mentions: OAI.SLEExactGauge.compensatorQuadraticError