SmallSphereLimits.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Mahler.MassHypotheses.small_sphere_surface_integral_limit line 13

Source documentation

The small-sphere limit of Bochner integrals on varying radius spheres, under the mass hypotheses alone.

theorem MassHypotheses.small_sphere_surface_integral_limit {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) :
    Tendsto (radiusSphereFlux k (logTau f)) (𝓝[>] 0)
      (𝓝 (unitSphereFlux k (logTau (polynomialMap G)))) := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.radiusSphereFlux, OAI.Mahler.logTau, OAI.Mahler.unitSphereFlux, OAI.Mahler.polynomialMap

def OAI.Mahler.massSphereFlux line 29
Source documentation
Dimension-indexed surface flux, including an irrelevant zero-dimensional branch.
```
noncomputable def massSphereFlux : (n : ℕ) → (ComplexEuclidean n → ℂ) → ℝ → ℂ
  | 0, _, _ => 0
  | k+1, u, r => radiusSphereFlux k u r
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.radiusSphereFlux
def OAI.Mahler.massUnitSphereFlux line 33
theorem OAI.Mahler.MassHypotheses.mass_small_sphere_limit line 39
Source documentation
The small-sphere limit in the full dimension variable, with the mass hypotheses and no added analytic convergence assumptions.
```
theorem MassHypotheses.mass_small_sphere_limit {n N m : ℕ}
    {U : Set (ComplexEuclidean n)} {f : Fin N → ComplexEuclidean n → ℂ}
    {G : Fin N → MvPolynomial (Fin n) ℂ} (h : MassHypotheses n N m U f G) :
    Tendsto (massSphereFlux n (logTau f)) (𝓝[>] 0)
      (𝓝 (massUnitSphereFlux n (logTau (polynomialMap G)))) := by
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.massSphereFlux, OAI.Mahler.logTau, OAI.Mahler.massUnitSphereFlux, OAI.Mahler.polynomialMap