New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: Conjugate exponents in ℝ≥0
#10589
Conversation
It happens often that we have `p q : ℝ≥0` that are conjugate. So far, we only had a predicate for real numbers to be conjugate, which made dealing with `ℝ≥0` conjugates clumsy. This PR * introduces `NNReal.IsConjExponent`, `NNReal.conjExponent` * renames `Real.IsConjugateExponent`, `Real.conjugateExponent` to `Real.IsConjExponent`, `Real.conjExponent` * renames a few more lemmas to match up the `Real` and `NNReal` versions From LeanAPAP
/-- Two real exponents `p, q` are conjugate if they are `> 1` and satisfy the equality | ||
`1/p + 1/q = 1`. This condition shows up in many theorems in analysis, notably related to `L^p` | ||
norms. -/ | ||
@[mk_iff] | ||
structure IsConjExponent (p q : ℝ) : Prop where |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is there a typeclass that abstracts this? I guess it would be something like OrderedSemifield
... which we probably don't have.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We do have LinearOrderedSemifield
. Do you think that's worth it given that there are exactly two types which we would use this for (namely ℝ
and ℝ≥0
. ℝ≥0∞
is not a linear ordered semifield so would need to be handled separately)?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If it roughly halves the length of this file, then yes I would attempt to use it, I think.
If we can come up with a typeclass that also humours ENNReal
, that would be even better.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I can't, actually. There's too much about tsub
that's not generalised (generalisable?) so that it applies to both Real
and NNReal
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ok, good point.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
It happens often that we have `p q : ℝ≥0` that are conjugate. So far, we only had a predicate for real numbers to be conjugate, which made dealing with `ℝ≥0` conjugates clumsy. This PR * introduces `NNReal.IsConjExponent`, `NNReal.conjExponent` * renames `Real.IsConjugateExponent`, `Real.conjugateExponent` to `Real.IsConjExponent`, `Real.conjExponent` * renames a few more lemmas to match up the `Real` and `NNReal` versions From LeanAPAP
Pull request successfully merged into master. Build succeeded: |
ℝ≥0
ℝ≥0
It happens often that we have `p q : ℝ≥0` that are conjugate. So far, we only had a predicate for real numbers to be conjugate, which made dealing with `ℝ≥0` conjugates clumsy. This PR * introduces `NNReal.IsConjExponent`, `NNReal.conjExponent` * renames `Real.IsConjugateExponent`, `Real.conjugateExponent` to `Real.IsConjExponent`, `Real.conjExponent` * renames a few more lemmas to match up the `Real` and `NNReal` versions From LeanAPAP
It happens often that we have `p q : ℝ≥0` that are conjugate. So far, we only had a predicate for real numbers to be conjugate, which made dealing with `ℝ≥0` conjugates clumsy. This PR * introduces `NNReal.IsConjExponent`, `NNReal.conjExponent` * renames `Real.IsConjugateExponent`, `Real.conjugateExponent` to `Real.IsConjExponent`, `Real.conjExponent` * renames a few more lemmas to match up the `Real` and `NNReal` versions From LeanAPAP
It happens often that we have `p q : ℝ≥0` that are conjugate. So far, we only had a predicate for real numbers to be conjugate, which made dealing with `ℝ≥0` conjugates clumsy. This PR * introduces `NNReal.IsConjExponent`, `NNReal.conjExponent` * renames `Real.IsConjugateExponent`, `Real.conjugateExponent` to `Real.IsConjExponent`, `Real.conjExponent` * renames a few more lemmas to match up the `Real` and `NNReal` versions From LeanAPAP
It happens often that we have `p q : ℝ≥0` that are conjugate. So far, we only had a predicate for real numbers to be conjugate, which made dealing with `ℝ≥0` conjugates clumsy. This PR * introduces `NNReal.IsConjExponent`, `NNReal.conjExponent` * renames `Real.IsConjugateExponent`, `Real.conjugateExponent` to `Real.IsConjExponent`, `Real.conjExponent` * renames a few more lemmas to match up the `Real` and `NNReal` versions From LeanAPAP
It happens often that we have
p q : ℝ≥0
that are conjugate. So far, we only had a predicate for real numbers to be conjugate, which made dealing withℝ≥0
conjugates clumsy.This PR
NNReal.IsConjExponent
,NNReal.conjExponent
Real.IsConjugateExponent
,Real.conjugateExponent
toReal.IsConjExponent
,Real.conjExponent
Real
andNNReal
versionsFrom LeanAPAP