FiberEndpoint.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Endpoints of the selected global angular fibers.

lemma OAI.SymmetricMahler.eventually_fiberDomain line 13
lemma OAI.SymmetricMahler.fiberAngle_neg line 19
lemma OAI.SymmetricMahler.fiberHeight_neg line 28
theorem OAI.SymmetricMahler.fiberAngle_tendsto_zero line 35
Source documentation
On the actual selected angle, the positive real basepoint has angle limit zero.
```
theorem fiberAngle_tendsto_zero {q r₀ : ℝ} (hr₀ : 0 < r₀) (hr₁ : r₀ < 1)
    (hq0 : 0 ≤ q) (hq : radialMap r₀ = |q|) :
    Tendsto (fiberAngle q) (𝓝[>] r₀) (𝓝 0) := by
…
```
Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.fiberAngle
theorem OAI.SymmetricMahler.fiberHeight_tendsto_at_zero line 75
Source documentation
Zero radius is handled by the norm of the actual polar preimage; no angle at the origin is imposed.
```
theorem fiberHeight_tendsto_at_zero (q : ℝ) :
    Tendsto (fiberHeight q) (𝓝 0) (𝓝 0) := by
…
```
Mentions: OAI.SymmetricMahler.fiberHeight
theorem OAI.SymmetricMahler.fiberHeight_tendsto_basepoint line 86
Source documentation
The endpoint of the selected fiber, including q=0.
```
theorem fiberHeight_tendsto_basepoint {q r₀ : ℝ} (hr₀ : 0 ≤ r₀) (hr₁ : r₀ < 1)
    (hq : radialMap r₀ = |q|) :
    Tendsto (fiberHeight q) (𝓝[>] r₀) (𝓝 0) := by
…
```
Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.fiberHeight