ErrorBound.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SymmetricMahler.radial_power_bound line 11

Source documentation

Exponential majorization on the outer interval.

theorem radial_power_bound {m r : ℝ} (hm : 2 ≤ m) (hr : 0 ≤ r) (hr1 : r ≤ 1) :
    r ^ (2*m-3/2 : ℝ) ≤ exp (-m*(1-r)) := by
…

def OAI.SymmetricMahler.radialDerivative line 33
Source documentation
The radial derivative formula on 0<r<1. Its removable value at r=0 is not asserted by this definition.
```
noncomputable def radialDerivative (r : ℝ) : ℝ :=
…
```
lemma OAI.SymmetricMahler.log_le_half line 36
lemma OAI.SymmetricMahler.radial_log_lower line 42
theorem OAI.SymmetricMahler.radial_derivative_lower line 53
Source documentation
A concrete global positive lower bound for the radial derivative.
```
theorem radial_derivative_lower {r : ℝ} (hr : 0 < r) (hr1 : r < 1) :
    4/Real.pi^2 ≤ radialDerivative r := by
…
```
Mentions: OAI.SymmetricMahler.radialDerivative

lemma OAI.SymmetricMahler.boundary_layer_log_lower line 64

Source documentation

The logarithmic boundary layer starts at 1-log(m)/m.

lemma boundary_layer_log_lower {m r : ℝ} (hm : 1 < m)
    (hr : 0 < r) (hr1 : r < 1) (hlayer : 1-log m/m ≤ r) :
    log m/2 ≤ log ((1+r)/(1-r)) := by
…

theorem OAI.SymmetricMahler.boundary_layer_derivative_lower line 83

Source documentation

The estimate M'≥c log m holds with c=2/π².

theorem boundary_layer_derivative_lower {m r : ℝ} (hm : 1 < m)
    (hr : 0 < r) (hr1 : r < 1) (hlayer : 1-log m/m ≤ r) :
    (2/Real.pi^2)*log m ≤ radialDerivative r := by
…

Mentions: OAI.SymmetricMahler.radialDerivative

theorem OAI.SymmetricMahler.radial_increment_lower line 104
Source documentation
The global M-increment estimate obtained from the actual radial derivative, with only open-interval derivatives required, including when the left endpoint is 0.
```
theorem radial_increment_lower {M : ℝ → ℝ} {a b : ℝ}
    (ha : 0 ≤ a) (hab : a ≤ b) (hb : b < 1)
    (hcont : ContinuousOn M (Icc a b))
    (hderiv : ∀ x ∈ Ioo a b, HasDerivAt M (radialDerivative x) x) :
    (4/Real.pi^2)*(b-a) ≤ M b-M a := by
…
```
Mentions: OAI.SymmetricMahler.radialDerivative

theorem OAI.SymmetricMahler.boundary_layer_increment_lower line 119

Source documentation

The strengthened increment estimate inside the logarithmic boundary layer.

theorem boundary_layer_increment_lower {M : ℝ → ℝ} {m a b : ℝ}
    (hm : 1 < m) (ha : 0 ≤ a) (hab : a ≤ b) (hb : b < 1)
    (hlayer : 1-log m/m ≤ a)
    (hcont : ContinuousOn M (Icc a b))
    (hderiv : ∀ x ∈ Ioo a b, HasDerivAt M (radialDerivative x) x) :
    ((2/Real.pi^2)*log m)*(b-a) ≤ M b-M a := by
…

Mentions: OAI.SymmetricMahler.radialDerivative

def OAI.SymmetricMahler.errorIntegrand line 141
Source documentation
The unscaled error integrand.
```
noncomputable def errorIntegrand (M : ℝ → ℝ) (r₀ m r : ℝ) : ℝ :=
…
```

theorem OAI.SymmetricMahler.error_integrand_outer_bound line 146

Source documentation

Pointwise domination by the exactly integrated outer-tail kernel. Here c is the lower slope for M on the boundary layer.

