Theorems · Definition · number theory
UpperHalfPlane.cuspFunction
ℝ → (UpperHalfPlane → ℂ) → ℂ → ℂ
The analytic function F such that f τ = F (exp (2 * π * I * τ / h)), extended by a choice of
limit at 0.
- Cited by
- 46 results in Mathlib
- Foundations
- Depth 191 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- OpenPartialHomeomorph.toFun'proof · cited by 745
- UpperHalfPlanestatement and proof · cited by 626
- UpperHalfPlane.ofComplexproof · cited by 59
- Function.Periodic.cuspFunctionproof · cited by 18
Cited by47
Results whose statement or proof uses this declaration.
- UpperHalfPlane.qExpansionproof · cited by 64
- ModularFormClass.analyticAt_cuspFunction_zerostatement · cited by 14
- UpperHalfPlane.qExpansion_coeffstatement and proof · cited by 10
- UpperHalfPlane.eq_cuspFunctionstatement · cited by 4
- UpperHalfPlane.differentiableOn_cuspFunction_ballstatement · cited by 3
- UpperHalfPlane.cuspFunction_apply_zerostatement and proof · cited by 3
- UpperHalfPlane.cuspFunction_negstatement and proof · cited by 2
- UpperHalfPlane.cuspFunction_smulstatement and proof · cited by 2
- UpperHalfPlane.differentiableAt_cuspFunctionstatement · cited by 2
- ModularForm.discriminant_qExpansion_coeff_oneproof · cited by 2
- ModularFormClass.levelOne_neg_weight_eq_zeroproof · cited by 2
- UpperHalfPlane.hasFPowerSeriesOnBall_cuspFunctionstatement and proof · cited by 2