[Merged by Bors] - feat(analysis/inner_product_space/projection): remove useless complete_space E assumption
#15682
Conversation
ADedecker
added
the
awaiting-review
| /-- The orthogonal projection is self-adjoint. -/ | ||
| lemma inner_orthogonal_projection_left_eq_right [complete_space E] | ||
| lemma inner_orthogonal_projection_left_eq_right |
There was a problem hiding this comment.
While you're at it, could you please change the statement and lemma name to be in terms of is_self_adjoint?
There was a problem hiding this comment.
The problem is that inner_product_space.is_self_adjoint is defined in analysis/inner_product_space/adjoint, which imports this. Should I remove this version completely and only keep the already existing https://leanprover-community.github.io/mathlib_docs/analysis/inner_product_space/adjoint.html#inner_product_space.orthogonal_projection_is_self_adjoint or should I keep both ?
There was a problem hiding this comment.
We could also make a separate small file for the theory of operators that are inner_product_space.is_self_adjoint-(soon-to-be-renamed-is_symmetric).
There was a problem hiding this comment.
Yes I'd be in favor of having the new is_self_adjoint where the current one is but moving is_symmetric earlier. Shall we put this PR on hold then ?
There was a problem hiding this comment.
I think that having a small file for symmetric operators would be better - I think having is_symmetric in basic is not a good idea since the file is way too large anyways.
Another random remark: golfing complete_space away is nice from the mathlib point of view, but mathematically completely irrelevant since nobody (at least I don't know anyone) cares about non-complete spaces - you always just take the completion and are happy.
There was a problem hiding this comment.
I'm not claiming this is super interesting mathematically. That said, taking the orthogonal projection of a polynomial onto a finite dimensional subset can be useful, right ? Or maybe I'm making things up, I'm not rue 😅
There was a problem hiding this comment.
And imo it makes the proof cleaner anyway
There was a problem hiding this comment.
I am sorry for not being clear, I think this PR is good.
There was a problem hiding this comment.
Oh I didn't take it as being against the PR, don't worry, I just wanted to give my thoughts on the matter.
|
✌️ ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
mathlib-dependent-issues-bot
added
the
blocked-by-other-PR
mathlib-dependent-issues-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
|
What is the current status of the PR? It is delegated, but hasn't been merged yet. |
|
As explained here I wasn't comfortable merging it because when it was finally ready no maintainer had had a look at it for quite some time. If you think it looks good I will merge master to make sure everything still compiles and then merge the PR. |
|
LGTM. Can you merge master, and bors the PR if it builds? |
|
✌️ ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
…te_space E` assumption (#15682) The current proof decomposes v as its projection on K and its projection on the orthogonal complement of K, thus requiring `E` to be complete. Instead, we decompose it as `v = p v + (v - p v)`, where `p` is the projection on K.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
complete_space E assumptioncomplete_space E assumption
…te_space E` assumption (#15682) The current proof decomposes v as its projection on K and its projection on the orthogonal complement of K, thus requiring `E` to be complete. Instead, we decompose it as `v = p v + (v - p v)`, where `p` is the projection on K.
The current proof decomposes v as its projection on K and its projection on the orthogonal complement of K, thus requiring
Eto be complete. Instead, we decompose it asv = p v + (v - p v), wherepis the projection on K.is_self_adjointtois_symmetricand addis_self_adjoint#15326is_symmetricto a new file lower in the import tree #16106