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(analysis/mean_inequalities): Hölder's inequality for infinite sums #11314
Conversation
summable (λ i, f i * g i) ∧ | ||
∑' i, f i * g i ≤ (∑' i, (f i) ^ p) ^ (1 / p) * (∑' i, (g i) ^ q) ^ (1 / q) := |
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.
It would be nice to have two more lemmas which each give one of the terms in this conjunction: one for summable, the other for tsum. Since the proof of both parts is the same, I don't suggest that you break this theorem in two, but rather that you keep this one and add two corollaries.
Same thing for the other summable (...) ∧ ...
theorems
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.
Good idea, done!
LGTM |
Pull request successfully merged into master. Build succeeded: |
State a few versions of Hölder's inequality for infinite sums.
The specific forms of the inequality chosen are parallel to those for Minkowski's inequality in #10984.