Theorems · Definition · complex analysis
Function.Periodic.cuspFunction
ℝ → (ℂ → ℂ) → ℂ → ℂ
The function q ↦ f (invQParam h q), extended by a non-canonical choice of limit at 0.
- Defined in
- Mathlib.Analysis.Complex.Periodic
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 190 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- Compl.complproof · cited by 2,925
- nhdsWithinproof · cited by 1,912
- Function.updateproof · cited by 502
- Filter.limUnderproof · cited by 47
- Function.Periodic.invQParamproof · cited by 18
Cited by19
Results whose statement or proof uses this declaration.
- UpperHalfPlane.cuspFunctionproof · cited by 46
- Function.Periodic.cuspFunction_eq_of_nonzerostatement · cited by 4
- UpperHalfPlane.eq_cuspFunctionproof · cited by 4
- Function.Periodic.eq_cuspFunctionstatement and proof · cited by 4
- Function.Periodic.cuspFunction_zero_of_zero_at_infstatement · cited by 3
- Function.Periodic.differentiableAt_cuspFunction_zerostatement and proof · cited by 3
- Function.Periodic.cuspFunction_addstatement and proof · cited by 2
- Function.Periodic.cuspFunction_negstatement and proof · cited by 2
- Function.Periodic.cuspFunction_smulstatement and proof · cited by 2
- Function.Periodic.differentiableAt_cuspFunctionstatement and proof · cited by 2
- UpperHalfPlane.exp_decay_sub_atImInftyproof · cited by 2
- Function.Periodic.exp_decay_sub_of_bounded_at_infstatement and proof · cited by 2