Cor. 5.0.2 — weak duals of infinite-dimensional Fréchet spaces are not complete
ProvedGarrettFA.not_isNetComplete_weakDual_of_isFrechetSpaceLet be an infinite-dimensional Fréchet space over or , for instance an infinite-dimensional Banach or Hilbert space. Then its weak dual is not complete: some Cauchy net in does not converge.
import Definitions.Def_GarrettFA_IsNetComplete import Definitions.Def_GarrettFA_IsFrechetSpace
namespace GarrettFA
theorem not_isNetComplete_weakDual_of_isFrechetSpace {𝕜 : Type*} [RCLike 𝕜] {X : Type*} [AddCommGroup X] [Module 𝕜 X] [Module ℝ X]
[IsScalarTower ℝ 𝕜 X] [UniformSpace X] [IsUniformAddGroup X] [ContinuousSMul 𝕜 X] [T2Space X]
(hX : IsFrechetSpace 𝕜 X) (hinf : ¬ FiniteDimensional 𝕜 X) :
¬ IsNetComplete (WeakDual 𝕜 X) := by sorry
end GarrettFARead-back
What the Lean code literally says, in plain math · Aristotle (Harmonic)
Let be a real-or-complex scalar field (in practice or ), and let be a -vector space that is also a real vector space with compatible scalar multiplications, carrying a uniform structure for which addition and subtraction are uniformly continuous (so the uniformity is the canonical translation-invariant uniformity of the induced topology), with scalar multiplication jointly continuous, and Hausdorff. Assume is Fréchet and is not finite-dimensional over . Fréchet (the bundle's definition, applied to the given uniform structure): locally convex as a real topological vector space, the topology is metrizable, and the space is complete for its uniform structure (every Cauchy filter converges).
Then the weak dual of (continuous -linear functionals on with the topology of pointwise convergence) is not net-complete. Net-complete (the bundle's definition): for every index type (in the same universe as the space) carrying a partial order in which any two elements have a common upper bound, every family that is Cauchy (for every neighbourhood of there is with for all ) has a point with for all some , for every neighbourhood of . No boundedness is required.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.