ActualVerticalPrimitive.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SymmetricMahler.verticalRadius line 12
Source documentation
The actual inverse radius in a vertical line of Omega.
```
noncomputable def verticalRadius (q t : ℝ) : ℝ :=
…
```
lemma OAI.SymmetricMahler.sqrt_verticalRadiusSq line 15
theorem OAI.SymmetricMahler.verticalRadius_polar line 20
theorem OAI.SymmetricMahler.hasDerivAt_verticalRadius_polar line 25
theorem OAI.SymmetricMahler.verticalRadius_fiber line 37
theorem OAI.SymmetricMahler.hasDerivAt_verticalRadius_fiber line 44
theorem OAI.SymmetricMahler.hasDerivAt_actual_vertical_primitive line 54
Source documentation
Composition with the actual inverse radius has the prescribed vertical primitive derivative, before taking the endpoint limit and global integral.
```
theorem hasDerivAt_actual_vertical_primitive {q r₀ m r : ℝ} (hm : 2 ≤ m) (hr₀ : 0 ≤ r₀)
    (hq : radialMap r₀ = |q|) (hr : r ∈ Ioo r₀ 1) :
    HasDerivAt (fun t => radialPrimitive q r₀ m (verticalRadius q t))
      ((4*m/Real.pi)*r^(2*m-2 : ℝ) /
        ‖deriv MahlerConformal.F (MahlerConformal.polar r (fiberAngle q r))‖^2)
      (fiberHeight q r) := by
…
```
Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.radialPrimitive, OAI.SymmetricMahler.verticalRadius, OAI.MahlerConformal.F, OAI.MahlerConformal.polar, OAI.SymmetricMahler.fiberAngle, OAI.SymmetricMahler.fiberHeight
lemma OAI.SymmetricMahler.fiber_image_eq line 67
lemma OAI.SymmetricMahler.fiber_image_mem line 74
lemma OAI.SymmetricMahler.inverseF_fiber line 80

theorem OAI.SymmetricMahler.actual_vertical_primitive_derivative line 89

Source documentation

The derivative along the upper fiber, with h and h' being the constructed holomorphic inverse and its derivative.

theorem actual_vertical_primitive_derivative {q r₀ m r : ℝ} (hm : 2 ≤ m) (hr₀ : 0 ≤ r₀)
    (hq : radialMap r₀ = |q|) (hr : r ∈ Ioo r₀ 1) :
    HasDerivAt (fun t => radialPrimitive q r₀ m (verticalRadius q t))
      ((4*m/Real.pi)*
        ‖MahlerConformal.inverseF ((q : ℂ)+(fiberHeight q r : ℂ)*Complex.I)‖^(2*m-2 : ℝ)*
        ‖deriv MahlerConformal.inverseF ((q : ℂ)+(fiberHeight q r : ℂ)*Complex.I)‖^2)
      (fiberHeight q r) := by
…

Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.radialPrimitive, OAI.SymmetricMahler.verticalRadius, OAI.MahlerConformal.inverseF, OAI.SymmetricMahler.fiberHeight

theorem OAI.SymmetricMahler.actual_vertical_primitive_bound line 103
Source documentation
The actual inverse-coordinate primitive has the concrete planar error bound.
```
theorem actual_vertical_primitive_bound {q r₀ m r : ℝ} (hm : 2 ≤ m) (hr₀ : 0 ≤ r₀)
    (hq : radialMap r₀ = |q|) (hr : r ∈ Ioo r₀ 1) :
    radialPrimitive q r₀ m (verticalRadius q (fiberHeight q r)) ≤
      ‖MahlerConformal.inverseF ((q : ℂ)+(fiberHeight q r : ℂ)*Complex.I)‖^(2*m : ℝ)+planarError m := by
…
```
Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.radialPrimitive, OAI.SymmetricMahler.verticalRadius, OAI.SymmetricMahler.fiberHeight, OAI.MahlerConformal.inverseF, OAI.SymmetricMahler.planarError