Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(analysis/normed): more lemmas about the sup norm on pi types and matrices #13536

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - feat(analysis/normed): more lemmas about the sup norm on pi types and matrices #13536

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
7379c73
feat(analysis/normed): more lemmas about the sup norm on pi types and…
eric-wieser Apr 20, 2022
22c5bd7
a couple more lemmas
eric-wieser Apr 20, 2022
aa54065
golf
eric-wieser Apr 20, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
50 changes: 44 additions & 6 deletions src/analysis/matrix.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,16 +20,16 @@ of a matrix.

noncomputable theory

open_locale nnreal
open_locale nnreal matrix

namespace matrix

variables {R m n α : Type*} [fintype m] [fintype n]
variables {R m n α β : Type*} [fintype m] [fintype n]

section semi_normed_group
variables [semi_normed_group α]
variables [semi_normed_group α] [semi_normed_group β]

/-- Seminormed group instance (using sup norm of sup norm) for matrices over a seminormed ring. Not
/-- Seminormed group instance (using sup norm of sup norm) for matrices over a seminormed group. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix. -/
protected def semi_normed_group : semi_normed_group (matrix m n α) :=
Expand Down Expand Up @@ -61,9 +61,47 @@ lemma nnnorm_entry_le_entrywise_sup_nnorm (A : matrix m n α) {i : m} {j : n} :
∥A i j∥₊ ≤ ∥A∥₊ :=
(nnnorm_le_pi_nnnorm (A i) j).trans (nnnorm_le_pi_nnnorm A i)

@[simp] lemma nnnorm_transpose (A : matrix m n α) : ∥Aᵀ∥₊ = ∥A∥₊ :=
by { simp_rw [pi.nnnorm_def], exact finset.sup_comm _ _ _ }
@[simp] lemma norm_transpose (A : matrix m n α) : ∥Aᵀ∥ = ∥A∥ := congr_arg coe $ nnnorm_transpose A

@[simp] lemma nnnorm_map_eq (A : matrix m n α) (f : α → β) (hf : ∀ a, ∥f a∥₊ = ∥a∥₊) :
∥A.map f∥₊ = ∥A∥₊ :=
by simp_rw [pi.nnnorm_def, matrix.map, hf]
@[simp] lemma norm_map_eq (A : matrix m n α) (f : α → β) (hf : ∀ a, ∥f a∥ = ∥a∥) :
∥A.map f∥ = ∥A∥ :=
(congr_arg (coe : ℝ≥0 → ℝ) $ nnnorm_map_eq A f $ λ a, subtype.ext $ hf a : _)

@[simp] lemma nnnorm_col (v : m → α) : ∥col v∥₊ = ∥v∥₊ := by simp [pi.nnnorm_def]
@[simp] lemma norm_col (v : m → α) : ∥col v∥ = ∥v∥ := congr_arg coe $ nnnorm_col v

@[simp] lemma nnnorm_row (v : n → α) : ∥row v∥₊ = ∥v∥₊ := by simp [pi.nnnorm_def]
@[simp] lemma norm_row (v : n → α) : ∥row v∥ = ∥v∥ := congr_arg coe $ nnnorm_row v

@[simp] lemma nnnorm_diagonal [decidable_eq n] (v : n → α) : ∥diagonal v∥₊ = ∥v∥₊ :=
begin
simp_rw pi.nnnorm_def,
congr' 1 with i : 1,
refine le_antisymm (finset.sup_le $ λ j hj, _) _,
{ obtain rfl | hij := eq_or_ne i j,
{ rw diagonal_apply_eq },
{ rw [diagonal_apply_ne hij, nnnorm_zero],
exact zero_le _ }, },
{ refine eq.trans_le _ (finset.le_sup (finset.mem_univ i)),
rw diagonal_apply_eq }
end

@[simp] lemma norm_diagonal [decidable_eq n] (v : n → α) : ∥diagonal v∥ = ∥v∥ :=
congr_arg coe $ nnnorm_diagonal v

/-- Note this is safe as an instance as it carries no data. -/
instance [nonempty n] [decidable_eq n] [has_one α] [norm_one_class α] :
norm_one_class (matrix n n α) :=
⟨(norm_diagonal _).trans $ norm_one⟩

end semi_normed_group

