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: provide the ℓ² operator norm on matrices #9474

Closed
wants to merge 28 commits into from
Closed

[Merged by Bors] - feat: provide the ℓ² operator norm on matrices #9474

wants to merge 28 commits into from

Conversation

j-loreaux
Copy link
Collaborator

@j-loreaux j-loreaux commented Jan 5, 2024 •
edited

This adds the (unique) C⋆-norm on matrices Matrix n n 𝕜 with IsROrC 𝕜 within the scope Matrix.L2OpNorm. This norm coincides with the operator norm induced by the ℓ² norm (i.e., the norm on Matrix m n 𝕜 obtained by pulling back the norm from EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m). Where possible, we state results for rectangular matrices.

Open in Gitpod

@j-loreaux j-loreaux added awaiting-review The author would like community review of the PR t-analysis Analysis (normed *, calculus) t-algebra Algebra (groups, rings, fields etc) labels Jan 5, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Jan 5, 2024
eric-wieser
eric-wieser reviewed Jan 6, 2024
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you add a comment in Analysis/Matrix (which contains other norms) that notes that this result exists in another file?

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Jan 6, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

j-loreaux and others added 2 commits January 8, 2024 17:00
@j-loreaux
more code review
a965b3f
@j-loreaux @eric-wieser
Update Mathlib/Analysis/InnerProductSpace/Adjoint.lean
3d11ef6 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jan 8, 2024
@eric-wieser
Copy link
Member

Can you add a comment in Analysis/Matrix (which contains other norms) that notes that this result exists in another file?

Can you do this?

eric-wieser
eric-wieser reviewed Jan 8, 2024
View reviewed changes
Mathlib/Analysis/NormedSpace/Star/Matrix.lean Outdated Show resolved Hide resolved
Mathlib/Analysis/NormedSpace/Star/Matrix.lean Outdated Show resolved Hide resolved
Mathlib/Analysis/NormedSpace/Star/Matrix.lean Outdated Show resolved Hide resolved
Mathlib/Analysis/NormedSpace/Star/Matrix.lean Show resolved Hide resolved
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jan 8, 2024
@j-loreaux
Copy link
Collaborator Author

I left a TODO for the diagonal result.

@j-loreaux
Copy link
Collaborator Author

j-loreaux commented Jan 8, 2024 •
edited

I guess there are versions of row and col which should hold too. Earlier I took your question too literally. But let's just leave it be for now.

eric-wieser
eric-wieser approved these changes Jan 8, 2024
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks

bors d+

I think CI wants you to use WithLp.equiv instead of EuclideanSpace.equiv in lemma statements (I agree with it)

Mathlib/Analysis/NormedSpace/Star/Matrix.lean Outdated Show resolved Hide resolved
Mathlib/Analysis/NormedSpace/Star/Matrix.lean Show resolved Hide resolved
@mathlib-bors
Copy link

mathlib-bors bot commented Jan 8, 2024

✌️ j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added delegated and removed awaiting-review The author would like community review of the PR labels Jan 8, 2024
@eric-wieser
Copy link
Member

Note: The C⋆-property actually holds for rectangular matrices too, but we're not including it here for now because we don't have the corresponding statement for continuous linear maps (i.e., between different spaces). In other words, it is possible to show, but we don't yet have it, that for A : E →L[𝕜] F,

#9569 does this generalization, though indeed it doesn't give us access to any of the other CstarRing results, like norm_star.

@j-loreaux j-loreaux changed the title feat: provide the C⋆-norm on square matrices feat: provide the ℓ² operator norm on matrices Jan 9, 2024
@j-loreaux
Copy link
Collaborator Author

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jan 9, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jan 9, 2024
@j-loreaux
feat: provide the ℓ² operator norm on matrices (#9474)
9d2a0f8 
This adds the (unique) C⋆-norm on matrices `Matrix n n 𝕜` with `IsROrC 𝕜` within the scope `Matrix.L2OpNorm`. This norm coincides with the operator norm induced by the ℓ² norm (i.e., the norm on `Matrix m n 𝕜` obtained by pulling back the norm from `EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m`). Where possible, we state results for rectangular matrices.
eric-wieser
eric-wieser reviewed Jan 9, 2024
View reviewed changes
Mathlib/Analysis/NormedSpace/Star/Matrix.lean
Comment on lines +182 to +185
lemma l2_op_norm_conjTranspose (A : Matrix m n 𝕜) : ‖Aᴴ‖ = ‖A‖ := by
rw [l2_op_norm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
toLin_conjTranspose, adjoint_toContinuousLinearMap]
exact ContinuousLinearMap.adjoint.norm_map _
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you add the nnnorm version too?

@mathlib-bors
Copy link

mathlib-bors bot commented Jan 9, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: provide the ℓ² operator norm on matrices [Merged by Bors] - feat: provide the ℓ² operator norm on matrices Jan 9, 2024
@mathlib-bors mathlib-bors bot closed this Jan 9, 2024
@mathlib-bors mathlib-bors bot deleted the j-loreaux/Matrix-CstarNorm branch January 9, 2024 15:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees
No one assigned
Labels
delegated ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields etc) t-analysis Analysis (normed *, calculus)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@j-loreaux @leanprover-community-mathlib4-bot @eric-wieser