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

Modified src/analysis/seminorm.lean

added theorem absorbent.gauge_set_nonempty

added theorem absorbent.subset

modified def absorbent

modified theorem absorbent_iff_forall_absorbs_singleton

added theorem absorbent_iff_nonneg_lt

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_lt_one_eq_self_of_open

added theorem gauge_lt_one_of_mem_of_open

added theorem gauge_lt_one_subset_self

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 interior_subset_gauge_lt_one

added theorem one_le_gauge_of_not_mem

added theorem self_subset_gauge_le_one

added theorem seminorm.absorbent_ball

added theorem seminorm.absorbent_ball_zero

added theorem seminorm.convex_ball

added theorem seminorm.ext

added theorem seminorm.gauge_ball

added theorem seminorm.gauge_seminorm_ball

added theorem seminorm.symmetric_ball_zero