theorem error_integrand_outer_bound {M : ℝ → ℝ} {r₀ m c b r : ℝ}
    (hm : 2 ≤ m) (hc : 0 < c) (hr : 0 ≤ r) (hbr : b < r) (hr1 : r < 1)
    (hincrement : c*(r-b) ≤ M r-M r₀) :
    errorIntegrand M r₀ m r ≤ sqrt (2/c) *
      (m*exp (-m*(1-r))*sqrt ((1-r)/(r-b))) := by
…

Mentions: OAI.SymmetricMahler.errorIntegrand

theorem OAI.SymmetricMahler.outer_error_integrable line 181

Source documentation

Integrability of the original outer error follows from the singular majorant; measurability is explicit so no unproved integrability is hidden in the integral.

theorem outer_error_integrable {M : ℝ → ℝ} {r₀ m c b : ℝ}
    (hM : Measurable M) (hm : 2 ≤ m) (hc : 0 < c) (hb : 0 ≤ b) (hb1 : b < 1)
    (hincrement : ∀ r ∈ Ioo b 1, c*(r-b) ≤ M r-M r₀) :
    IntervalIntegrable (errorIntegrand M r₀ m) volume b 1 := by
…

Mentions: OAI.SymmetricMahler.errorIntegrand

theorem OAI.SymmetricMahler.outer_error_integral_bound line 204

Source documentation

The outer portion of the error integral, with an explicit constant.

theorem outer_error_integral_bound {M : ℝ → ℝ} {r₀ m c b : ℝ}
    (hM : Measurable M) (hm : 2 ≤ m) (hc : 0 < c) (hb : 0 ≤ b) (hb1 : b < 1)
    (hincrement : ∀ r ∈ Ioo b 1, c*(r-b) ≤ M r-M r₀) :
    (∫ r in b..(1 : ℝ), errorIntegrand M r₀ m r) ≤
      sqrt (2/c)*(1+4/exp 1) := by
…

Mentions: OAI.SymmetricMahler.errorIntegrand

theorem OAI.SymmetricMahler.error_integrand_inner_bound line 230

Source documentation

The inner error is controlled by an integrable square-root singularity.

theorem error_integrand_inner_bound {M : ℝ → ℝ} {r₀ m c b r : ℝ}
    (hm : 2 ≤ m) (hc : 0 < c) (hr : 0 ≤ r) (hr₀ : r₀ < r)
    (hrb : r ≤ b) (_hb1 : b ≤ 1)
    (hincrement : c*(r-r₀) ≤ M r-M r₀) :
    errorIntegrand M r₀ m r ≤
      (m*b^(2*m-3/2 : ℝ)/sqrt c)*(1/sqrt (r-r₀)) := by
…

Mentions: OAI.SymmetricMahler.errorIntegrand

theorem OAI.SymmetricMahler.inner_error_integrable line 262

Source documentation

Integrability of the inner portion follows from the square-root majorant.

theorem inner_error_integrable {M : ℝ → ℝ} {r₀ m c b : ℝ}
    (hM : Measurable M) (hm : 2 ≤ m) (hc : 0 < c)
    (hr₀ : 0 ≤ r₀) (hr₀b : r₀ ≤ b) (hb1 : b ≤ 1)
    (hincrement : ∀ r ∈ Ioc r₀ b, c*(r-r₀) ≤ M r-M r₀) :
    IntervalIntegrable (errorIntegrand M r₀ m) volume r₀ b := by
…

Mentions: OAI.SymmetricMahler.errorIntegrand

theorem OAI.SymmetricMahler.inner_error_integral_bound line 284

Source documentation

The bound on the inner portion of the error integral, with its constant.

theorem inner_error_integral_bound {M : ℝ → ℝ} {r₀ m c b : ℝ}
    (hM : Measurable M) (hm : 2 ≤ m) (hc : 0 < c)
    (hr₀ : 0 ≤ r₀) (hr₀b : r₀ ≤ b) (hb1 : b ≤ 1)
    (hincrement : ∀ r ∈ Ioc r₀ b, c*(r-r₀) ≤ M r-M r₀) :
    (∫ r in r₀..b, errorIntegrand M r₀ m r) ≤ 2*m*b^(2*m-3/2 : ℝ)/sqrt c := by
…

Mentions: OAI.SymmetricMahler.errorIntegrand