Theorems · Theorem · number theory

UpperHalfPlane.cuspFunction_apply_zero

∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    AnalyticAt ℂ (UpperHalfPlane.cuspFunction h f) 0 →
      Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
        UpperHalfPlane.cuspFunction h f 0 = UpperHalfPlane.valueAtInfty f

Defined in: Mathlib.NumberTheory.ModularForms.QExpansion
Cited by: 3 results in Mathlib
Foundations: Depth 200 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.

Cites22

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

Realstatement and proof · cited by 25,697
Complexstatement and proof · cited by 5,565
nhdsproof · cited by 5,554
Filter.Tendstoproof · cited by 3,814
Complex.ofRealstatement and proof · cited by 1,654
LT.lt.ne'proof · cited by 1,417
OpenPartialHomeomorph.toFun'statement and proof · cited by 745
UpperHalfPlanestatement and proof · cited by 626
Filter.Tendsto.compproof · cited by 560
AnalyticAtstatement and proof · cited by 321
UpperHalfPlane.coeproof · cited by 288
Function.Periodicstatement and proof · cited by 154

Cited by3

Results whose statement or proof uses this declaration.

UpperHalfPlane.qExpansion_coeff_zeroproof · cited by 2
UpperHalfPlane.exp_decay_sub_atImInftyproof · cited by 2
ModularForm.isZeroAtImInfty_of_valueAtInfty_eq_zeroproof · cited by 1