GlobalPlanarBound.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SymmetricMahler.planarPrimitive_eq_radial line 13
Source documentation
The vertical integral is the radial primitive, with endpoint continuity and every integration segment contained in the actual domain.
```
theorem planarPrimitive_eq_radial {q r₀ r : ℝ} {m : ℕ}
    (hm : 2 ≤ m) (hr₀ : 0 ≤ r₀) (hq : radialMap r₀ = |q|) (hr : r ∈ Ioo r₀ 1) :
    planarPrimitive m q (fiberHeight q r) = radialPrimitive q r₀ (m : ℝ) r := by
…
```
Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.planarPrimitive, OAI.SymmetricMahler.fiberHeight, OAI.SymmetricMahler.radialPrimitive
theorem OAI.SymmetricMahler.hasDerivAt_planarPrimitive_global line 36
Source documentation
The FTC applies at every point of Omega, including the real axis.
```
theorem hasDerivAt_planarPrimitive_global (m : ℕ) {q t : ℝ}
    (hu : (q : ℂ)+(t : ℂ)*I ∈ Omega) :
    HasDerivAt (planarPrimitive m q) (planarDensity m ((q : ℂ)+(t : ℂ)*I)) t := by
…
```
Mentions: OAI.SymmetricMahler.planarPrimitive, OAI.SymmetricMahler.planarDensity

theorem OAI.SymmetricMahler.planarPrimitive_upper_bound line 44

Source documentation

Uniform bound for the vertical integral on the upper section.

theorem planarPrimitive_upper_bound {m : ℕ} (hm : 2 ≤ m) {q t : ℝ}
    (hu : (q : ℂ)+(t : ℂ)*I ∈ Omega) (ht : 0 ≤ t) :
    planarPrimitive m q t ≤ ‖inverseF ((q : ℂ)+(t : ℂ)*I)‖^(2*(m : ℝ) : ℝ)+planarError m := by
…

Mentions: OAI.SymmetricMahler.planarPrimitive, OAI.SymmetricMahler.planarError

theorem OAI.SymmetricMahler.planarPrimitive_abs_bound line 65
Source documentation
Uniform bound for F, inverseF and the vertical integral: one nonnegative error tends to zero and controls every point of Omega.
```
theorem planarPrimitive_abs_bound {m : ℕ} (hm : 2 ≤ m) {u : ℂ} (hu : u ∈ Omega) :
    |planarPrimitive m u.re u.im| ≤ ‖inverseF u‖^(2*(m : ℝ) : ℝ)+planarError m := by
…
```
Mentions: OAI.SymmetricMahler.planarPrimitive, OAI.SymmetricMahler.planarError