Commit 2026-03-18 15:17 f86a8b6b

View on Github →

refactor(Analysis/Lp): EuclideanSpace.single -> PiLp.single (#36685) Resolving a TODO in the code. This also makes PiLp.single the simp-normal form, as opposite to toLp _ (Pi.single _ _) that was in the code.

Estimated changes

modified theorem EuclideanSpace.ofLp_single
modified theorem EuclideanSpace.toLp_single
added theorem PiLp.dist_single_same
added theorem PiLp.edist_single_same
added theorem PiLp.nnnorm_single
modified theorem PiLp.nnnorm_toLp_single
added theorem PiLp.norm_single
added theorem PiLp.ofLp_single
added def PiLp.single
added theorem PiLp.single_add
added theorem PiLp.single_apply
added theorem PiLp.single_eq_of_ne'
added theorem PiLp.single_eq_of_ne
added theorem PiLp.single_eq_same
added theorem PiLp.single_neg
added theorem PiLp.single_sub
added theorem PiLp.toLp_single