Commit 2025-04-27 05:05 44f760b7

View on Github →

feat: ‖x i‖ ≤ ‖x‖ for PiLp (#24402)

Estimated changes

Modified Mathlib/Analysis/Normed/Lp/PiLp.lean

added theorem PiLp.dist_apply_le

added theorem PiLp.edist_apply_le

added theorem PiLp.enorm_apply_le

modified theorem PiLp.lipschitzWith_equiv_aux

added theorem PiLp.nndist_apply_le

added theorem PiLp.nnnorm_apply_le

added theorem PiLp.norm_apply_le