Theorems · Theorem · number theory
summableLocallyUniformlyOn_iteratedDerivWithin_cexp
∀ (k : ℕ),
SummableLocallyUniformlyOn
(fun n =>
iteratedDerivWithin k (fun z => Complex.exp (2 * ↑Real.pi * Complex.I * z) ^ n) UpperHalfPlane.upperHalfPlaneSet)
UpperHalfPlane.upperHalfPlaneSetThis is a version of summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp for level one
and q-expansion coefficients all 1.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Realproof · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Filter.Eventuallyproof · cited by 3,134
- one_mulproof · cited by 2,841
- Nat.cast_oneproof · cited by 2,501
- Filter.atTopproof · cited by 2,405
- Nat.cast_zeroproof · cited by 1,870
- Real.pistatement and proof · cited by 1,774
- Complex.ofRealstatement and proof · cited by 1,654
- one_smulproof · cited by 1,374
- pow_oneproof · cited by 894
- Complex.Istatement and proof · cited by 866
Cited by2
Results whose statement or proof uses this declaration.
- iteratedDerivWithin_tsum_cexp_eqproof · cited by 1
- contDiffOn_tsum_cexpproof · cited by 0