Theorems · Theorem · number theory

UpperHalfPlane.differentiableAt_cuspFunction

∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
      MDiff f →
        UpperHalfPlane.IsBoundedAtImInfty f →
          ∀ {q : ℂ}, ‖q‖ < 1 → DifferentiableAt ℂ (UpperHalfPlane.cuspFunction h f) q

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

Cites29

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
Norm.normstatement and proof · cited by 5,413
Set.preimageproof · cited by 4,946
Complex.ofRealstatement and proof · cited by 1,654
Set.Ioiproof · cited by 1,463
LT.lt.ne'proof · cited by 1,417
eq_or_neproof · cited by 1,117
modelWithCornersSelfstatement and proof · cited by 920
OpenPartialHomeomorph.toFun'statement and proof · cited by 745
UpperHalfPlanestatement and proof · cited by 626
DifferentiableAtstatement · cited by 617

Cited by2

Results whose statement or proof uses this declaration.

UpperHalfPlane.differentiableOn_cuspFunction_ballproof · cited by 3
ModularFormClass.differentiableAt_cuspFunctionproof · cited by 0