[Merged by Bors] - refactor(Analysis/InnerProductSpace/Positive): generalize positivity to use IsSymmetric instead of IsSelfAdjoint and CompleteSpace
#30000
+73
−56
Conversation
This file contains hidden or 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
PR summary 5a6cfc3c42Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
themathqueen
commented
Sep 26, 2025
themathqueen
commented
Sep 27, 2025
j-loreaux
reviewed
Oct 16, 2025
Comment on lines
+234
to
+235
| theorem IsPositive.inner_left_eq_inner_right {T : E →L[𝕜] E} (hT : IsPositive T) (x y : E) : | ||
| ⟪T x, y⟫ = ⟪x, T y⟫ := hT.isSymmetric _ _ |
There was a problem hiding this comment.
Thanks for fixing this to have x y instead of just x! I noticed it was wrong in the diff above.
themathqueen
changed the title
IsSymmetric instead of IsSelfAdjoint and CompleteSpaceIsSymmetric instead of IsSelfAdjoint and CompleteSpace
j-loreaux
reviewed
Oct 17, 2025
leanprover-community-mathlib4-bot
added
the
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Oct 17, 2025
…to use `IsSymmetric` instead of `IsSelfAdjoint` and `CompleteSpace` (#30000) The definition of `ContinuousLinearMap.IsPositive` remains the same in complete spaces, but this allows us to use positivity and the partial order without needing completeness. The new definition is now exactly the same as `LinearMap.IsPositive` but for continuous linear maps. To use the old definition (i.e., `IsSelfAdjoint` and ...), instead of unfolding, use `ContinuousLinearMap.isPositive_def'`. `isPositive_iff` is renamed to `isPositive_iff'`, and `isPositive_iff` points to the same thing but with `IsSymmetric` instead of `IsSelfAdjoint`.
|
Build failed (retrying...): |
|
bors r- I believe you now need to qualify |
|
Canceled. |
|
@j-loreaux can ya bors merge this again :) |
|
bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Oct 17, 2025
…to use `IsSymmetric` instead of `IsSelfAdjoint` and `CompleteSpace` (#30000) The definition of `ContinuousLinearMap.IsPositive` remains the same in complete spaces, but this allows us to use positivity and the partial order without needing completeness. The new definition is now exactly the same as `LinearMap.IsPositive` but for continuous linear maps. To use the old definition (i.e., `IsSelfAdjoint` and ...), instead of unfolding, use `ContinuousLinearMap.isPositive_def'`. `isPositive_iff` is renamed to `isPositive_iff'`, and `isPositive_iff` points to the same thing but with `IsSymmetric` instead of `IsSelfAdjoint`.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
IsSymmetric instead of IsSelfAdjoint and CompleteSpaceIsSymmetric instead of IsSelfAdjoint and CompleteSpace
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
6 participants
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 definition of
ContinuousLinearMap.IsPositiveremains the same in complete spaces, but this allows us to use positivity and the partial order without needing completeness. The new definition is now exactly the same asLinearMap.IsPositivebut for continuous linear maps.To use the old definition (i.e.,
IsSelfAdjointand ...), instead of unfolding, useContinuousLinearMap.isPositive_def'.isPositive_iffis renamed toisPositive_iff', andisPositive_iffpoints to the same thing but withIsSymmetricinstead ofIsSelfAdjoint.