[Merged by Bors] - feat(Analysis/InnerProductSpace/Basic): add PreInnerProductSpace#14024
[Merged by Bors] - feat(Analysis/InnerProductSpace/Basic): add PreInnerProductSpace#14024yoh-tanimoto wants to merge 31 commits intomasterfrom
Conversation
PR summary 5f93724fb7
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Analysis.InnerProductSpace.Basic | 1470 | 1471 | +1 (+0.07%) |
| Mathlib.LinearAlgebra.Matrix.PosDef | 1679 | 1680 | +1 (+0.06%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 247 files with changed transitive imports: this is too many to display! |
Declarations diff
+ PreInnerProductSpace.Core
+ PreInnerProductSpace.toCore
+ cauchy_schwarz_aux'
+ inner_self_of_eq_zero
+ inner_smul_ofReal_left
+ inner_smul_ofReal_right
+ instance (𝕜 : Type*) (F : Type*) [RCLike 𝕜] [AddCommGroup F]
+ instance : InnerProductSpace ℝ ℂ := InnerProductSpace.complexToReal
+ ne_zero_of_inner_self_ne_zero
+ normSq_eq_zero_of_eq_zero
+ re_inner_smul_ofReal_smul_self
+ toPreInner'
+ toSeminormedAddCommGroup
+ toSeminormedSpace
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
|
Well, you should remove the inner product versions for these that are strictly more general, as a first step. @ADedecker do you have thoughts about this preinner product stuff before we get into the weeds of review? |
|
I'm sorry I have absolutely no time to help reviewing this, I'm currently buried under PHD-funding paperwork and the related stress... But I did think about this some time ago, so here are my thoughts. I strongly think the correct approach for the general theory is simply to assume only Of course this trick doesn't work for the "Core" version since it doesn't come with a norm. I am not so sure that it's the correct approach, but I would still say to just remove the definiteness from the definition, and add a Anyway, thanks for working on this! |
|
@j-loreaux @ADedecker I see, I thought this would be a small PR, but instead there seems to be much to do! I probably need some time to do anything reasonable. Meanwhile, if you have comments on how things should be organized, please do so. |
|
I completely agree with Anatole here. I had forgotten we separated out the |
|
I tried, and the first issue is that, since I remove |
|
You should have two |
|
I made two |
|
You can just close the scope for the existing local notation (this might mean moving it into a |
j-loreaux
left a comment
There was a problem hiding this comment.
These are the last corrections. Ping me when you're finished and I'll merge.
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
|
@j-loreaux done! |
|
Can you please merge master, then wait for CI to finish? After that, assuming CI is successful, you're welcome to merge. bors d+ |
|
✌️ yoh-tanimoto can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
) add the structure `PreInnerProductSpace`, which does not assume `definite` for the inner product, with a proof of the Cauchy-Schwarz inequality using the discriminant. Motivation: Such structures arise very often in applications, and by quotienting the kernel one obtains `InnerProductSpace.Core`. I duplicated most of the proofs from the namespace `InnerProductSpace.Core` and put them under the namespace `PreInnerProductSpace` . Is there a better way?
|
Pull request successfully merged into master. Build succeeded: |
) add the structure `PreInnerProductSpace`, which does not assume `definite` for the inner product, with a proof of the Cauchy-Schwarz inequality using the discriminant. Motivation: Such structures arise very often in applications, and by quotienting the kernel one obtains `InnerProductSpace.Core`. I duplicated most of the proofs from the namespace `InnerProductSpace.Core` and put them under the namespace `PreInnerProductSpace` . Is there a better way?
) add the structure `PreInnerProductSpace`, which does not assume `definite` for the inner product, with a proof of the Cauchy-Schwarz inequality using the discriminant. Motivation: Such structures arise very often in applications, and by quotienting the kernel one obtains `InnerProductSpace.Core`. I duplicated most of the proofs from the namespace `InnerProductSpace.Core` and put them under the namespace `PreInnerProductSpace` . Is there a better way?
) add the structure `PreInnerProductSpace`, which does not assume `definite` for the inner product, with a proof of the Cauchy-Schwarz inequality using the discriminant. Motivation: Such structures arise very often in applications, and by quotienting the kernel one obtains `InnerProductSpace.Core`. I duplicated most of the proofs from the namespace `InnerProductSpace.Core` and put them under the namespace `PreInnerProductSpace` . Is there a better way?
…ddCommGroup` (#17007) replace the assumption `NormedAddCommGroup` to `SemiNormedAddCommGroup` in various places. motivation: with the weakened assumption the results apply to `InnerProductSpace` without `definite` assumption. This is suggested in #16707, and continues from #14024. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…ddCommGroup` (#17007) replace the assumption `NormedAddCommGroup` to `SemiNormedAddCommGroup` in various places. motivation: with the weakened assumption the results apply to `InnerProductSpace` without `definite` assumption. This is suggested in #16707, and continues from #14024. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
add the structure
PreInnerProductSpace, which does not assumedefinitefor the inner product, with a proof of the Cauchy-Schwarz inequality using the discriminant.Motivation: Such structures arise very often in applications, and by quotienting the kernel one obtains
InnerProductSpace.Core.I duplicated most of the proofs from the namespace
InnerProductSpace.Coreand put them under the namespacePreInnerProductSpace. Is there a better way?