Commit 2026-09-23 11:38 6a00b6b4

View on Github →

feat(Analysis/Convex): egauge of a seminorm ball (#42846) Prove relations between the seminorm and the egauge of the (closed) ball. This is a step to calculate derivatives of functions with codomain in locally convex spaces.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/TVS.lean

Modified Mathlib/Analysis/Convex/EGauge.lean

added theorem Seminorm.div_le_egauge_ball

added theorem Seminorm.div_le_egauge_closedBall

added theorem Seminorm.egauge_ball_le_of_one_lt_norm

added theorem Seminorm.egauge_unitBall_le_of_one_lt_norm

added theorem Seminorm.le_egauge_unitBall

added theorem Seminorm.le_egauge_unitClosedBall

deleted theorem egauge_ball_one_le_of_one_lt_norm

added theorem egauge_unitBall_le_of_one_lt_norm

deleted theorem le_egauge_ball_one

deleted theorem le_egauge_closedBall_one

added theorem le_egauge_unitBall

added theorem le_egauge_unitClosedBall