Analytic properties of the translate package, and the norm decomposition at ∞ #
For a modular form f, each translate in the package SlashInvariantForm.quotientFunc is
holomorphic, and — when the cusp ∞ is a cusp of ℋ of finite relative index — bounded at
infinity. For 𝒢 of finite relative index in 𝒮ℒ, the norm of f from 𝒢 down to 𝒮ℒ
factors at ∞ as the Galois product of the first Subgroup.integerCuspWidth 𝒢 integer
translates of f times a 1-periodic remainder analytic at ∞.
Main declarations #
TauCeti.SlashInvariantForm.mdifferentiable_quotientFunc.TauCeti.SlashInvariantForm.isBoundedAtImInfty_quotientFunc.TauCeti.ModularForm.normRest, withTauCeti.ModularForm.periodic_normRest,TauCeti.ModularForm.mdifferentiable_normRest,TauCeti.ModularForm.isBoundedAtImInfty_normRestandTauCeti.ModularForm.analyticAt_cuspFunction_normRest.TauCeti.ModularForm.slashInvariantForm_norm_apply_eq_galoisProd_mul_normRest, withTauCeti.ModularForm.norm_apply_eq_galoisProd_mul_normRestas its modular-form corollary.TauCeti.ModularForm.normRest_def: the remainder as a product of coset factors.TauCeti.ModularForm.normRest_apply_eq_div: how to compute the remainder off the zeros of the Galois product.TauCeti.ModularForm.normRest_ne_zero_of_norm_ne_zero, withTauCeti.ModularForm.normRest_ne_zeroas its modular-form corollary: the remainder of a nonzero form is nonzero.TauCeti.ModularForm.qExpansion_one_norm_order_eq: theq-expansion order of the norm at∞splits as the order offplus the order of the remainder.TauCeti.ModularForm.qExpansion_one_normRest_ne_zero: the remainder'sq-expansion is a nonzero power series.
The remainder and the decomposition itself are algebraic, so they are stated for
SlashInvariantForm.norm under SlashInvariantFormClass; only analyticity at the cusp
needs f to be a modular form.
References #
- Mathlib PR #39083 and Mathlib PR #39088 (Chris Birkbeck) — the upstream drafts this file ports onto the current Mathlib pin.
- Mathlib PR #39000
(Chris Birkbeck) — the source of
qExpansion_one_norm_order_eq, whose proof moved here from the Sturm-bound development.
Each translate in the package quotientFunc of a modular form is holomorphic.
Each translate in the package quotientFunc of a modular form is bounded at infinity,
when ∞ is a cusp of ℋ and the relative index is finite.
The algebraic layer #
Everything up to the decomposition itself is a statement about the coset product, so it needs only slash invariance. Analyticity at the cusp is separated out below.
The remainder factor of the norm at the cusp ∞: the product of the coset factors
outside the T-power cosets, so that the norm is the Galois product of the integer
translates of f times this factor.
Under SlashInvariantFormClass alone it is 1-periodic (periodic_normRest) and is
characterised by slashInvariantForm_norm_apply_eq_galoisProd_mul_normRest. Analyticity is the
one property that needs f to be a modular form: see analyticAt_cuspFunction_normRest.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The remainder as a product. normRest f is the product of the coset factors
quotientFunc f q over those q that are not the class of a power of T below the integer
cusp width, for any choice of the finiteness and decidability instances on the coset space.
normRest is 1-periodic.
Decomposition of the norm at the cusp, with the remainder factor named: the norm is
the Galois product of the first Subgroup.integerCuspWidth 𝒢 integer translates of f
times normRest f.
Stated for SlashInvariantForm.norm: the decomposition is algebraic, so it needs only slash
invariance. norm_apply_eq_galoisProd_mul_normRest is the modular-form corollary.
Off the zeros of the Galois product, normRest is the quotient of the norm by that
product: together with the decomposition, this says how to compute normRest at a point with
no reference to the coset indexing used to define it.
Nothing is claimed here about the size of the excluded set — slash invariance alone gives no zero-isolation property.
If the norm does not vanish identically then neither does its remainder factor: the remainder is a factor of the norm, so a vanishing remainder would kill the whole product.
This is the algebraic content; normRest_ne_zero is the modular-form corollary. Order
arguments over normRest need one of the two, since orderOfVanishingAt_prod and the rest
of the vanishing-order API are stated only for factors that are not identically zero.
The analytic layer #
Holomorphy and boundedness of the translates need f to be a modular form.
normRest is holomorphic: it is a product of coset factors, each of which is.
normRest is bounded at ∞: it is a product of coset factors, each of which is.
The cusp function of normRest is analytic at 0.
Decomposition of the norm at the cusp for a modular form: the norm of f from 𝒢
down to 𝒮ℒ is the Galois product of the first Subgroup.integerCuspWidth 𝒢 integer
translates of f times normRest f. This is the form to rewrite with when f is a modular
form; slashInvariantForm_norm_apply_eq_galoisProd_mul_normRest is the general statement.
The remainder factor of a nonzero modular form is itself nonzero: the modular-form
corollary of normRest_ne_zero_of_norm_ne_zero, discharged by ModularForm.norm_ne_zero.
The q-expansion order of the norm at the cusp ∞ splits as the order of f at width
Subgroup.integerCuspWidth 𝒢 plus the order of the remainder factor normRest f.
No discreteness hypothesis is needed here. Discreteness is what converts 𝒢.strictWidthInfty
into Subgroup.integerCuspWidth 𝒢 — see
Subgroup.exists_pos_nat_integerCuspWidth_eq_mul_strictWidthInfty — and that conversion
belongs to the Sturm-bound inequality derived from this identity, not to the identity.
Not @[simp]: ModularForm.coe_norm is itself an unconditional simp lemma, so the
left-hand side is not in simp normal form — it simplifies on to the raw coset product.
The q-expansion of normRest f is a nonzero power series whenever f is nonzero.
This is what makes the order at ∞ of normRest f finite, so that it can appear as a
summand in a cusp-order count.