Limits, vanishing, and boundedness at cusps

Mathlib's OnePoint.IsZeroAt and OnePoint.IsBoundedAt are closed under binary sums (OnePoint.IsZeroAt.add, OnePoint.IsBoundedAt.add), but the zero function and a Finset.sum are not recorded. Nor is scaling by a constant: Filter.ZeroAtFilter.smul and Filter.BoundedAtFilter.smul supply that one level down, but carrying them up to the cusp predicate has to cross the σ-twist of ModularForm.smul_slash. This file adds all three.

The gap matters for the Hecke operators, which are finite sums of slashes: a proof that such an operator preserves vanishing at the cusps is an induction over the summands, and without OnePoint.IsZeroAt.sum each call site has to rerun that induction by hand. The scalar half is what the nebentypus twist needs, where each summand carries a character value as its weight.

An upper-triangular slash preserves the filter at infinity and has constant automorphy factor. The limit-transport lemma records this factor, including the conjugation for negative determinant.

Main declarations

• TauCeti.tendsto_slash_atImInfty_of_upperTriangular: the limit of an upper-triangular slash.
• UpperHalfPlane.isZeroAtImInfty_zero: the zero analogue of Mathlib's zero_form_isBoundedAtImInfty, which is absent upstream.
• OnePoint.IsZeroAt.zero, OnePoint.IsBoundedAt.zero: the zero function vanishes, and is bounded, at every point of OnePoint ℝ.
• OnePoint.IsZeroAt.sum, OnePoint.IsBoundedAt.sum: a finite sum of functions vanishing (resp. bounded) at c vanishes (resp. is bounded) at c.
• OnePoint.IsZeroAt.const_smul, OnePoint.IsBoundedAt.const_smul: both properties survive scaling by a constant.

Provenance

No code is transcribed here. The gap the zero and sum lemmas fill was identified from the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0): LeanModularForms/HeckeRIngs/GL2/AdjointTheory.lean lines 62-70, at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08. Its heckeT_p_ut_zero_at_cusps open-codes this induction with Finset.sum_induction, and obtains the base case by constructing a zero CuspForm purely to invoke zero_at_cusps' — because IsZeroAt c 0 k is not stated anywhere. The const_smul pair has a different origin: it is the scalar step the nebentypus-twisted slash sum needs, and is not open-coded in that source. All the statements below are about Mathlib's OnePoint.IsZeroAt/IsBoundedAt, at arbitrary c and k (and, for the sums, an arbitrary index type).

theorem TauCeti.tendsto_slash_atImInfty_of_upperTriangular {f : UpperHalfPlane → ℂ} {c : ℂ} (k : ℤ) (g : GL (Fin 2) ℝ) (hg : ↑g 1 0 = 0) (hf : Filter.Tendsto f UpperHalfPlane.atImInfty (nhds c)) : Filter.Tendsto (SlashAction.map k g f) UpperHalfPlane.atImInfty (nhds ((UpperHalfPlane.σ g) c * ↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k - 1) * ↑(↑g 1 1) ^ (-k)))

An upper-triangular slash carries a limit at infinity to the same limit times its constant automorphy factor, with complex conjugation when the determinant is negative.

@[simp]

theorem UpperHalfPlane.isZeroAtImInfty_zero {α : Type u_1} [Zero α] [TopologicalSpace α] : IsZeroAtImInfty 0

The zero function is zero at im → ∞. This is the missing analogue of Mathlib's zero_form_isBoundedAtImInfty, which covers only the bounded predicate.

@[simp]

theorem OnePoint.IsZeroAt.zero {c : OnePoint ℝ} {k : ℤ} : c.IsZeroAt 0 k

The zero function vanishes at every point of OnePoint ℝ.

@[simp]

theorem OnePoint.IsBoundedAt.zero {c : OnePoint ℝ} {k : ℤ} : c.IsBoundedAt 0 k

The zero function is bounded at every point of OnePoint ℝ.

theorem OnePoint.IsZeroAt.sum {c : OnePoint ℝ} {k : ℤ} {ι : Type u_1} {s : Finset ι} {F : ι → UpperHalfPlane → ℂ} (h : ∀ i ∈ s, c.IsZeroAt (F i) k) : c.IsZeroAt (∑ i ∈ s, F i) k

A finite sum of functions vanishing at c vanishes at c.

theorem OnePoint.IsBoundedAt.sum {c : OnePoint ℝ} {k : ℤ} {ι : Type u_1} {s : Finset ι} {F : ι → UpperHalfPlane → ℂ} (h : ∀ i ∈ s, c.IsBoundedAt (F i) k) : c.IsBoundedAt (∑ i ∈ s, F i) k

A finite sum of functions bounded at c is bounded at c.

theorem OnePoint.IsZeroAt.const_smul {c : OnePoint ℝ} {k : ℤ} {f : UpperHalfPlane → ℂ} (a : ℂ) (hf : c.IsZeroAt f k) : c.IsZeroAt (a • f) k

Vanishing at c survives scaling by a constant.

theorem OnePoint.IsBoundedAt.const_smul {c : OnePoint ℝ} {k : ℤ} {f : UpperHalfPlane → ℂ} (a : ℂ) (hf : c.IsBoundedAt f k) : c.IsBoundedAt (a • f) k

Boundedness at c survives scaling by a constant.