Theorems · Theorem · functional analysis
summable_norm_sum_mul_antidiagonal_of_summable_norm
∀ {R : Type u_1} [inst : NormedRing R] {f g : ℕ → R},
(Summable fun x => ‖f x‖) →
(Summable fun x => ‖g x‖) → Summable fun n => ‖∑ kl ∈ Finset.HasAntidiagonal.antidiagonal n, f kl.1 * g kl.2‖- Defined in
- Mathlib.Analysis.Normed.Ring.InfiniteSum
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 162 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Norm.normstatement and proof · cited by 5,413
- Finset.sumstatement and proof · cited by 5,195
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- NormedRingstatement and proof · cited by 924
- Summablestatement and proof · cited by 778
- norm_nonnegproof · cited by 725
- Finset.HasAntidiagonal.antidiagonalstatement and proof · cited by 218
- Finset.sum_le_sumproof · cited by 182
- Summable.of_nonneg_of_leproof · cited by 36
- norm_mul_leproof · cited by 31
- norm_sum_leproof · cited by 25
Cited by1
Results whose statement or proof uses this declaration.
- summable_norm_sum_mul_range_of_summable_normproof · cited by 1