SourceSphereLimit.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.sphereAnnulus line 11
Source documentation
A fixed closed annulus about the unit sphere.
```
def sphereAnnulus (n : ℕ) : Set (ComplexEuclidean n) :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean
lemma OAI.Mahler.isCompact_sphereAnnulus line 14
lemma OAI.Mahler.sphere_subset_annulus line 17
lemma OAI.Mahler.sphereAnnulus_ne_zero line 22

theorem OAI.Mahler.MassHypotheses.eventually_sphereAnnulus_log_regular line 29

Source documentation

All regularity and positivity for small rescaled points follows from the literal open-domain and isolated-zero hypotheses.

theorem MassHypotheses.eventually_sphereAnnulus_log_regular {k N m : ℕ}
    {U : Set (ComplexEuclidean (k+1))} {f : Fin N → ComplexEuclidean (k+1) → ℂ}
    {G : Fin N → MvPolynomial (Fin (k+1)) ℂ} (h : MassHypotheses (k+1) N m U f G) :
    ∀ᶠ r in 𝓝[>] (0 : ℝ), ∀ z ∈ sphereAnnulus (k+1),
      ContinuousAt (tau f) (r • z) ∧ 0 < tau f (r • z) ∧
      ContDiffAt ℝ 2 (logTau f) (r • z) := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.sphereAnnulus, OAI.Mahler.tau, OAI.Mahler.logTau

theorem OAI.Mahler.MassHypotheses.eventually_rescaledLog_C2 line 60

Source documentation

C^2 regularity of the actual rescaled logarithm; no regularity premise is added to MassHypotheses.

theorem MassHypotheses.eventually_rescaledLog_C2 {k N m : ℕ}
    {U : Set (ComplexEuclidean (k+1))} {f : Fin N → ComplexEuclidean (k+1) → ℂ}
    {G : Fin N → MvPolynomial (Fin (k+1)) ℂ} (h : MassHypotheses (k+1) N m U f G) :
    ∀ᶠ r in 𝓝[>] (0 : ℝ), ∀ z ∈ sphereAnnulus (k+1),
      ContDiffAt ℝ 2 (rescaledLog (tau f) m r) z := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.sphereAnnulus, OAI.Mahler.rescaledLog, OAI.Mahler.tau

theorem OAI.Mahler.MassHypotheses.actual_small_sphere_limit line 73