Theorems · Theorem · number theory

UpperHalfPlane.hasSum_qExpansion_of_norm_lt

∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
      MDiff f →
        UpperHalfPlane.IsBoundedAtImInfty f →
          ∀ {q : ℂ},
            ‖q‖ < 1 →
              HasSum (fun m => (PowerSeries.coeff m) (UpperHalfPlane.qExpansion h f) • q ^ m)
                (UpperHalfPlane.cuspFunction h f q)

Defined in: Mathlib.NumberTheory.ModularForms.QExpansion
Cited by: 2 results in Mathlib
Foundations: Depth 291 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites28

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Realstatement and proof · cited by 25,697
TopologicalSpaceproof · cited by 24,529
RingHom.idstatement · cited by 18,349
AddCommMonoidproof · cited by 12,281
LinearMapstatement · cited by 10,215
Complexstatement and proof · cited by 5,565
Norm.normstatement and proof · cited by 5,413
SummationFilter.unconditionalstatement and proof · cited by 2,068
Complex.ofRealstatement and proof · cited by 1,654
modelWithCornersSelfstatement and proof · cited by 920
PowerSeriesstatement · cited by 797

Cited by2

Results whose statement or proof uses this declaration.

UpperHalfPlane.hasSum_qExpansionproof · cited by 2
UpperHalfPlane.qExpansionFormalMultilinearSeries_radiusproof · cited by 0