[Merged by Bors] - feat(Analysis): add WithLp for products #6136
Conversation
This reverts commit 58c0ff7.
|
I think it would be good to wait until #6409 is merged (or else thrown out), but I'll have an in-depth look after that. |
The motivation is to be able to reuse this for `ProdLp` in #6136. This matches the pattern of how the `Lex` type synonym is used.
bors
bot
changed the base branch from
master
to
ScottCarnahan/BinomialRing2
semorrison
changed the base branch from
ScottCarnahan/BinomialRing2
to
master
j-loreaux
added
awaiting-author
|
@mcdoll if you make this build I am ready to merge it, but please merge master first. |
|
@j-loreaux, I'm not sure how to rectify that comment with your comment above. Do you want to see the L2 lemmas moved back first, or are you happy to merge it either way? |
|
Sorry, that was unclear. I'm ready to merge it modulo moving the lemmas back. |
mcdoll
added
awaiting-review
and removed
awaiting-author
|
✌️ mcdoll can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
The file `NormedSpace.ProdLp` is copied from `NormedSpace.PiLp` with a two changes - For `p = 0` we define the distance by using and if-else block which in turn makes it necessary to add some classicality assumptions - We omit the sections about basis and constant maps Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
The current definition of the distance in `piLp` uses the distance for `p > 0`, but avoids it for `p = 0`. We change the definition for `p = 0` to also have it in terms of the distance, to make sure it is reasonable even when one uses non-Hausdorff spaces.This matches what has been done for `prodLp` in #6136.
The current definition of the distance in `piLp` uses the distance for `p > 0`, but avoids it for `p = 0`. We change the definition for `p = 0` to also have it in terms of the distance, to make sure it is reasonable even when one uses non-Hausdorff spaces.This matches what has been done for `prodLp` in #6136.
The file
NormedSpace.ProdLpis copied fromNormedSpace.PiLpwith a two changesp = 0we define the distance by using and if-else block which in turn makes it necessary to add some classicality assumptionsThe file
InnerProductSpace.ProdL2will contain more things later on, this is also why I importedInnerProductSpace.Projectionsince for the adjoint I need the properties of the orthogonal complement on products.