WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Reflexive space

Revision #1531 → #2467 · back to history

modifiedReflexive space (lead)9314cdefdb26
FieldFrom #1531To #2467
mathlib.decl—Module.IsReflexive
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.Dual.Defs
note—Mathlib has the purely algebraic `Module.IsReflexive` (bijection to double dual as R-modules) but no analytic reflexive locally convex TVS class using the strong bidual topology.
status—partial
modifiedStrong dualb22260e5ba3a
FieldFrom #1531To #2467
mathlib.decl—StrongDual
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
note—`StrongDual 𝕜 E := E →SL[σ] 𝕜` is Mathlib's continuous dual with the strong (operator-norm) topology in the normed setting.
status—formalized
modifiedBidual66e4972c39a4
FieldFrom #1531To #2467
mathlib.decl—StrongDual
mathlib.match_kind—invocation
mathlib.module—Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
note—The bidual `StrongDual 𝕜 (StrongDual 𝕜 E)` is expressible directly by iterating `StrongDual`.
status—formalized
modifiedEvaluation map8e9f0cd73424
FieldFrom #1531To #2467
mathlib.decl—NormedSpace.inclusionInDoubleDual
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Module.DoubleDual
note—`NormedSpace.inclusionInDoubleDual` is the canonical evaluation map into the double strong dual (as a bounded linear map); the algebraic version is `Module.Dual.eval`.
status—formalized
modifiedSemi-reflexive and reflexive TVS5fd8fc0904a4
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib does not have separate `SemiReflexive` / `Reflexive` TVS classes distinguishing bijection of evaluation from being a topological isomorphism.
status—not_formalized
modifiedNormable reflexive iff semi-reflexivec2b8bd2cf73d
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not present: no semi-reflexive/reflexive TVS distinction is formalized in Mathlib.
status—not_formalized
modifiedDual normed spacee66c6463c837
FieldFrom #1531To #2467
mathlib.decl—StrongDual
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
note—For a normed space `E`, `StrongDual 𝕜 E = E →L[𝕜] 𝕜` is the dual normed space with the operator-norm topology.
status—formalized
modifiedBidual normed spacef7c3e7659e02
FieldFrom #1531To #2467
mathlib.decl—StrongDual
mathlib.match_kind—invocation
mathlib.module—Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
note—The bidual `StrongDual 𝕜 (StrongDual 𝕜 E)` is directly available; `NormedSpace.inclusionInDoubleDual` uses it.
status—formalized
modifiedEvaluation map is isometric injection8eb3a6e1c50f
FieldFrom #1531To #2467
mathlib.decl—NormedSpace.inclusionInDoubleDualLi
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Module.DoubleDual
note—`NormedSpace.inclusionInDoubleDualLi` bundles the canonical evaluation as a linear isometry `E →ₗᵢ[𝕜] StrongDual 𝕜 (StrongDual 𝕜 E)`.
status—formalized
modifiedReflexive normed spaced793e43042fb
FieldFrom #1531To #2467
mathlib.decl—Module.IsReflexive
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.Dual.Defs
note—Only the algebraic `Module.IsReflexive` exists; there is no dedicated Mathlib class for a reflexive normed/Banach space via the isometric double-dual embedding being surjective.
status—partial
modifiedReflexive normed space is Banach07b9abe30b10
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Requires a reflexive-normed-space class, which Mathlib does not have.
status—not_formalized
modifiedQuasi-reflexive354b43c24c81
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No quasi-reflexive concept in Mathlib.
status—not_formalized
addedJames' space (non-reflexive, isometric to bidual)d818b8e25004
modifiedFinite-dimensional normed space is reflexive33210b3252cb
FieldFrom #1531To #2467
mathlib.decl—Module.IsReflexive.of_finite_of_free
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.Dual.Lemmas
note—Algebraically finite free modules are `Module.IsReflexive`, but Mathlib has no analytic finite-dim ⇒ reflexive-normed-space statement.
status—partial
modifiedc0, ℓ1, ℓ∞ not reflexive91b7ed73758c
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Non-reflexivity of the classical sequence spaces is not stated in Mathlib.
status—not_formalized
modifiedHilbert and Lp spaces reflexive69516f668d49
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has `InnerProductSpace.toDual` and Lp duality lemmas, but no theorem asserting `Hilbert`/`Lp` are reflexive normed spaces.
status—not_formalized
modifiedMilman–Pettis theorem3ad37e825afa
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—`UniformConvexSpace` exists but the Milman–Pettis theorem (uniform convexity ⇒ reflexivity) is not proved in Mathlib.
status—not_formalized
modifiedL1, L∞, C[0,1] not reflexive7df7e4c27894
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No non-reflexivity results for `L¹`, `L∞`, or `C[0,1]` are in Mathlib.
status—not_formalized
modifiedSchatten class operatorse0262cfcd4ce
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Schatten classes are not defined in Mathlib.
status—not_formalized
modifiedOnly infinite-dim can be non-reflexivead4bdbc4f92d
FieldFrom #1531To #2467
mathlib.decl—Module.instFiniteDimensionalOfIsReflexive
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.Dual.Lemmas
note—Algebraically, `Module.IsReflexive` over a field forces `FiniteDimensional`; no analytic counterpart for reflexive Banach spaces.
status—partial
modifiedIsomorphism preserves reflexivity7eb7e86c0a1c
FieldFrom #1531To #2467
mathlib.decl—LinearEquiv.isReflexive_of_equiv_dual_of_isReflexive
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.PerfectPairing.Basic
note—Reflexivity transports along algebraic linear equivalences (`Module.IsReflexive.equiv`-style lemmas in `Dual/Defs`), but the topological Banach-space version is not.
status—partial
modifiedClosed subspace, dual, quotient of reflexive945ed88b0b9e
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No results on closed-subspace/quotient/dual preservation of Banach-space reflexivity in Mathlib.
status—not_formalized
modifiedReflexive iff dual is reflexivee6cef2da137d
FieldFrom #1531To #2467
mathlib.decl—Module.Dual.instIsReflecive
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.Dual.Defs
note—The algebraic statement that the dual of a reflexive module is reflexive is present; the Banach-space iff-statement is not.
status—partial
modifiedKakutani's theorem6f8f820a8123
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Kakutani's characterization of reflexivity by weak compactness of the unit ball is absent from Mathlib.
status—not_formalized
modifiedBounded sequence has weakly convergent subsequence9a685c53c9ba
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has `WeakDual.isSeqCompact_of_isBounded_of_isClosed` on the weak-* side, but no reflexive-Banach weak sequential compactness theorem.
status—not_formalized
modifiedRiesz's lemma at distance 1c3054c11deb1
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib's `riesz_lemma_of_lt_one` covers only `r<1`; the reflexive-space improvement to `r=1` is not proved.
status—not_formalized
modifiedRiesz lemma example in reflexive Banach9c830b0827b8
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedJames' theorem (functional attains supremum)e6fefcdf03f6
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—James' theorem is absent from Mathlib.
status—not_formalized
modifiedClosed convex sets weakly compact, intersection nonempty9af7614e8ad5
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The reflexive-space consequence for nested closed convex sets is not proved in Mathlib.
status—not_formalized
modifiedClosest point in convex subsetacc260b3a4cd
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib proves best approximation for complete convex sets only in inner-product spaces (`exists_norm_eq_iInf_of_complete_convex`), not for general reflexive Banach spaces.
status—not_formalized
modifiedReflexive separable iff dual separable195555402a44
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not stated in Mathlib.
status—not_formalized
modifiedSuper-reflexive (informal)b7aabb8fbb7c
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Super-reflexivity is not defined in Mathlib.
status—not_formalized
modifiedFinitely representable9178b04344df
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Finite representability of Banach spaces is not formalized.
status—not_formalized
modifiedFinitely representable in ℓ2 is Hilbert787ddf82afbd
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedSuper-reflexive (formal)c1cbd8c27d7c
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No formal super-reflexivity in Mathlib.
status—not_formalized
modifiedJames: super-reflexive iff dual super-reflexiveb5d0a6d02aab
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedVectorial binary tree591e69a59499
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedδ-separated tree40ee4a00af47
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedTree characterization of super-reflexivity69269cbee6df
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedUniformly convex implies super-reflexive2ed7cab7f5fc
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not proved in Mathlib.
status—not_formalized
modifiedEnflo's theorem21c9dd93a006
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Enflo's renorming theorem is not in Mathlib.
status—not_formalized
modifiedPisier's modulus of convexity boundd65bd3bccca9
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedSemi-reflexive and reflexive locally convex2b44b7f945e7
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `SemiReflexive`/`Reflexive` LCS classes in Mathlib.
status—not_formalized
modifiedSemi-reflexive iff Heine–Borel (weak)fa4b831213ac
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedReflexive iff semi-reflexive and barreleda04cf27804bb
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib; `BarrelledSpace` exists but the equivalence is not proved.
status—not_formalized
modifiedStrong dual of semireflexive is barrelled0fb450ab73df
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedCanonical injection topological embedding iff infrabarreledf5a7840a97d0
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Infrabarrelled spaces are not defined in Mathlib.
status—not_formalized
modifiedCharacterizations of semireflexive49179b73b49e
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedCharacterizations of reflexive locally convexa7dd0163cd71
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedCharacterizations of reflexive normed space742453b2b30b
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedSeparation by hyperplane characterizationc4a24ab922f0
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedJames' theorem9a840eb22995
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—James' theorem is not proved in Mathlib.
status—not_formalized
modifiedSemireflexive normed is reflexive Banachc12eefc47b01
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized in Mathlib.
status—not_formalized
modifiedClosed subspace of reflexive Banach reflexive9d039ab496e0
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedThree-space property0702a0391f82
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedBarreled semireflexive implies reflexive684099ca199e
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedStrong dual of reflexive is reflexive; Montel is reflexive70cbd5abd74f
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—`MontelSpace` exists but neither reflexivity of Montel spaces nor stability of reflexivity under strong dual is proved.
status—not_formalized
modifiedReflexive Hausdorff locally convex is barrelled4ff0a4af53f4
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedGoldstine's theorem42b3e849e7bc
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Goldstine's theorem is not in Mathlib.
status—not_formalized
modifiedFinite-dim Hausdorff TVS is reflexivea2fd9b7ba9f3
FieldFrom #1531To #2467
mathlib.decl—Module.IsReflexive.of_finite_of_free
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.Dual.Lemmas
note—Only the algebraic reflexivity of finite free modules is formalized; the topological version for finite-dim Hausdorff TVS is not.
status—partial
modifiedNormed reflexive iff locally convex reflexive45d8994bafe9
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedSemi-reflexive not reflexive (weak topology)29bddf605f1b
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedMontel spaces are reflexivea302d8ec6933
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—`MontelSpace` is defined but not shown reflexive (no reflexive LCS class exists to compare against).
status—not_formalized
modifiedNon-reflexive TVS with reflexive strong dual933847fb9aa2
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedStereotype / polar reflexive space456580e20143
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized
modifiedReflective spaced28f2ad6ca1d
FieldFrom #1531To #2467
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib.
status—not_formalized