Commit 2025-08-29 01:08 87e5ad11

View on Github →

feat(MeasureTheory): add Star, InvolutiveStar, and TrivialStar instances for Lp (#28410) This PR introduces the three above instances, aiming toward a CStarAlgebra instance for Linfty.

Estimated changes

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

added theorem MeasureTheory.AEEqFun.eLpNorm_star

added theorem MeasureTheory.eLpNorm_star

Modified Mathlib/MeasureTheory/Function/LpSpace/Basic.lean

added theorem MeasureTheory.Lp.coeFn_star