GlobalFiberParametrization.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SymmetricMahler.fiberDomain_eq_Ioo line 12
lemma OAI.SymmetricMahler.F_polar_fiberAngle line 24
theorem OAI.SymmetricMahler.inverseF_fiberHeight line 31
Source documentation
The already proved conformal inverse agrees with the actual global polar choice.
```
theorem inverseF_fiberHeight {q r : ℝ} (hr : r ∈ fiberDomain q) :
    inverseF ((q : ℂ) + (fiberHeight q r : ℂ)*I) = polar r (fiberAngle q r) := by
…
```
Mentions: OAI.SymmetricMahler.fiberDomain, OAI.SymmetricMahler.fiberHeight, OAI.SymmetricMahler.fiberAngle
theorem OAI.SymmetricMahler.norm_inverseF_fiberHeight line 37
theorem OAI.SymmetricMahler.positive_verticalFiber_eq_image line 42
Source documentation
No positive heights are omitted, and no spurious positive heights are added.
```
theorem positive_verticalFiber_eq_image {q r₀ : ℝ} (hqstrip : q ∈ Ioo (-1 : ℝ) 1)
    (hr₀ : 0 ≤ r₀) (hr₁ : r₀ < 1) (hq : radialMap r₀ = |q|) :
    verticalFiber q ∩ Ioi 0 = fiberHeight q '' Ioo r₀ 1 := by
…
```
Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.verticalFiber, OAI.SymmetricMahler.fiberHeight
theorem OAI.SymmetricMahler.fiberHeight_bijOn line 65
theorem OAI.SymmetricMahler.vertical_segment_mem_Omega line 73
Source documentation
The whole integration segment for the vertical primitive belongs to Omega.
```
theorem vertical_segment_mem_Omega {u : ℂ} (hu : u ∈ Omega) {t : ℝ}
    (ht : t ∈ uIcc 0 u.im) : (u.re : ℂ) + (t : ℂ)*I ∈ Omega := by
…
```

theorem OAI.SymmetricMahler.global_vertical_geometry line 86

Source documentation

Global geometry of F, Omega, inverseF and fiberHeight. The fiber endpoints and parametrization give the geometric prerequisites for the radial primitive, without asserting its derivative or bound.

theorem global_vertical_geometry {q : ℝ} (hq : q ∈ Ioo (-1 : ℝ) 1) :
    IsOpen (verticalFiber q) ∧ OrdConnected (verticalFiber q) ∧
    0 ∈ verticalFiber q ∧
    ∃ r₀ ∈ Ico (0 : ℝ) 1, radialMap r₀ = |q| ∧
      fiberDomain q = Ioo r₀ 1 ∧
      StrictMonoOn (fiberHeight q) (Ico r₀ 1) ∧
      BijOn (fiberHeight q) (Ioo r₀ 1) (verticalFiber q ∩ Ioi 0) ∧
      Tendsto (fiberHeight q) (𝓝[>] r₀) (𝓝 0) ∧
      Tendsto (fun r => polar r (fiberAngle q r)) (𝓝[>] r₀)
        (𝓝 (if 0 ≤ q then (r₀ : ℂ) else -(r₀ : ℂ))) ∧
      ∀ r ∈ Ioo r₀ 1, ‖inverseF ((q : ℂ) + (fiberHeight q r : ℂ)*I)‖ = r := by
…

Mentions: OAI.SymmetricMahler.verticalFiber, OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.fiberDomain, OAI.SymmetricMahler.fiberHeight, OAI.SymmetricMahler.fiberAngle