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 6cc078933b

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)	1863

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
+ nsmul_apply
+ sub_apply
+ unique
+ zero_apply
+ zsmul_apply
++ holder
- PreLp.unique

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

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>

themathqueen · 2026-05-16T13:02:35Z

+open scoped lp ENNReal NNReal
+
+namespace lp
+-- the material in this section could be moved to `lpSpace`, but would require some extra imports


how heavy are the imports?

themathqueen · 2026-05-16T13:05:13Z

+
+end NontriviallyNormedField
+
+lemma norm_tsumCLM {α 𝕜 E : Type*} [NontriviallyNormedField 𝕜]


I think norm_tsumCLM_le would be better (to match the above naming)

Suggested change

lemma norm_tsumCLM {α 𝕜 E : Type*} [NontriviallyNormedField 𝕜]

lemma norm_tsumCLM_le {α 𝕜 E : Type*} [NontriviallyNormedField 𝕜]

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

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

mcdoll reviewed May 17, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: Hölder framework for `lp` spaces#35197

feat: Hölder framework for `lp` spaces#35197
j-loreaux wants to merge 12 commits into
leanprover-community:masterfrom
j-loreaux:lpHolder

j-loreaux commented Feb 12, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Feb 12, 2026 •

edited

Loading

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

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

themathqueen May 16, 2026

Uh oh!

themathqueen May 16, 2026

Uh oh!

mcdoll May 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants


		end NontriviallyNormedField

		lemma norm_tsumCLM {α 𝕜 E : Type*} [NontriviallyNormedField 𝕜]

	lemma norm_tsumCLM {α 𝕜 E : Type*} [NontriviallyNormedField 𝕜]
	lemma norm_tsumCLM_le {α 𝕜 E : Type*} [NontriviallyNormedField 𝕜]

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 6cc078933b

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!

themathqueen May 16, 2026

Choose a reason for hiding this comment

Uh oh!

themathqueen May 16, 2026

Choose a reason for hiding this comment

Uh oh!

mcdoll May 17, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

j-loreaux commented Feb 12, 2026 •

edited

Loading

github-actions Bot commented Feb 12, 2026 •

edited

Loading