summable_matrix_conjTranspose — Mathlib

English

The equivalence (Summable (f^H) L) ↔ (Summable f L) holds for conjugate transpose.

Русский

Эквивалентность суммируемости транспонированной коньюгатной матрицы и исходной матрицы.

LaTeX

$$$\\text{Summable}(f^H,L) \\iff \\text{Summable}(f,L)$$$

Lean4

@[simp]
theorem summable_matrix_conjTranspose [StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R} :
    (Summable (fun x => (f x)ᴴ) L) ↔ Summable f L :=
  Summable.map_iff_of_equiv (Matrix.conjTransposeAddEquiv m n R) continuous_id.matrix_conjTranspose
    continuous_id.matrix_conjTranspose

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