OAI/Analysis/Mahler/FiberPreimageEndpoint.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Polar preimage limits along the vertical fibers.

  1. theorem OAI.SymmetricMahler.fiberAngle_tendsto_pi line 13
  2. theorem OAI.SymmetricMahler.fiberPreimage_tendsto_basepoint line 25

    Source documentation

    The sign convention includes q=0 without imposing an angle at radius zero.

    theorem fiberPreimage_tendsto_basepoint {q r₀ : ℝ} (hr₀ : 0 ≤ r₀) (hr₁ : r₀ < 1)
    (hq : radialMap r₀ = |q|) :
    Tendsto (fun r => polar r (fiberAngle q r)) (𝓝[>] r₀)
      (𝓝 (if 0 ≤ q then (r₀ : ℂ) else -(r₀ : ℂ))) := by
…

    Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.fiberAngle