Commit 2023-05-13 03:00 b28404d8

View on Github →

feat: port Analysis.Convex.Gauge (#3942)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Gauge.lean

added theorem Absorbent.gauge_set_nonempty

added theorem Balanced.starConvex

added theorem Convex.gauge_le

added theorem Seminorm.gaugeSeminorm_ball

added theorem exists_lt_of_gauge_lt

added def gauge

added def gaugeSeminorm

added theorem gaugeSeminorm_ball_one

added theorem gaugeSeminorm_lt_one_of_open

added theorem gauge_add_le

added theorem gauge_ball

added theorem gauge_def'

added theorem gauge_def

added theorem gauge_empty

added theorem gauge_le_eq

added theorem gauge_le_of_mem

added theorem gauge_le_one_of_mem

added theorem gauge_lt_eq'

added theorem gauge_lt_eq

added theorem gauge_lt_of_mem_smul

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_mono

added theorem gauge_neg

added theorem gauge_neg_set_eq_gauge_neg

added theorem gauge_neg_set_neg

added theorem gauge_nonneg

added theorem gauge_norm_smul

added theorem gauge_of_subset_zero

added theorem gauge_smul

added theorem gauge_smul_left

added theorem gauge_smul_left_of_nonneg

added theorem gauge_smul_of_nonneg

added theorem gauge_unit_ball

added theorem gauge_zero'

added theorem gauge_zero

added theorem interior_subset_gauge_lt_one

added theorem le_gauge_of_not_mem

added theorem mul_gauge_le_norm

added theorem one_le_gauge_of_not_mem

added theorem self_subset_gauge_le_one