Commit 2025-09-23 06:31 fb1c3596

View on Github →

feat(NumberTheory/ModularForms): integrand for Petersson product (#29640) Define integrand in Petersson product pairing of modular forms, & show its invariance property

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/Basic.lean

Modified Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean

added theorem UpperHalfPlane.σ_conj

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

Modified Mathlib/NumberTheory/ModularForms/Basic.lean

added theorem ModularFormClass.continuous

Created Mathlib/NumberTheory/ModularForms/Petersson.lean

added theorem SlashInvariantFormClass.petersson_smul

added theorem UpperHalfPlane.petersson_continuous

added theorem UpperHalfPlane.petersson_slash

added theorem UpperHalfPlane.petersson_slash_SL