norm_entry_le_norm — Mathlib

English

For any M ∈ CStarMatrix(m,n,A) and indices i ∈ m, j ∈ n, the entry M_{i j} satisfies the inequality ‖M_{i j}‖ ≤ ‖M‖.

Русский

Для любой матрицы M и индексов i, j выполняется неравенство: ‖M_{i j}‖ ≤ ‖M‖.

LaTeX

$$$$\\|M_{ij}\\| \\le \\|M\\|.$$$$

Lean4

theorem norm_entry_le_norm {M : CStarMatrix m n A} {i : m} {j : n} : ‖M i j‖ ≤ ‖M‖ := by
  classical
  suffices ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
    by
    obtain (h | h) := eq_zero_or_norm_pos (M i j)
    · simp [h, norm_def]
    · exact le_of_mul_le_mul_right this h
  rw [← CStarRing.norm_star_mul_self, ← toCLM_apply_single_apply]
  apply norm_apply_le_norm _ _ |>.trans
  apply (toCLM M).le_opNorm _ |>.trans
  simp [norm_def]

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