Revision #1858 → #2736 · back to history
modifiedFunctional problem (general)a8ec41c25c92
| Field | From #1858 | To #2736 |
|---|
| mathlib.decl | exists_extension_of_le_sublinear | — |
| mathlib.match_kind | exact | — |
| mathlib.module | Mathlib.Analysis.Convex.Cone.Extension | — |
| note | This is the standard Hahn–Banach extension formalized as `exists_extension_of_le_sublinear`. | Helly-style characterization of a continuous linear functional attaining prescribed values; not exposed as a standalone Mathlib lemma. |
| provenance | ai | ai-moderated |
| status | formalized | not_formalized |
modifiedEvery sublinear function is convex29d0e0575ac0
| Field | From #1858 | To #2736 |
|---|
| note | Mathlib lacks an `IsSublinear` predicate but proves `Seminorm.convexOn`, the seminorm special case of the same fact. | Mathlib lacks an `IsSublinear` predicate but proves `Seminorm.convexOn`, the seminorm special case. |
modifiedReal sublinear is seminorm iff symmetric9a645eb5b2cb
| Field | From #1858 | To #2736 |
|---|
| note | Same — without a sublinear-function class this real-case characterization is absent. | Without a sublinear-function class this real-case characterization is absent. |
modifiedHahn–Banach theorem (seminorm version)96398359ae34
| Field | From #1858 | To #2736 |
|---|
| note | Exactly `Module.Dual.exists_extension_of_le_seminorm` for fields satisfying `IsRCLikeNormedField`. | Exactly `Module.Dual.exists_extension_of_le_seminorm` for RCLike fields. |
modifiedOne-dimensional dominated extension lemma1d205e192d61
| Field | From #1858 | To #2736 |
|---|
| note | The one-dimensional step is inlined inside the Zorn argument of `RieszExtension.step`/`exists_extension_of_le_sublinear` and not exposed as a separate lemma. | The one-dimensional step is inlined inside the Zorn argument of `exists_extension_of_le_sublinear` and not exposed as a separate lemma. |
modifiedSeparation of convex sets (locally convex TVS)6fca749fe9f0
| Field | From #1858 | To #2736 |
|---|
| note | Strict separation in a locally convex space is `geometric_hahn_banach_compact_closed` (compact/closed) with companion `geometric_hahn_banach_open` variants. | Strict separation in a locally convex space is `geometric_hahn_banach_compact_closed`. |
modifiedMazur's theorem4a52c02e8fd2
| Field | From #1858 | To #2736 |
|---|
| note | Mazur's theorem on weak closure of convex sets does not appear in Mathlib (only Gelfand–Mazur and Mazur–Ulam exist). | Mazur's theorem on hyperplane containment for a subspace and an open convex set is not formalized as a standalone result in Mathlib. |
modifiedSmooth normed space3b6756ff9d07
| Field | From #1858 | To #2736 |
|---|
| note | The notion of a (point-) smooth normed space (unique supporting functional) is not defined in Mathlib. | The notion of a (point-)smooth normed space (unique supporting functional) is not defined in Mathlib. |
modifiedLinear subspaces characterized by continuous functionalse4461b86f54a
| Field | From #1858 | To #2736 |
|---|
| note | No standalone statement that closed subspaces equal the intersection of zero-sets of continuous functionals appears in Mathlib (only `iInter_halfSpaces_eq` for closed convex sets). | No standalone statement that closed subspaces equal the intersection of zero-sets of continuous functionals appears in Mathlib. |
modifiedCharacterization of reflexive Banach spaces via separation48d49ac3e929
| Field | From #1858 | To #2736 |
|---|
| note | Mathlib has no notion of reflexive Banach space, so this characterization is not formalized. | Mathlib has `Module.IsReflexive` but not this separation-based characterization of reflexivity for real Banach spaces. |
| provenance | ai | ai-moderated |
modifiedHahn–Banach theorem for seminorms42f23592f66a
| Field | From #1858 | To #2736 |
|---|
| mathlib.decl | Module.Dual.exists_extension_of_le_seminorm | — |
| mathlib.match_kind | exact | — |
| mathlib.module | Mathlib.Analysis.LocallyConvex.HahnBanach | — |
| note | `Module.Dual.exists_extension_of_le_seminorm` is the seminorm-bounded extension. | The seminorm-extends-seminorm form is not formalized; Mathlib's `Module.Dual.exists_extension_of_le_seminorm` instead extends a linear functional bounded by a seminorm. |
| provenance | ai | ai-moderated |
| status | formalized | not_formalized |
modifiedVector-valued Hahn–Banach theorem8b5cd8bca526
| Field | From #1858 | To #2736 |
|---|
| note | Only the finite-dimensional-codomain special case is in Mathlib via `ContinuousLinearMap.exist_extension_of_finiteDimensional_range`. | The closest exposed result is the finite-dimensional-codomain continuous-linear case; the plain vector-space statement is not exposed as a single named lemma. |
addedDominated extension holds with convex pb43185a48120