Skip to content

[Merged by Bors] - feat: generalize Hölder's inequality for sums to Real.HolderTriple#35198

Closed
j-loreaux wants to merge 7 commits into
leanprover-community:masterfrom
j-loreaux:holder-triple-inequalities
Closed

[Merged by Bors] - feat: generalize Hölder's inequality for sums to Real.HolderTriple#35198
j-loreaux wants to merge 7 commits into
leanprover-community:masterfrom
j-loreaux:holder-triple-inequalities

Commits

Commits on Feb 12, 2026

Commits on Feb 20, 2026

Commits on Mar 9, 2026

Commits on Mar 18, 2026