frobenius_norm_mul

Mathlib.Analysis.Matrix

URI: https://scilib.ai/kg/mathlib#Matrix.frobenius_norm_mul

English

For matrices A and B of compatible sizes over a complex-like field, the Frobenius norm of AB is at most the product of the Frobenius norms.

Русский

Нормa Фробениуса для произведения AB не превышает произведение норм AB.

LaTeX

$$$\\|AB\\| \\le \\|A\\| \\|B\\|$$$

Lean4

theorem frobenius_norm_mul (A : Matrix l m α) (B : Matrix m n α) : ‖A * B‖ ≤ ‖A‖ * ‖B‖ :=
  frobenius_nnnorm_mul A B

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru