Commit 2025-01-05 01:44 a5ae6711

View on Github →

feat: shorthand lemmas for the L1 norm (#20383) These are consistent with the existing lemmas about the L2 norm.

Estimated changes

added theorem PiLp.dist_eq_of_L1
modified theorem PiLp.dist_eq_of_L2
added theorem PiLp.edist_eq_of_L1
modified theorem PiLp.edist_eq_of_L2
added theorem PiLp.nndist_eq_of_L1
modified theorem PiLp.nndist_eq_of_L2
added theorem PiLp.nnnorm_eq_of_L1
modified theorem PiLp.nnnorm_eq_of_L2
added theorem PiLp.norm_eq_of_L1
modified theorem PiLp.norm_eq_of_L2