[Merged by Bors] - feat: real-valued Lᵖ norm by YaelDillies · Pull Request #23881 · leanprover-community/mathlib4

YaelDillies · 2025-04-09T16:43:05Z

github-actions · 2025-04-09T16:44:09Z

PR summary 4e498b8337

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm` (new file)	2301

Declarations diff

+ ae_le_lpNorm_exponent_top
+ coe_lt_ofReal
+ eLpNorm_eq_lintegral_rpow_enorm_toReal
+ lpNorm
+ lpNorm_abs
+ lpNorm_add_le
+ lpNorm_add_le'
+ lpNorm_conj
+ lpNorm_const
+ lpNorm_const'
+ lpNorm_const_smul
+ lpNorm_div_natCast
+ lpNorm_eq_integral_norm_rpow_toReal
+ lpNorm_eq_zero
+ lpNorm_expect_le
+ lpNorm_exponent_top_eq_essSup
+ lpNorm_exponent_zero
+ lpNorm_fun_abs
+ lpNorm_fun_div_natCast
+ lpNorm_fun_mul_natCast
+ lpNorm_fun_natCast_mul
+ lpNorm_fun_neg
+ lpNorm_fun_zero
+ lpNorm_le_add_lpNorm_add
+ lpNorm_le_lpNorm_add_lpNorm_sub
+ lpNorm_le_lpNorm_add_lpNorm_sub'
+ lpNorm_measure_zero
+ lpNorm_mono_real
+ lpNorm_mul_natCast
+ lpNorm_natCast_mul
+ lpNorm_neg
+ lpNorm_nnreal_eq_integral_norm_rpow
+ lpNorm_nonneg
+ lpNorm_norm
+ lpNorm_nsmul
+ lpNorm_of_isEmpty
+ lpNorm_of_not_aestronglyMeasurable
+ lpNorm_of_not_memLp
+ lpNorm_one
+ lpNorm_one'
+ lpNorm_one_eq_integral_norm
+ lpNorm_smul_measure_of_ne_top
+ lpNorm_smul_measure_of_ne_zero
+ lpNorm_sub_comm
+ lpNorm_sub_le
+ lpNorm_sub_le_lpNorm_sub_add_lpNorm_sub
+ lpNorm_sum_le
+ lpNorm_zero
+ ofReal_essSup
+ ofReal_limsup
+ ofReal_lpNorm
+ toReal_eLpNorm
+ toReal_essSup
+ toReal_limsup
- eLpNorm_eq_lintegral_rpow_enorm

You can run this locally as follows

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

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

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

No changes to technical debt.

You can run this locally as

./scripts/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).

leanprover-community-bot-assistant · 2025-04-15T13:38:50Z

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

b-mehta

This looks reasonable enough to me, but I'd like an analyst to check too.

maintainer merge

github-actions · 2025-04-15T13:47:16Z

🚀 Pull request has been placed on the maintainer queue by b-mehta.

sgouezel

I'm not completely sure I am convinced by the PR: one lesson from Carleson is that when you formalize analysis, you need the ennreal-valued norms, and the real-valued norms. Can you explain why you think the nnreal valued version is more important than the real-valued?

sgouezel · 2025-04-22T12:29:10Z

+variable {α E : Type*} {m : MeasurableSpace α} {p : ℝ≥0∞} {q : ℝ} {μ ν : Measure α}
+  [NormedAddCommGroup E] {f g h : α → E}
+
+lemma coe_nnLpNorm_eq_eLpNorm (hf : MemLp f p μ) : nnLpNorm f p μ = eLpNorm f p μ := by


Do you think the MemLp assumption will be inferrable in practice?

leanprover-community-bot-assistant · 2025-05-13T14:11:30Z

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

leanprover-community-bot-assistant · 2025-07-16T15:33:28Z

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

mathlib4-merge-conflict-bot · 2025-08-18T14:14:16Z

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

mathlib4-merge-conflict-bot · 2025-11-19T07:43:18Z

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

sgouezel · 2026-02-09T07:28:42Z

bors r+
Thanks!

mathlib-bors · 2026-02-09T07:57:07Z

Pull request successfully merged into master.

Build succeeded:

From leanprover-community#23881.

…35203) From #23881.

…eanprover-community#35203) From leanprover-community#23881.

YaelDillies requested a review from b-mehta April 9, 2025 16:43

github-actions bot added the t-measure-probability Measure theory / Probability theory label Apr 9, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 15, 2025

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 15, 2025

b-mehta reviewed Apr 15, 2025

View reviewed changes

Comment thread Mathlib/MeasureTheory/Function/LpSeminorm/NNLpNorm.lean Outdated

Comment thread Mathlib/MeasureTheory/Function/LpSeminorm/Defs.lean Outdated

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 15, 2025

sgouezel reviewed Apr 17, 2025

View reviewed changes

Comment thread Mathlib/MeasureTheory/Function/LpSeminorm/NNLpNorm.lean Outdated

Comment thread Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean Outdated

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 17, 2025

YaelDillies removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 18, 2025

sgouezel reviewed Apr 22, 2025

View reviewed changes

sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 23, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 13, 2025

YaelDillies force-pushed the nnlpnorm branch from febf5db to 2b0d44c Compare May 14, 2025 09:51

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 May 14, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 16, 2025

YaelDillies force-pushed the nnlpnorm branch from 2cc2a1f to 1af6a09 Compare July 17, 2025 07:09

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 17, 2025

mathlib4-merge-conflict-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 Aug 18, 2025

YaelDillies force-pushed the nnlpnorm branch from 1af6a09 to 8195db9 Compare August 18, 2025 14:21

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 Aug 18, 2025

mathlib4-merge-conflict-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 Nov 19, 2025

YaelDillies force-pushed the nnlpnorm branch from 8195db9 to 7be37b8 Compare November 19, 2025 10:58

YaelDillies removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 5, 2026

sgouezel reviewed Feb 7, 2026

View reviewed changes

sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 7, 2026

weaken

ce912c2

YaelDillies removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 8, 2026

YaelDillies added 4 commits February 8, 2026 11:41

better

a439809

other junk value

1be872f

better

32caa06

better

ded3fac

sgouezel reviewed Feb 8, 2026

View reviewed changes

Comment thread Mathlib/Order/Filter/ENNReal.lean Outdated

one fewer assumption

583098b

mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Feb 9, 2026

mathlib-bors bot pushed a commit that referenced this pull request Feb 9, 2026

feat: real-valued Lᵖ norm (#23881)

507f18f

mathlib-bors bot changed the title ~~feat: real-valued Lᵖ norm~~ [Merged by Bors] - feat: real-valued Lᵖ norm Feb 9, 2026

mathlib-bors bot closed this Feb 9, 2026

mathlib-bors bot deleted the nnlpnorm branch February 9, 2026 07:57

justus-springer pushed a commit to justus-springer/mathlib4 that referenced this pull request Feb 10, 2026

feat: real-valued Lᵖ norm (leanprover-community#23881)

59b0bd6

Ruben-VandeVelde added a commit to Ruben-VandeVelde/mathlib4 that referenced this pull request Feb 12, 2026

chore: add missing deprecation for eLpNorm_eq_lintegral_rpow_enorm

da48442

From leanprover-community#23881.

Ruben-VandeVelde mentioned this pull request Feb 12, 2026

[Merged by Bors] - chore: add missing deprecation for eLpNorm_eq_lintegral_rpow_enorm #35203

Closed

mathlib-bors bot pushed a commit that referenced this pull request Feb 12, 2026

chore: add missing deprecation for eLpNorm_eq_lintegral_rpow_enorm (#…

5264399

…35203) From #23881.

kim-em pushed a commit to kim-em/mathlib4 that referenced this pull request Feb 14, 2026

chore: add missing deprecation for eLpNorm_eq_lintegral_rpow_enorm (l…

d8306f1

…eanprover-community#35203) From leanprover-community#23881.

michaellee94 pushed a commit to michaellee94/mathlib4 that referenced this pull request Feb 15, 2026

feat: real-valued Lᵖ norm (leanprover-community#23881)

b959f19

rao107 pushed a commit to rao107/mathlib4 that referenced this pull request Feb 18, 2026

feat: real-valued Lᵖ norm (leanprover-community#23881)

83e6f82

rao107 pushed a commit to rao107/mathlib4 that referenced this pull request Feb 18, 2026

chore: add missing deprecation for eLpNorm_eq_lintegral_rpow_enorm (l…

a19b094

…eanprover-community#35203) From leanprover-community#23881.

Maldooor pushed a commit to Maldooor/mathlib4 that referenced this pull request Feb 25, 2026

feat: real-valued Lᵖ norm (leanprover-community#23881)

614d739

Maldooor pushed a commit to Maldooor/mathlib4 that referenced this pull request Feb 25, 2026

chore: add missing deprecation for eLpNorm_eq_lintegral_rpow_enorm (l…

8635778

…eanprover-community#35203) From leanprover-community#23881.

pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Mar 2, 2026

feat: real-valued Lᵖ norm (leanprover-community#23881)

37bb2fc

pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Mar 2, 2026

chore: add missing deprecation for eLpNorm_eq_lintegral_rpow_enorm (l…

5d18990

…eanprover-community#35203) From leanprover-community#23881.

Conversation

YaelDillies commented Apr 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Apr 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 4e498b8337

Import changes for modified files

Declarations diff

Uh oh!

leanprover-community-bot-assistant commented Apr 15, 2025

Uh oh!

b-mehta left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Apr 15, 2025

Uh oh!

Uh oh!

Uh oh!

sgouezel left a comment

Choose a reason for hiding this comment

Uh oh!

sgouezel Apr 22, 2025

Choose a reason for hiding this comment

Uh oh!

YaelDillies Feb 5, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

leanprover-community-bot-assistant commented May 13, 2025

Uh oh!

leanprover-community-bot-assistant commented Jul 16, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Aug 18, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sgouezel commented Feb 9, 2026

Uh oh!

mathlib-bors bot commented Feb 9, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

YaelDillies commented Apr 9, 2025 •

edited

Loading

github-actions bot commented Apr 9, 2025 •

edited

Loading