Minkowski #1000
Merged
Minkowski #1000
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
hoheinzollern
force-pushed
the
minkowski
branch
4 times, most recently
from
a9f7045 to
cb3368e
Compare
hoheinzollern
force-pushed
the
minkowski
branch
from
cb3368e to
72db09d
Compare
hoheinzollern
force-pushed
the
minkowski
branch
from
c131baf to
048badf
Compare
|
Minkowski should also hold with p = 1 |
It does, I just updated the proof. |
hoheinzollern
force-pushed
the
minkowski
branch
2 times, most recently
from
a70eaa8 to
5211206
Compare
hoheinzollern
force-pushed
the
minkowski
branch
from
2a88a17 to
7995997
Compare
|
I tried to simplify the proof after our meeting, but it's impossible to merge the " |
- definition of convex_function - lnorm and equivalence lemma - hoelder for sums - convexity of powR Co-authored-by: Alessandro Bruni <[email protected]>
Co-authored-by: @affeldt-aist
affeldt-aist
force-pushed
the
minkowski
branch
from
7995997 to
5756c76
Compare
| @@ -924,6 +943,21 @@ Qed. | |||
| Lemma poweR_eq0_eq0 x r : 0 <= x -> x `^ r = 0 -> x = 0. | |||
| Proof. by move=> + /eqP => /poweR_eq0-> /andP[/eqP]. Qed. | |||
|
|
|||
| Lemma gt0_ler_poweR (r : R) : (0 <= r)%R -> | |||
| {in `[0, +oo] &, {homo poweR ^~ r : x y / x <= y >-> x <= y}}. | |||
There was a problem hiding this comment.
Maybe we should use Rpos.nneg here? I misread.
theories/hoelder.v
Outdated
| @@ -87,7 +85,15 @@ under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//. | |||
| by rewrite fp//; apply: integral_ge0 => t _; rewrite lee_fin powR_ge0. | |||
| Qed. | |||
|
|
|||
| Lemma Lnorm_powR_K f (p : R) : p != 0%R -> | |||
There was a problem hiding this comment.
This is maybe not a good name, I looked at the proof steps using this lemma but couldn't come with an improvement. :-(
There was a problem hiding this comment.
At least, powR_Lnorm would be better (head symbol goes first).
affeldt-aist
approved these changes
Oct 28, 2023
affeldt-aist
pushed a commit
to affeldt-aist/analysis
that referenced
this pull request
Nov 14, 2023
* Minkowski's inequality and accessory lemmas --------- Co-authored-by: Alessandro Bruni <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]>
proux01
pushed a commit
that referenced
this pull request
Nov 15, 2023
* Minkowski's inequality and accessory lemmas --------- Co-authored-by: Alessandro Bruni <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]>
proux01
added
TODO: MC2 port
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.
Motivation for this change
This PR introduces Minkowski's inequality, a consequence of Hoelder's.
Things done/to do
CHANGELOG_UNRELEASED.mdCompatibility with MathComp 2.0
TODO: HB portto make sure someone ports this PR tothe
hierarchy-builderbranch or I already opened an issue or PR (please cross reference).Automatic note to reviewers
Read this Checklist and put a milestone if possible.