Documentation

TauCeti.NumberTheory.LSeries.EntireExtension

The entire-continuation predicate for L-series #

The entire-continuation obligation of Hecke theory, as a predicate on a coefficient sequence a : ℕ → ℂ: LSeries.HasEntireExtension a says the abscissa of absolute convergence is finite and some entire function agrees with LSeries a on the (nonempty) convergence half-plane. Such an extension is unique (LSeries.HasEntireExtension.unique) by analytic continuation.

The predicate comes with introduction lemmas — LSeries.HasEntireExtension.of_extension (agreement on the full convergence half-plane) and the principal LSeries.HasEntireExtension.of_extension_of_eq_on_lt_re (agreement on Re s > c for some real c) — and elimination lemmas (.abscissa_lt_top, .exists_extension), so consumers never unfold the definition. It is exercised: every finitely supported coefficient sequence has an entire extension (LSeries.hasEntireExtension_of_support_finite, with the delta sequence LSeries.hasEntireExtension_delta as the basic instance), and LSeries.HasEntireExtension.existsUnique pins down the unique extension.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/Modularforms/LFunction.lean). This is prerequisite infrastructure: general LSeries API with no modular-forms dependence, supplied ahead of the ModularForms roadmap's Layer-7 entirety/functional-equation obligations, and usable by any Dirichlet-series development.

References #

source
def LSeries.HasEntireExtension (a : ℕ → ℂ) :
Prop

Hecke entire-continuation predicate. A coefficient sequence a : ℕ → ℂ has an entire extension if its abscissa of absolute convergence is finite — so the agreement region below is a genuine half-plane, not vacuously empty — and some entire F : ℂ → ℂ agrees with LSeries a on it. The extension is unique (HasEntireExtension.unique).

Equations
Instances For
    source
    theorem LSeries.HasEntireExtension.of_extension {a : ℕ → ℂ} {F : ℂ → ℂ} (h_finite : abscissaOfAbsConv a < ⊤) (hF : Differentiable ℂ F) (hFa : ∀ {s : ℂ}, abscissaOfAbsConv a < ↑s.re → F s = LSeries a s) :
    HasEntireExtension a

    Introduction lemma for HasEntireExtension: exhibit an entire function agreeing with LSeries a on the absolute-convergence half-plane.

    source
    theorem LSeries.HasEntireExtension.of_extension_of_eq_on_lt_re {a : ℕ → ℂ} {F : ℂ → ℂ} {c : ℝ} (h_finite : abscissaOfAbsConv a < ⊤) (hF : Differentiable ℂ F) (hFa : ∀ {s : ℂ}, c < s.re → F s = LSeries a s) :
    HasEntireExtension a

    Introduction from agreement on any real-cutoff half-plane: if an entire function agrees with LSeries a on Re s > c for some real c, and the abscissa of absolute convergence is finite, then a has an entire extension.

    source
    theorem LSeries.HasEntireExtension.abscissa_lt_top {a : ℕ → ℂ} (h : HasEntireExtension a) :
    abscissaOfAbsConv a < ⊤

    The abscissa of absolute convergence of a sequence with an entire extension is finite.

    source
    theorem LSeries.HasEntireExtension.exists_extension {a : ℕ → ℂ} (h : HasEntireExtension a) :
    ∃ (F : ℂ → ℂ), Differentiable ℂ F ∧ ∀ {s : ℂ}, abscissaOfAbsConv a < ↑s.re → F s = LSeries a s

    Elimination lemma for HasEntireExtension: some entire function agrees with LSeries a on the absolute-convergence half-plane.

    source
    theorem LSeries.HasEntireExtension.unique {a : ℕ → ℂ} {F G : ℂ → ℂ} (hF : Differentiable ℂ F) (hG : Differentiable ℂ G) (h_finite : abscissaOfAbsConv a < ⊤) (hFa : ∀ {s : ℂ}, abscissaOfAbsConv a < ↑s.re → F s = LSeries a s) (hGa : ∀ {s : ℂ}, abscissaOfAbsConv a < ↑s.re → G s = LSeries a s) :
    F = G

    Uniqueness of the entire extension: two entire functions that both extend LSeries a on the absolute-convergence half-plane are equal everywhere on ℂ.

    source
    theorem LSeries.HasEntireExtension.existsUnique {a : ℕ → ℂ} (h : HasEntireExtension a) :
    ∃! F : ℂ → ℂ, Differentiable ℂ F ∧ ∀ ⦃s : ℂ⦄, abscissaOfAbsConv a < ↑s.re → F s = LSeries a s

    The entire extension, as an ∃!: HasEntireExtension pins down a unique entire function agreeing with LSeries a on the convergence half-plane.

    source
    theorem LSeries.hasEntireExtension_of_support_finite {a : ℕ → ℂ} (ha : (Function.support a).Finite) :
    HasEntireExtension a

    Every finitely supported coefficient sequence has an entire extension: the finite sum of its Dirichlet terms is entire and agrees with the L-series everywhere.

    source
    theorem LSeries.hasEntireExtension_delta :
    HasEntireExtension delta

    The delta sequence (the coefficients of the constant Dirichlet series 1) has an entire extension: the predicate is not vacuous.