[Merged by Bors] - fix(analysis/inner_product_space/pi_L2): add missing type cast functions #18574
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
eric-wieser
added
awaiting-review
4 tasks
eric-wieser
commented
Mar 15, 2023
Comment on lines
-437
to
439
| lemma conj_transpose_eq_adjoint (A : matrix m n 𝕜) : | ||
| to_lin' A.conj_transpose = | ||
| @linear_map.adjoint _ (euclidean_space 𝕜 n) (euclidean_space 𝕜 m) _ _ _ _ _ (to_lin' A) := | ||
| lemma to_euclidean_lin_conj_transpose_eq_adjoint (A : matrix m n 𝕜) : | ||
| A.conj_transpose.to_euclidean_lin = A.to_euclidean_lin.adjoint := | ||
| begin |
There was a problem hiding this comment.
The statement of this lemma was the subject of some discussion in #11551 (comment), and in this Zulip thread.
Note the new version is now consistent with the statement of matrix.is_hermitian_iff_is_symmetric below.
In the year since it was added, there are still no consumers of this lemma.
eric-wieser
commented
Mar 15, 2023
Comment on lines
202
to
204
| lemma is_hermitian_iff_is_symmetric [fintype n] [decidable_eq n] {A : matrix n n α} : | ||
| is_hermitian A ↔ linear_map.is_symmetric | ||
| ((pi_Lp.linear_equiv 2 α (λ _ : n, α)).symm.conj A.to_lin' : module.End α (pi_Lp 2 _)) := | ||
| is_hermitian A ↔ A.to_euclidean_lin.is_symmetric := | ||
| begin |
There was a problem hiding this comment.
This spelling (suggested in #14231 (comment)) was already type-correct, but has been folded into to_euclidean_lin.
YaelDillies
approved these changes
Mar 16, 2023
ocfnash
approved these changes
Mar 17, 2023
leanprover-community-bot-assistant
added
ready-to-merge
|
Note that |
bors bot
pushed a commit
that referenced
this pull request
Mar 17, 2023
…ons (#18574) The preferred way to convert between `ι → 𝕜` and `euclidean_space 𝕜 ι` is via `pi_Lp.equiv`, as this preserves the right typing information. We use the local notation `⟪x, y⟫ₑ` to refer the euclidean inner product of `x y : ι → 𝕜`, which inserts the casting within the notation. This adds a new definition `matrix.to_euclidean_lin` as a shorthand to turn a matrix into a `linear_map` over `euclidean_space`. It also generalizes `inner_matrix_row_row` and `inner_matrix_col_col` away from `fin n` to arbitrary index types.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The preferred way to convert between
ι → 𝕜andeuclidean_space 𝕜 ιis viapi_Lp.equiv, as this preserves the right typing information.We use the local notation
⟪x, y⟫ₑto refer the euclidean inner product ofx y : ι → 𝕜, which inserts the casting within the notation.This adds a new definition
matrix.to_euclidean_linas a shorthand to turn a matrix into alinear_mapovereuclidean_space.It also generalizes
inner_matrix_row_rowandinner_matrix_col_colaway fromfin nto arbitrary index types.Similar to
pi_Lp.equiv#17327