Theorems · Theorem · complex analysis
CircleIntegrable.sum
∀ {E : Type u_1} [inst : NormedAddCommGroup E] {c : ℂ} {R : ℝ} {ι : Type u_3} (s : Finset ι) {f : ι → ℂ → E},
(∀ i ∈ s, CircleIntegrable (f i) c R) → CircleIntegrable (∑ i ∈ s, f i) c RSums of circle integrable functions are circle integrable.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 245 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedAddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- NormedAddCommGroupstatement and proof · cited by 15,752
- Finsetstatement and proof · cited by 13,712
- Complexstatement and proof · cited by 5,565
- Finset.sumstatement and proof · cited by 5,195
- Real.piproof · cited by 1,774
- MeasureTheory.MeasureSpace.volumeproof · cited by 1,323
- IntervalIntegrableproof · cited by 316
- Finset.sum_applyproof · cited by 234
- circleMapproof · cited by 117
- CircleIntegrablestatement and proof · cited by 86
- IntervalIntegrable.sumproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- CircleIntegrable.finsumproof · cited by 2
- ValueDistribution.proximity_sum_top_leproof · cited by 2
- CircleIntegrable.fun_sumproof · cited by 1