Commit 2022-08-09 09:08 a88bc4f7

View on Github →

feat(analysis/convex): the gauge as a seminorm over is_R_or_C (#14879) Constructs the gauge for a set on a vector spaces over is_R_or_C assuming that the set is convex, balanced and absorbing. The main part of this PR is to show that if a set is balanced then the corresponding gauge has the correct scaling behavior.

Estimated changes

Modified src/analysis/convex/gauge.lean

added theorem gauge_norm_smul

modified def gauge_seminorm

modified theorem gauge_smul

Modified src/analysis/locally_convex/basic.lean

added theorem balanced_iff_neg_mem

Modified src/data/complex/is_R_or_C.lean

added theorem is_R_or_C.real_smul_eq_coe_mul

added theorem is_R_or_C.real_smul_eq_coe_smul