OAI/Analysis/Mahler/GlobalVerticalGeometry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SymmetricMahler.verticalFiber line 16

   Source documentation

   Exact vertical section of the previously constructed conformal image.

   def verticalFiber (q : ℝ) : Set ℝ := {y | (q : ℂ) + (y : ℂ)*I ∈ Omega}

2. lemma OAI.SymmetricMahler.exists_radial_basepoint line 18
3. lemma OAI.SymmetricMahler.fiberHeight_basepoint line 28
4. lemma OAI.SymmetricMahler.continuousOn_fiberHeight_basepoint line 33
5. lemma OAI.SymmetricMahler.strictMonoOn_fiberHeight_basepoint line 44
6. lemma OAI.SymmetricMahler.fiberHeight_pos line 52
7. lemma OAI.SymmetricMahler.fiberHeight_nonneg line 58
8. lemma OAI.SymmetricMahler.zero_mem_verticalFiber line 64
9. lemma OAI.SymmetricMahler.fiberHeight_mem_verticalFiber line 70
10. lemma OAI.SymmetricMahler.verticalFiber_neg line 78
11. lemma OAI.SymmetricMahler.angular_height_mem_image line 82
12. theorem OAI.SymmetricMahler.verticalFiber_eq_images line 105

    Source documentation

    Every image height belongs to the global increasing upper fiber or its reflection.

    theorem verticalFiber_eq_images {q r₀ : ℝ} (hqstrip : q ∈ Ioo (-1 : ℝ) 1)
        (hr₀ : 0 ≤ r₀) (hr₁ : r₀ < 1) (hq : radialMap r₀ = |q|) :
        verticalFiber q = fiberHeight q '' Ico r₀ 1 ∪
          (fun r => -fiberHeight q r) '' Ico r₀ 1 := by
    …

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

13. theorem OAI.SymmetricMahler.verticalFiber_interval line 142

    Source documentation

    The actual global vertical section is an open interval containing zero.

    theorem verticalFiber_interval {q : ℝ} (hq : q ∈ Ioo (-1 : ℝ) 1) :
        IsOpen (verticalFiber q) ∧ OrdConnected (verticalFiber q) ∧ 0 ∈ verticalFiber q := by
    …

    Mentions: OAI.SymmetricMahler.verticalFiber