Theorems · Theorem · number theory

UpperHalfPlane.differentiableOn_cuspFunction_ball

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

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

Cites16

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
Complex.ofRealstatement and proof · cited by 1,654
modelWithCornersSelfstatement and proof · cited by 920
OpenPartialHomeomorph.toFun'statement and proof · cited by 745
Metric.ballstatement and proof · cited by 735
UpperHalfPlanestatement and proof · cited by 626
DifferentiableOnstatement · cited by 419
Function.Periodicstatement and proof · cited by 154
MDifferentiablestatement and proof · cited by 134
DifferentiableAt.differentiableWithinAtproof · cited by 96
UpperHalfPlane.ofComplexstatement and proof · cited by 59

Cited by3

Results whose statement or proof uses this declaration.

UpperHalfPlane.analyticAt_cuspFunction_zeroproof · cited by 2
UpperHalfPlane.hasSum_qExpansion_of_norm_ltproof · cited by 2
UpperHalfPlane.qExpansion_coeff_eq_circleIntegralproof · cited by 1