/-- Normed group instance (using sup norm of sup norm) for matrices over a normed ring. Not
/-- Normed group instance (using sup norm of sup norm) for matrices over a normed group. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix. -/
protected def normed_group [normed_group α] : normed_group (matrix m n α) :=
Expand All @@ -74,7 +112,7 @@ local attribute [instance] matrix.semi_normed_group

variables [normed_field R] [semi_normed_group α] [normed_space R α]

/-- Normed space instance (using sup norm of sup norm) for matrices over a normed field. Not
/-- Normed space instance (using sup norm of sup norm) for matrices over a normed space. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix. -/
protected def normed_space : normed_space R (matrix m n α) :=
Expand Down
6 changes: 6 additions & 0 deletions src/analysis/normed/group/basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -765,6 +765,12 @@ noncomputable instance pi.semi_normed_group {π : ι → Type*} [fintype ι]
congr_arg (coe : ℝ≥0 → ℝ) $ congr_arg (finset.sup finset.univ) $ funext $ assume a,
show nndist (x a) (y a) = ∥x a - y a∥₊, from nndist_eq_nnnorm _ _ }

lemma pi.norm_def {π : ι → Type*} [fintype ι] [Π i, semi_normed_group (π i)] (f : Π i, π i) :
∥f∥ = ↑(finset.univ.sup (λ b, ∥f b∥₊)) := rfl

lemma pi.nnnorm_def {π : ι → Type*} [fintype ι] [Π i, semi_normed_group (π i)] (f : Π i, π i) :
∥f∥₊ = finset.univ.sup (λ b, ∥f b∥₊) := subtype.eta _ _

/-- The seminorm of an element in a product space is `≤ r` if and only if the norm of each
component is. -/
lemma pi_norm_le_iff {π : ι → Type*} [fintype ι] [∀i, semi_normed_group (π i)] {r : ℝ}
Expand Down
5 changes: 5 additions & 0 deletions src/analysis/normed/normed_field.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -127,6 +127,11 @@ instance prod.norm_one_class [semi_normed_group α] [has_one α] [norm_one_class
norm_one_class (α × β) :=
⟨by simp [prod.norm_def]⟩

instance pi.norm_one_class {ι : Type*} {α : ι → Type*} [nonempty ι] [fintype ι]
[Π i, semi_normed_group (α i)] [Π i, has_one (α i)] [∀ i, norm_one_class (α i)] :
norm_one_class (Π i, α i) :=
⟨by simp [pi.norm_def, finset.sup_const finset.univ_nonempty]⟩

section non_unital_semi_normed_ring
variables [non_unital_semi_normed_ring α]

Expand Down
21 changes: 9 additions & 12 deletions src/analysis/normed_space/star/matrix.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,24 +16,21 @@ This file collects facts about the unitary matrices over `𝕜` (either `ℝ` or

open_locale big_operators matrix

variables {𝕜 n E : Type*}
variables {𝕜 m n E : Type*}

namespace matrix
variables [fintype n] [semi_normed_group E] [star_add_monoid E] [normed_star_group E]
variables [fintype m] [fintype n] [semi_normed_group E] [star_add_monoid E] [normed_star_group E]

local attribute [instance] matrix.semi_normed_group

@[simp] lemma entrywise_sup_norm_star_eq_norm (M : matrix n n E) : ∥star M∥ = ∥M∥ :=
begin
refine le_antisymm (by simp [matrix.norm_le_iff, M.norm_entry_le_entrywise_sup_norm]) _,
refine ((matrix.norm_le_iff (norm_nonneg _)).mpr (λ i j, _)).trans
(congr_arg _ M.star_eq_conj_transpose).ge,
exact (norm_star _).ge.trans Mᴴ.norm_entry_le_entrywise_sup_norm
end
@[simp] lemma norm_conj_transpose (M : matrix m n E) : ∥Mᴴ∥ = ∥M∥ :=
(norm_map_eq _ _ norm_star).trans M.norm_transpose

@[simp] lemma nnnorm_conj_transpose (M : matrix m n E) : ∥Mᴴ∥₊ = ∥M∥₊ :=
subtype.ext M.norm_conj_transpose

@[priority 100] -- see Note [lower instance priority]
instance to_normed_star_group : normed_star_group (matrix n n E) :=
⟨matrix.entrywise_sup_norm_star_eq_norm⟩
instance : normed_star_group (matrix n n E) :=
⟨matrix.norm_conj_transpose⟩

end matrix

Expand Down