Entrywise bounds for the Euclidean action of a matrix

For a finite rectangular matrix over RCLike 𝕜, the norm of its action on a Euclidean vector is bounded by the largest entry norm times the geometric mean of the row and column counts. For an n × n matrix, this specializes to the constant n * ε. The bounds include matrices with empty row or column types.

Main results

• Matrix.norm_toEuclideanLin_le_of_entry_le: rectangular entrywise-to-action bound.
• Matrix.norm_toEuclideanLin_le_of_entry_le_square: square finite-index specialization.

Source

Adapted from ForTauCeti/Analysis/Matrix/EntrywiseOpNorm.lean in the AIQ-Kitware DKPS formalization (Kitware, Inc.; Apache-2.0).

theorem Matrix.norm_toEuclideanLin_apply_le_of_entry_le {𝕜 : Type u_1} {ι : Type u_2} {κ : Type u_3} [RCLike 𝕜] [Fintype κ] [DecidableEq κ] {A : Matrix ι κ 𝕜} {ε : ℝ} (heps : 0 ≤ ε) (i : ι) (hentry : ∀ (j : κ), ‖A i j‖ ≤ ε) (x : EuclideanSpace 𝕜 κ) : ‖((toEuclideanLin A) x).ofLp i‖ ≤ ε * (√↑(Fintype.card κ) * ‖x‖)

If every entry in row i of a finite matrix is bounded by ε ≥ 0, the i-th coordinate of its Euclidean action has norm at most ε * (√(card κ) * ‖x‖).

theorem Matrix.norm_toEuclideanLin_le_of_entry_le {𝕜 : Type u_1} {ι : Type u_2} {κ : Type u_3} [RCLike 𝕜] [Fintype ι] [Fintype κ] [DecidableEq κ] {A : Matrix ι κ 𝕜} {ε : ℝ} (hentry : ∀ (i : ι) (j : κ), ‖A i j‖ ≤ ε) (x : EuclideanSpace 𝕜 κ) : ‖(toEuclideanLin A) x‖ ≤ √↑(Fintype.card ι) * ε * √↑(Fintype.card κ) * ‖x‖

If every entry of a finite rectangular matrix is bounded by ε, its Euclidean action has norm at most √(card ι) * ε * √(card κ) times the input norm.

Both index types may be empty; in that case the action is zero, even if ε is negative.

theorem Matrix.norm_toEuclideanLin_le_of_entry_le_square {𝕜 : Type u_1} {ι : Type u_2} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] {A : Matrix ι ι 𝕜} {ε : ℝ} (hentry : ∀ (i j : ι), ‖A i j‖ ≤ ε) (x : EuclideanSpace 𝕜 ι) : ‖(toEuclideanLin A) x‖ ≤ ↑(Fintype.card ι) * ε * ‖x‖

The square finite-index form of the entrywise-to-Euclidean operator bound: ‖A x‖ ≤ card ι * ε * ‖x‖ when ‖A i j‖ ≤ ε.