Commit 2024-10-12 07:45 52e14c08

View on Github →

feat(HolderNorm): Define the Hölder norm (#16711)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/HolderNorm.lean

added theorem HolderWith.eHolderNorm_le

added theorem HolderWith.memHolder

added theorem HolderWith.nnholderNorm_le

added theorem MemHolder.add

added theorem MemHolder.coe_nnHolderNorm_eq_eHolderNorm

added theorem MemHolder.comp

added theorem MemHolder.holderWith

added theorem MemHolder.nnHolderNorm_add_le

added theorem MemHolder.nnHolderNorm_eq_zero

added theorem MemHolder.nnHolderNorm_nsmul

added theorem MemHolder.nnHolderNorm_smul

added theorem MemHolder.nsmul

added theorem MemHolder.smul

added def MemHolder

added theorem coe_nnHolderNorm_le_eHolderNorm

added def eHolderNorm

added theorem eHolderNorm_add_le

added theorem eHolderNorm_const

added theorem eHolderNorm_eq_top

added theorem eHolderNorm_eq_zero

added theorem eHolderNorm_lt_top

added theorem eHolderNorm_ne_top

added theorem eHolderNorm_nsmul

added theorem eHolderNorm_of_isEmpty

added theorem eHolderNorm_smul

added theorem eHolderNorm_zero

added theorem memHolder_const'

added theorem memHolder_const

added theorem memHolder_iff_holderWith

added theorem memHolder_zero

added def nnHolderNorm

added theorem nnHolderNorm_const

added theorem nnHolderNorm_zero