FiberPrimitive.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SymmetricMahler.fiberAngle_sine_bound line 11
Source documentation
The actual chosen angular fiber satisfies the singular sine estimate.
```
theorem fiberAngle_sine_bound {q r₀ r : ℝ} (hr₀ : 0 ≤ r₀)
    (hq : radialMap r₀ = |q|) (hr : r ∈ Ioo r₀ 1) :
    sqrt ((1-r^2)*(radialMap r-radialMap r₀)/r) ≤ sin (fiberAngle q r) := by
…
```
Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.fiberAngle

theorem OAI.SymmetricMahler.fiber_primitive_uniform_small line 22

Source documentation

The small-error estimate for the angular fibers; measurability and the sine estimate are consequences, not premises.

theorem fiber_primitive_uniform_small {ε : ℝ} (hε : 0 < ε) :
    ∃ m₀ : ℝ, ∀ m : ℝ, m₀ ≤ m → ∀ r₀ ∈ Ico (0 : ℝ) 1,
      ∀ q : ℝ, radialMap r₀ = |q| → ∀ s ∈ Ico r₀ 1,
        IntervalIntegrable (radialPrimitiveDensity (fiberAngle q) m) volume r₀ s ∧
        (∫ r in r₀..s, radialPrimitiveDensity (fiberAngle q) m r) < s^(2*m : ℝ)+ε := by
…

Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.radialPrimitiveDensity, OAI.SymmetricMahler.fiberAngle

def OAI.SymmetricMahler.planarError line 34
Source documentation
A concrete nonnegative error function, valid also for every smaller m≥2.
```
noncomputable def planarError (m : ℝ) : ℝ := max 0 (Real.pi*errorEnvelope m)
```
Mentions: OAI.SymmetricMahler.errorEnvelope
lemma OAI.SymmetricMahler.planarError_nonneg line 36
lemma OAI.SymmetricMahler.planarError_tendsto_zero line 38
theorem OAI.SymmetricMahler.fiber_primitive_bound line 46
Source documentation
The actual radial primitive obeys the concrete error bound for every m≥2, not only eventually large m.
```
theorem fiber_primitive_bound {q r₀ m s : ℝ} (hm : 2 ≤ m) (hr₀ : 0 ≤ r₀)
    (hq : radialMap r₀ = |q|) (hs : s ∈ Ico r₀ 1) :
    (∫ r in r₀..s, radialPrimitiveDensity (fiberAngle q) m r) ≤ s^(2*m : ℝ)+planarError m := by
…
```
Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.radialPrimitiveDensity, OAI.SymmetricMahler.fiberAngle, OAI.SymmetricMahler.planarError