UniformError.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SymmetricMahler.radialCutoff line 8
lemma OAI.SymmetricMahler.radial_cutoff_bounds line 10
def OAI.SymmetricMahler.errorEnvelope line 20
Source documentation
A uniform majorant for the unscaled E_m, independent of r₀.
```
noncomputable def errorEnvelope (m : ℝ) : ℝ :=
…
```
theorem OAI.SymmetricMahler.uniform_error_bound line 27
Source documentation
The whole singular error integral is bounded uniformly in its basepoint. The only analytic premise about M is the radial derivative formula plus continuity/measurability; every integral estimate and endpoint argument is proved.
```
theorem uniform_error_bound {M : ℝ → ℝ}
    (hM : Measurable M) (hcont : ContinuousOn M (Ico 0 1))
    (hderiv : ∀ r ∈ Ioo 0 1, HasDerivAt M (radialDerivative r) r)
    {m r₀ : ℝ} (hm : 2 ≤ m) (hr₀ : 0 ≤ r₀) (hr₀1 : r₀ < 1) :
    IntervalIntegrable (errorIntegrand M r₀ m) volume r₀ 1 ∧
      (∫ r in r₀..(1 : ℝ), errorIntegrand M r₀ m r) ≤ errorEnvelope m := by
…
```
Mentions: OAI.SymmetricMahler.radialDerivative, OAI.SymmetricMahler.errorIntegrand, OAI.SymmetricMahler.errorEnvelope
theorem OAI.SymmetricMahler.cutoff_power_bound line 99
Source documentation
A decaying bound for the inner term, weaker than O(m⁻¹) but sufficient for uniform convergence.
```
theorem cutoff_power_bound {m : ℝ} (hm : 3 ≤ m) :
    m*(radialCutoff m)^(2*m-3/2 : ℝ) ≤ 1/sqrt m := by
…
```
Mentions: OAI.SymmetricMahler.radialCutoff
theorem OAI.SymmetricMahler.error_envelope_tendsto_zero line 137
Source documentation
The uniform majorant tends to zero; its rate is enough for the planar lemma.
```
theorem error_envelope_tendsto_zero : Tendsto errorEnvelope atTop (𝓝 0) := by
…
```
Mentions: OAI.SymmetricMahler.errorEnvelope

theorem OAI.SymmetricMahler.uniform_error_small line 179

Source documentation

The exact basepoint-uniform convergence needed in the planar lemma. No fixed basepoint is chosen before the threshold m₀.

theorem uniform_error_small {M : ℝ → ℝ}
    (hM : Measurable M) (hcont : ContinuousOn M (Ico 0 1))
    (hderiv : ∀ r ∈ Ioo 0 1, HasDerivAt M (radialDerivative r) r)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ m₀ : ℝ, ∀ m : ℝ, m₀ ≤ m → ∀ r₀ ∈ Ico (0 : ℝ) 1,
      IntervalIntegrable (errorIntegrand M r₀ m) volume r₀ 1 ∧
      (∫ r in r₀..(1 : ℝ), errorIntegrand M r₀ m r) < ε := by
…

Mentions: OAI.SymmetricMahler.radialDerivative, OAI.SymmetricMahler.errorIntegrand