[Merged by Bors] - feat(MeasureTheory): add Star, InvolutiveStar, and TrivialStar instances for Lp

[JonBannon]

This PR introduces the three above instances, aiming toward a CStarAlgebra instance for Linfty.

---

[github-actions]

PR summary 3b097993a0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ AEEqFun.eLpNorm_star
+ MemLp.star
+ coeFn_star
+ eLpNorm_star
+ instance [TrivialStar R] {p : ℝ≥0∞} : TrivialStar (Lp R p μ)
+ instance {p : ℝ≥0∞} : InvolutiveStar (Lp R p μ)
+ instance {p : ℝ≥0∞} : Star (Lp R p μ)

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

[JonBannon]

Oh man. Super slick.

…

On Thu, Aug 28, 2025, 10:48 AM Jireh Loreaux ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In Mathlib/MeasureTheory/Function/LpSpace/Basic.lean <#28410 (comment)> : > +noncomputable instance {p : ℝ≥0∞} : InvolutiveStar (Lp R p μ) where + star_involutive f := by + ext + filter_upwards + exact congrFun (congrArg AEEqFun.cast <| star_involutive f.1) + +noncomputable instance [TrivialStar R] {p : ℝ≥0∞} : TrivialStar (Lp R p μ) where + star_trivial f := by + ext + filter_upwards + exact congrFun (congrArg AEEqFun.cast <| star_trivial f.1) Here's the right approach: ⬇️ Suggested change -noncomputable instance {p : ℝ≥0∞} : InvolutiveStar (Lp R p μ) where - star_involutive f := by - ext - filter_upwards - exact congrFun (congrArg AEEqFun.cast <| star_involutive f.1) - -noncomputable instance [TrivialStar R] {p : ℝ≥0∞} : TrivialStar (Lp R p μ) where - star_trivial f := by - ext - filter_upwards - exact congrFun (congrArg AEEqFun.cast <| star_trivial f.1) +noncomputable instance {p : ℝ≥0∞} : InvolutiveStar (Lp R p μ) where + star_involutive _ := Subtype.ext <| star_involutive _ + +noncomputable instance [TrivialStar R] {p : ℝ≥0∞} : TrivialStar (Lp R p μ) where + star_trivial _ := Subtype.ext <| star_trivial _ What I was originally suggesting was this: noncomputable instance {p : ℝ≥0∞} : InvolutiveStar (Lp R p μ) where star_involutive f := by ext filter_upwards with x congrm($(star_involutive f.1) x) noncomputable instance [TrivialStar R] {p : ℝ≥0∞} : TrivialStar (Lp R p μ) where star_trivial f := by ext filter_upwards with x congrm($(star_trivial f.1) x) — Reply to this email directly, view it on GitHub <#28410 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AOJJJTRMNCXRC7WTVNVSY233P4JC5AVCNFSM6AAAAACD5FKFNWVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZTCNRVGIYTEMJVGQ> . You are receiving this because you modified the open/close state.Message ID: ***@***.*** com>

[j-loreaux]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• CI Success