Commit 2021-11-03 16:10 4f033b7d

View on Github →

feat(analysis/seminorm): define the Minkowski functional (#9097) This defines the gauge of a set, aka the Minkowski functional, in a vector space over a real normed field.

Estimated changes

added theorem absorbent.subset
modified def absorbent
modified def absorbs
added theorem balanced.smul_eq
added theorem balanced.subset_smul
added theorem convex.gauge_le_one
added theorem exists_lt_of_gauge_lt
added def gauge
added theorem gauge_add_le
added theorem gauge_def'
added theorem gauge_def
added theorem gauge_le_of_mem
added theorem gauge_le_one_eq'
added theorem gauge_le_one_eq
added theorem gauge_le_one_of_mem
added theorem gauge_lt_one_eq'
added theorem gauge_lt_one_eq
added theorem gauge_neg
added theorem gauge_nonneg
added def gauge_seminorm
added theorem gauge_smul
added theorem gauge_smul_of_nonneg
added theorem gauge_zero
added theorem seminorm.convex_ball
added theorem seminorm.ext
added theorem seminorm.gauge_ball