Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(analysis/normed_space/basic): norm_entry_le_entrywise_sup_norm #12159

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - feat(analysis/normed_space/basic): norm_entry_le_entrywise_sup_norm #12159

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9170395
the entrywise sup norm
hparshall Feb 20, 2022
bfe37ea
Update src/analysis/normed_space/basic.lean
hparshall Feb 21, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions src/analysis/normed_space/basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -789,6 +789,11 @@ def matrix.normed_space {α : Type*} [normed_field α] {n m : Type*} [fintype n]
normed_space α (matrix n m α) :=
pi.normed_space

lemma matrix.norm_entry_le_entrywise_sup_norm {α : Type*} [normed_field α] {n m : Type*} [fintype n]
[fintype m] (M : (matrix n m α)) {i : n} {j : m} :
∥M i j∥ ≤ ∥M∥ :=
(norm_le_pi_norm (M i) j).trans (norm_le_pi_norm M i)

end

end normed_group
Expand Down