The Galois product of a periodic function

For f : ℍ → α valued in a commutative monoid and N : ℕ, the product galoisProd N f τ = ∏_{j < N} f(τ − j) over the integer translates — the building block of the modular norm map. If f has period N along ofComplex then the product has period 1. A product of functions bounded at i∞ is bounded at i∞ over any seminormed commutative ring, and for complex-valued holomorphic f the product is holomorphic; when moreover 0 < N, f is bounded and holomorphic, the q-expansion of the product at period 1 has the same order at 0 as that of f at period N.

Main declarations

• TauCeti.ModularForm.galoisProd.
• TauCeti.ModularForm.qExpansion_one_galoisProd_order_eq.

References

• Mathlib PR #39086 (Chris Birkbeck) — the upstream draft this file ports onto the current Mathlib pin.

noncomputable def TauCeti.ModularForm.galoisProd {α : Type u_1} [CommMonoid α] (N : ℕ) (f : UpperHalfPlane → α) (τ : UpperHalfPlane) : α

The product ∏_{j < N} f(τ - j), used as a building block of the norm map.

Equations

• TauCeti.ModularForm.galoisProd N f τ = ∏ j ∈ Finset.range N, f (↑UpperHalfPlane.ofComplex (↑τ - ↑j))

@[simp]

theorem TauCeti.ModularForm.galoisProd_apply {α : Type u_1} [CommMonoid α] {N : ℕ} {f : UpperHalfPlane → α} (τ : UpperHalfPlane) : galoisProd N f τ = ∏ j ∈ Finset.range N, f (↑UpperHalfPlane.ofComplex (↑τ - ↑j))

theorem TauCeti.ModularForm.galoisProd_periodic_one {α : Type u_1} [CommMonoid α] {N : ℕ} {f : UpperHalfPlane → α} (hf_per : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑↑N) : Function.Periodic (galoisProd N f ∘ ↑UpperHalfPlane.ofComplex) 1

If f has period N along ofComplex, then galoisProd N f has period 1.

theorem TauCeti.ModularForm.mdifferentiable_galoisProd {N : ℕ} {f : UpperHalfPlane → ℂ} (hf_mdiff : MDiff f) : MDiff (galoisProd N f)

If f is holomorphic on ℍ, so is galoisProd N f.

theorem TauCeti.ModularForm.isBoundedAtImInfty_galoisProd {R : Type u_1} [SeminormedCommRing R] {N : ℕ} {f : UpperHalfPlane → R} (hf_bdd : UpperHalfPlane.IsBoundedAtImInfty f) : UpperHalfPlane.IsBoundedAtImInfty (galoisProd N f)

If f is bounded at i∞, so is galoisProd N f, over any seminormed commutative ring.

theorem TauCeti.ModularForm.qExpansion_one_galoisProd_order_eq {N : ℕ} {f : UpperHalfPlane → ℂ} (hN : 0 < N) (hf_per : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑↑N) (hf_bdd : UpperHalfPlane.IsBoundedAtImInfty f) (hf_mdiff : MDiff f) : (UpperHalfPlane.qExpansion 1 (galoisProd N f)).order = (UpperHalfPlane.qExpansion (↑N) f).order

The q-expansion of galoisProd N f (period 1) and that of f (period N) have the same order at 0.