linfty_opNNNorm_eq_opNNNorm — Mathlib

English

Let A be a matrix. The NN-norm of A equals the NN-norm of the associated continuous linear map x ↦ A x, i.e. the operator NN-norm of A as a linear operator coincides with the NN-norm defined entrywise.

Русский

Пусть A — матрица. NN-нормa A равна NN-норме соответствующего непрерывного линейного отображения x ↦ A x; то есть операторная NN-норма матрицы совпадает с NN-нормой по элементам.

LaTeX

$$$\|A\|_{+} = \|\mathrm{ContinuousLinearMap.mk(A\cdot)}\|_{+},$ where $A\cdot$ denotes the linear map $x \mapsto A x$.$$

Lean4

theorem linfty_opNNNorm_eq_opNNNorm (A : Matrix m n α) : ‖A‖₊ = ‖ContinuousLinearMap.mk (Matrix.mulVecLin A)‖₊ :=
  by
  rw [ContinuousLinearMap.opNNNorm_eq_of_bounds _ (linfty_opNNNorm_mulVec _) fun N hN => ?_]
  rw [linfty_opNNNorm_def]
  refine Finset.sup_le fun i _ => ?_
  cases isEmpty_or_nonempty n
  · simp
  classical
  let x : n → α := fun j => unitOf (A i j)
  have hxn : ‖x‖₊ = 1 := by simp_rw [x, Pi.nnnorm_def, norm_unitOf, Finset.sup_const Finset.univ_nonempty]
  specialize hN x
  rw [hxn, mul_one, Pi.nnnorm_def, Finset.sup_le_iff] at hN
  replace hN := hN i (Finset.mem_univ _)
  dsimp [mulVec, dotProduct] at hN
  simp_rw [x, mul_unitOf, ← map_sum, nnnorm_algebraMap, ← NNReal.coe_sum, NNReal.nnnorm_eq, nnnorm_one, mul_one] at hN
  exact hN

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