[Merged by Bors] - feat: Hölder framework for `lp` spaces by j-loreaux · Pull Request #35197 · leanprover-community/mathlib4

j-loreaux · 2026-02-12T20:05:06Z

depends on: [Merged by Bors] - feat: add missing API for lp E p #35152
depends on: [Merged by Bors] - feat: generalize Hölder's inequality for sums to Real.HolderTriple #35198

github-actions · 2026-02-12T20:06:17Z

PR summary 7b185b2fb9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.Normed.Lp.lpHolder` (new file)	1874

Declarations diff

+ add_apply
+ bilin_of_top_left
+ bilin_of_top_right
+ bilin_of_zero_left
+ bilin_of_zero_right
+ dualPairing
+ dualPairing_apply
+ holderL
+ holder_gen_bound
+ holder_top_left_bound
+ holder_top_right_bound
+ holderₗ
+ mapCLM
+ neg_apply
+ norm_dualPairing
+ norm_holderL_le
+ norm_mapCLM_le
+ norm_postcomp_le
+ norm_tsumCLM_le
+ nsmul_apply
+ sub_apply
+ unique
+ zero_apply
+ zsmul_apply
++ holder
- PreLp.unique

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 7b185b2fb9
Reference commit 23bafd5167

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

mathlib-merge-conflicts · 2026-02-18T06:15:28Z

This pull request has conflicts, please merge master and resolve them.

…35198) Currently the API exists only for `Real.HolderConjugate`. This generalizes it in anticipation of #35197, which implements the Hölder framework for `lp` spaces.

mathlib-merge-conflicts · 2026-03-18T20:53:36Z

This pull request has conflicts, please merge master and resolve them.

…eanprover-community#35198) Currently the API exists only for `Real.HolderConjugate`. This generalizes it in anticipation of leanprover-community#35197, which implements the Hölder framework for `lp` spaces.

mathlib-dependent-issues · 2026-03-30T21:06:06Z

This PR/issue depends on:

~~[Merged by Bors] - feat: add missing API for lp E p #35152~~
~~[Merged by Bors] - feat: generalize Hölder's inequality for sums to Real.HolderTriple #35198~~
By Dependent Issues (🤖). Happy coding!

mike1729

I found a couple of small nits.

Co-authored-by: Michal Swietek <4404982+mike1729@users.noreply.github.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

mcdoll · 2026-05-17T02:44:25Z

+@[simps!]
+noncomputable def holderₗ (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ} (hBK : ∀ i, ‖B i‖ ≤ K) :
+    lp E p →ₗ[𝕜] lp F q →ₗ[𝕜] lp G r :=
+  .mk₂ 𝕜 (holder r B hBK) ?_ ?_ ?_ ?_ where finally


There is a PR about the convention for where and finally: leanprover-community/leanprover-community.github.io#844
This was my take from the zulip discussion, but if you prefer your current version, then feel free to revive the discussion

dupuisf

Looks good!

bors d+

dupuisf · 2026-06-02T14:16:07Z

+lemma norm_tsumCLM_le {α 𝕜 E : Type*} [NontriviallyNormedField 𝕜]
+    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] :
+    ‖tsumCLM 𝕜 α E‖ ≤ 1 :=


This looks a bit out of place in this file, could we put it in lpSpace instead?

This was discussed earlier in the review comments. Doing so would increase the imports of that file more than I would prefer to do.

mathlib-bors · 2026-06-02T14:25:33Z

✌️ j-loreaux can now approve this pull request until 2026-06-16 14:25 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

j-loreaux · 2026-06-04T21:52:06Z

bors merge

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-bors · 2026-06-04T22:15:22Z

Pull request successfully merged into master.

Build succeeded:

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

j-loreaux added 6 commits February 11, 2026 15:53

feat: add missing API for Memℓp and lp

e7a3415

fix

c2db0e0

more fixes

64df3f4

tsum

04b5866

open scope

788e623

feat: Hölder framework for lp spaces.

0d91bc9

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 12, 2026

j-loreaux mentioned this pull request Feb 12, 2026

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

Closed

loefflerd added the t-analysis Analysis (normed *, calculus) label Feb 14, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 18, 2026

mathlib-merge-conflicts Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 6, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 18, 2026

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 30, 2026

Merge branch 'master' into lpHolder

0ce22fb

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 1, 2026

j-loreaux added 2 commits April 1, 2026 15:39

fixes

db7d96e

add lint exception

be105a5

mathlib-triage Bot assigned loefflerd Apr 3, 2026

loefflerd removed their assignment Apr 3, 2026

mathlib-triage Bot assigned urkud Apr 5, 2026

mike1729 reviewed Apr 21, 2026

View reviewed changes

j-loreaux commented Apr 21, 2026

View reviewed changes

Comment thread Mathlib/Analysis/Normed/Lp/lpHolder.lean Outdated

j-loreaux and others added 2 commits April 21, 2026 16:30

Apply suggestions from code review

9608f03

Co-authored-by: Michal Swietek <4404982+mike1729@users.noreply.github.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

[pre-commit.ci lite] apply automatic fixes

04afd3a

Merge branch 'master' into lpHolder

e8803be

mathlib-triage Bot assigned themathqueen and unassigned urkud May 15, 2026

themathqueen reviewed May 16, 2026

View reviewed changes

Comment thread Mathlib/Analysis/Normed/Lp/lpHolder.lean

themathqueen reviewed May 16, 2026

View reviewed changes

Comment thread Mathlib/Analysis/Normed/Lp/lpHolder.lean Outdated

mcdoll reviewed May 17, 2026

View reviewed changes

mathlib-triage Bot assigned sgouezel and unassigned themathqueen May 31, 2026

j-loreaux added 2 commits June 1, 2026 16:55

rename

4457330

Merge branch 'master' into lpHolder

7b185b2

dupuisf reviewed Jun 2, 2026

View reviewed changes

mathlib-triage Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jun 2, 2026

mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label Jun 4, 2026

mathlib-bors Bot pushed a commit that referenced this pull request Jun 4, 2026

feat: Hölder framework for lp spaces (#35197)

859caf7

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-bors Bot changed the title ~~feat: Hölder framework for lp spaces~~ [Merged by Bors] - feat: Hölder framework for lp spaces Jun 4, 2026

mathlib-bors Bot closed this Jun 4, 2026

ReemMelamed pushed a commit to ReemMelamed/mathlib4 that referenced this pull request Jun 20, 2026

feat: Hölder framework for lp spaces (leanprover-community#35197)

c8d8c58

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Uh oh!

Conversation

j-loreaux commented Feb 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Feb 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 7b185b2fb9

Import changes for modified files

Declarations diff

Uh oh!

mathlib-merge-conflicts Bot commented Feb 18, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Mar 18, 2026

Uh oh!

mathlib-dependent-issues Bot commented Mar 30, 2026

Uh oh!

mike1729 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mcdoll May 17, 2026

Choose a reason for hiding this comment

Uh oh!

dupuisf left a comment

Choose a reason for hiding this comment

Uh oh!

dupuisf Jun 2, 2026

Choose a reason for hiding this comment

Uh oh!

j-loreaux Jun 4, 2026

Choose a reason for hiding this comment

Uh oh!

mathlib-bors Bot commented Jun 2, 2026

Uh oh!

j-loreaux commented Jun 4, 2026

Uh oh!

mathlib-bors Bot commented Jun 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

j-loreaux commented Feb 12, 2026 •

edited

Loading

github-actions Bot commented Feb 12, 2026 •

edited

Loading