summable_matrix_diagonal — Mathlib

English

For any f : X → n → R and any summation filter L on X, Summable (x ↦ diag(f(x))) L is equivalent to Summable f L.

Русский

Пусть для любого f: X → n → R и L — фильтр суммирования на X, суммируемость диагонализации эквивалентна суммируемости самой функции: Summable (diag ∘ f) L ⇔ Summable f L.

LaTeX

$$Summable(λ x, diag(f(x)), L) ⇔ Summable(f, L)$$

Lean4

@[simp]
theorem summable_matrix_diagonal [DecidableEq n] {f : X → n → R} :
    (Summable (fun x => diagonal (f x)) L) ↔ Summable f L :=
  Summable.map_iff_of_leftInverse (Matrix.diagonalAddMonoidHom n R) (Matrix.diagAddMonoidHom n R)
    continuous_id.matrix_diagonal continuous_matrix_diag fun A => diag_diagonal A

Похожие утверждения