diff --git a/Mathlib.lean b/Mathlib.lean index c21c7fbff44e6e..1b3ebf1d246d05 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1997,7 +1997,7 @@ public import Mathlib.Analysis.LocallyConvex.Polar public import Mathlib.Analysis.LocallyConvex.SeparatingDual public import Mathlib.Analysis.LocallyConvex.Separation public import Mathlib.Analysis.LocallyConvex.StrongTopology -public import Mathlib.Analysis.LocallyConvex.WeakDual +public import Mathlib.Analysis.LocallyConvex.WeakBilin public import Mathlib.Analysis.LocallyConvex.WeakOperatorTopology public import Mathlib.Analysis.LocallyConvex.WeakSpace public import Mathlib.Analysis.LocallyConvex.WithSeminorms @@ -7317,6 +7317,7 @@ public import Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM public import Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM public import Mathlib.Topology.Algebra.Module.Spaces.WeakBilin public import Mathlib.Topology.Algebra.Module.Spaces.WeakDual +public import Mathlib.Topology.Algebra.Module.Spaces.WeakSpace public import Mathlib.Topology.Algebra.Module.Star public import Mathlib.Topology.Algebra.Module.StrongTopology public import Mathlib.Topology.Algebra.Module.TopDualPairing diff --git a/Mathlib/Analysis/LocallyConvex/WeakDual.lean b/Mathlib/Analysis/LocallyConvex/WeakBilin.lean similarity index 98% rename from Mathlib/Analysis/LocallyConvex/WeakDual.lean rename to Mathlib/Analysis/LocallyConvex/WeakBilin.lean index 2e681cc7c9ceb5..f6af0f65face71 100644 --- a/Mathlib/Analysis/LocallyConvex/WeakDual.lean +++ b/Mathlib/Analysis/LocallyConvex/WeakBilin.lean @@ -12,7 +12,7 @@ public import Mathlib.LinearAlgebra.Finsupp.Span public import Mathlib.Topology.Algebra.Module.Spaces.WeakBilin /-! -# Weak Dual in Topological Vector Spaces +# Weak Bilinear Topologies in Topological Vector Spaces We prove that the weak topology induced by a bilinear form `B : E β†’β‚—[π•œ] F β†’β‚—[π•œ] π•œ` is locally convex and we explicitly give a neighborhood basis in terms of the family of seminorms @@ -28,7 +28,7 @@ convex and we explicitly give a neighborhood basis in terms of the family of sem * `LinearMap.hasBasis_weakBilin`: the seminorm balls of `B.toSeminormFamily` form a neighborhood basis of `0` in the weak topology. -* `LinearMap.toSeminormFamily.withSeminorms`: the topology of a weak space is induced by the +* `LinearMap.weakBilin_withSeminorms`: the topology of a weak space is induced by the family of seminorms `B.toSeminormFamily`. * `WeakBilin.locallyConvexSpace`: a space endowed with a weak topology is locally convex. * `LinearMap.rightDualEquiv`: When `B` is right-separating, `F` is linearly equivalent to the @@ -43,7 +43,7 @@ convex and we explicitly give a neighborhood basis in terms of the family of sem ## Tags -weak dual, seminorm +weak bilinear, seminorm -/ @[expose] public section diff --git a/Mathlib/Analysis/LocallyConvex/WeakSpace.lean b/Mathlib/Analysis/LocallyConvex/WeakSpace.lean index c56bde3b317779..09619412b8e6e4 100644 --- a/Mathlib/Analysis/LocallyConvex/WeakSpace.lean +++ b/Mathlib/Analysis/LocallyConvex/WeakSpace.lean @@ -1,18 +1,27 @@ /- Copyright (c) 2024 Jireh Loreaux. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jireh Loreaux +Authors: Jireh Loreaux, MichaΕ‚ ŚwiΔ™tek -/ module public import Mathlib.Analysis.LocallyConvex.Separation public import Mathlib.Analysis.LocallyConvex.SeparatingDual +public import Mathlib.Analysis.LocallyConvex.WeakBilin public import Mathlib.LinearAlgebra.Dual.Defs -public import Mathlib.Topology.Algebra.Module.Spaces.WeakDual +public import Mathlib.Topology.Algebra.Module.Spaces.WeakSpace -/-! # Closures of convex sets in locally convex spaces +/-! # Weak topology on normed spaces: seminorm family and convex closures -This file contains the standard result that if `E` is a vector space with two locally convex +## Seminorm family + +The weak topology on `WeakSpace π•œ E` is generated by the seminorm family `fun f x ↦ β€–f xβ€–` +indexed by `StrongDual π•œ E`. This follows from the general `LinearMap.weakBilin_withSeminorms` +applied to the flipped `topDualPairing`. + +## Closures of convex sets + +This file also contains the standard result that if `E` is a vector space with two locally convex topologies, then the closure of a convex set is the same in either topology, provided they have the same collection of continuous linear functionals. In particular, the weak closure of a convex set in a locally convex space coincides with the closure in the original topology. @@ -20,7 +29,38 @@ Of course, we phrase this in terms of linear maps between locally convex spaces, creating two separate topologies on the same space. -/ -public section +@[expose] public section + +section Seminorms + +variable {π•œ : Type*} [NormedField π•œ] {E : Type*} [AddCommGroup E] [Module π•œ E] + [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul π•œ E] + +namespace WeakSpace + +set_option backward.isDefEq.respectTransparency false in +variable (π•œ E) in +/-- The family of seminorms on `WeakSpace π•œ E` given by `fun f x ↦ β€–f xβ€–`, indexed by +`StrongDual π•œ E`. This is the seminorm family associated to the weak topology via the +flipped `topDualPairing`. -/ +def seminormFamily : SeminormFamily π•œ (WeakSpace π•œ E) (StrongDual π•œ E) := + (topDualPairing π•œ E).flip.toSeminormFamily + +set_option backward.isDefEq.respectTransparency false in +omit [ContinuousAdd E] [ContinuousConstSMul π•œ E] in +@[simp] +lemma seminormFamily_apply (f : StrongDual π•œ E) (x : WeakSpace π•œ E) : + seminormFamily π•œ E f x = β€–f xβ€– := rfl + +set_option backward.isDefEq.respectTransparency false in +omit [ContinuousAdd E] [ContinuousConstSMul π•œ E] in +variable (π•œ E) in +lemma withSeminorms : WithSeminorms (seminormFamily π•œ E) := + (topDualPairing π•œ E).flip.weakBilin_withSeminorms + +end WeakSpace + +end Seminorms variable {π•œ E F : Type*} variable [RCLike π•œ] [AddCommGroup E] [Module π•œ E] [AddCommGroup F] [Module π•œ F] diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean index 9d2e4be266bab9..f26fae58dd91b4 100644 --- a/Mathlib/Analysis/Normed/Module/WeakDual.lean +++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean @@ -10,7 +10,7 @@ public import Mathlib.Analysis.Normed.Operator.Completeness public import Mathlib.Topology.Algebra.Module.Spaces.WeakDual public import Mathlib.Topology.MetricSpace.PiNat public import Mathlib.Analysis.Normed.Operator.BanachSteinhaus -public import Mathlib.Analysis.LocallyConvex.WeakDual +public import Mathlib.Analysis.LocallyConvex.WeakBilin /-! # Weak dual of normed space diff --git a/Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean b/Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean index 19a6c438d7d721..7ee2725e59f85b 100644 --- a/Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean +++ b/Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean @@ -12,28 +12,15 @@ public import Mathlib.Topology.Algebra.Module.Spaces.WeakBilin /-! # Weak dual topology -We continue in the setting of `Mathlib/Topology/Algebra/Module/WeakBilin.lean`, -which defines the weak topology given two vector spaces `E` and `F` over a commutative semiring -`π•œ` and a bilinear form `B : E β†’β‚—[π•œ] F β†’β‚—[π•œ] π•œ`. The weak topology on `E` is the coarsest topology -such that for all `y : F` every map `fun x => B x y` is continuous. - -In this file, we consider two special cases. -In the case that `F = E β†’L[π•œ] π•œ` and `B` being the canonical pairing, we obtain the weak-* topology, -`WeakDual π•œ E := (E β†’L[π•œ] π•œ)`. Interchanging the arguments in the bilinear form yields the -weak topology `WeakSpace π•œ E := E`. +This file defines the weak-* (weak dual) topology on the continuous dual `E β†’L[π•œ] π•œ`. +It is the coarsest topology such that for all `z : E` every evaluation map +`fun v => v z` is continuous. ## Main definitions -The main definitions are the types `WeakDual π•œ E` and `WeakSpace π•œ E`, -with the respective topology instances on it. - -* `WeakDual π•œ E` is a type synonym for `Dual π•œ E` (when the latter is defined): both are equal to - the type `E β†’L[π•œ] π•œ` of continuous linear maps from a module `E` over `π•œ` to the ring `π•œ`. +* `WeakDual π•œ E` is a type synonym for `E β†’L[π•œ] π•œ` (equal to `Dual π•œ E`). * The instance `WeakDual.instTopologicalSpace` is the weak-* topology on `WeakDual π•œ E`, i.e., the coarsest topology making the evaluation maps at all `z : E` continuous. -* `WeakSpace π•œ E` is a type synonym for `E` (when the latter is defined). -* The instance `WeakSpace.instTopologicalSpace` is the weak topology on `E`, i.e., the - coarsest topology such that all `v : dual π•œ E` remain continuous. ## References @@ -165,82 +152,12 @@ end Ring end WeakDual -/-- The weak topology is the topology coarsest topology on `E` such that all functionals -`fun x => v x` are continuous. -/ -def WeakSpace (π•œ E) [CommSemiring π•œ] [TopologicalSpace π•œ] [ContinuousAdd π•œ] - [ContinuousConstSMul π•œ π•œ] [AddCommMonoid E] [Module π•œ E] [TopologicalSpace E] := - WeakBilin (topDualPairing π•œ E).flip -deriving AddCommMonoid, Module π•œ, TopologicalSpace, ContinuousAdd - section Semiring variable [CommSemiring π•œ] [TopologicalSpace π•œ] [ContinuousAdd π•œ] variable [ContinuousConstSMul π•œ π•œ] variable [AddCommMonoid E] [Module π•œ E] [TopologicalSpace E] -namespace WeakSpace - -instance instModule' [CommSemiring 𝕝] [Module 𝕝 E] : Module 𝕝 (WeakSpace π•œ E) := - inferInstanceAs <| Module 𝕝 (WeakBilin (topDualPairing π•œ E).flip) - -instance instIsScalarTower [CommSemiring 𝕝] [Module 𝕝 π•œ] [Module 𝕝 E] [IsScalarTower 𝕝 π•œ E] : - IsScalarTower 𝕝 π•œ (WeakSpace π•œ E) := - WeakBilin.instIsScalarTower (topDualPairing π•œ E).flip - -instance instContinuousSMul [ContinuousSMul π•œ π•œ] : ContinuousSMul π•œ (WeakSpace π•œ E) := - WeakBilin.instContinuousSMul _ - -variable [AddCommMonoid F] [Module π•œ F] [TopologicalSpace F] - -/-- A continuous linear map from `E` to `F` is still continuous when `E` and `F` are equipped with -their weak topologies. -/ -def map (f : E β†’L[π•œ] F) : WeakSpace π•œ E β†’L[π•œ] WeakSpace π•œ F := - { f with - cont := - WeakBilin.continuous_of_continuous_eval _ fun l => WeakBilin.eval_continuous _ (l ∘L f) } - -theorem map_apply (f : E β†’L[π•œ] F) (x : E) : WeakSpace.map f x = f x := - rfl - -@[simp] -theorem coe_map (f : E β†’L[π•œ] F) : (WeakSpace.map f : E β†’ F) = f := - rfl - -end WeakSpace - -variable (π•œ E) in -/-- There is a canonical map `E β†’ WeakSpace π•œ E` (the "identity" -mapping). It is a linear equivalence. -/ -def toWeakSpace : E ≃ₗ[π•œ] WeakSpace π•œ E := LinearEquiv.refl π•œ E - -variable (π•œ E) in -/-- For a topological vector space `E`, "identity mapping" `E β†’ WeakSpace π•œ E` is continuous. -This definition implements it as a continuous linear map. -/ -def toWeakSpaceCLM : E β†’L[π•œ] WeakSpace π•œ E where - __ := toWeakSpace π•œ E - cont := by - apply WeakBilin.continuous_of_continuous_eval - exact ContinuousLinearMap.continuous - -variable (π•œ E) in -@[simp] -theorem toWeakSpaceCLM_eq_toWeakSpace (x : E) : - toWeakSpaceCLM π•œ E x = toWeakSpace π•œ E x := by rfl - -theorem toWeakSpaceCLM_bijective : - Function.Bijective (toWeakSpaceCLM π•œ E) := - (toWeakSpace π•œ E).bijective - -/-- The canonical map from `WeakSpace π•œ E` to `E` is an open map. -/ -theorem isOpenMap_toWeakSpace_symm : IsOpenMap (toWeakSpace π•œ E).symm := - IsOpenMap.of_inverse (toWeakSpaceCLM π•œ E).cont - (toWeakSpace π•œ E).left_inv (toWeakSpace π•œ E).right_inv - -/-- A set in `E` which is open in the weak topology is open. -/ -theorem WeakSpace.isOpen_of_isOpen (V : Set E) - (hV : IsOpen ((toWeakSpaceCLM π•œ E) '' V : Set (WeakSpace π•œ E))) : IsOpen V := by - simpa [Set.image_image] using isOpenMap_toWeakSpace_symm _ hV - theorem tendsto_iff_forall_eval_tendsto_topDualPairing {l : Filter Ξ±} {f : Ξ± β†’ WeakDual π•œ E} {x : WeakDual π•œ E} : Tendsto f l (𝓝 x) ↔ @@ -248,20 +165,3 @@ theorem tendsto_iff_forall_eval_tendsto_topDualPairing {l : Filter Ξ±} {f : Ξ± WeakBilin.tendsto_iff_forall_eval_tendsto _ ContinuousLinearMap.coe_injective end Semiring - -section Ring - -namespace WeakSpace - -variable [CommRing π•œ] [TopologicalSpace π•œ] [IsTopologicalAddGroup π•œ] [ContinuousConstSMul π•œ π•œ] -variable [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [IsTopologicalAddGroup E] - -instance instAddCommGroup : AddCommGroup (WeakSpace π•œ E) := - inferInstanceAs <| AddCommGroup (WeakBilin (topDualPairing π•œ E).flip) - -instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakSpace π•œ E) := - WeakBilin.instIsTopologicalAddGroup (topDualPairing π•œ E).flip - -end WeakSpace - -end Ring diff --git a/Mathlib/Topology/Algebra/Module/Spaces/WeakSpace.lean b/Mathlib/Topology/Algebra/Module/Spaces/WeakSpace.lean new file mode 100644 index 00000000000000..88b6429fb956e7 --- /dev/null +++ b/Mathlib/Topology/Algebra/Module/Spaces/WeakSpace.lean @@ -0,0 +1,137 @@ +/- +Copyright (c) 2021 Kalle KytΓΆlΓ€. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kalle KytΓΆlΓ€, Moritz Doll +-/ +module + +public import Mathlib.LinearAlgebra.BilinearMap +public import Mathlib.Topology.Algebra.Module.LinearMap +public import Mathlib.Topology.Algebra.Module.Spaces.WeakBilin + +/-! +# Weak topology + +This file defines the weak topology on a topological vector space `E`. +It is the coarsest topology on `E` such that all continuous linear functionals +`fun x => v x` for `v : E β†’L[π•œ] π•œ` remain continuous. + +## Main definitions + +* `WeakSpace π•œ E` is a type synonym for `E`. +* The instance `WeakSpace.instTopologicalSpace` is the weak topology on `E`, i.e., the + coarsest topology such that all `v : E β†’L[π•œ] π•œ` remain continuous. +* `toWeakSpace`: The canonical linear equivalence `E ≃ₗ[π•œ] WeakSpace π•œ E`. +* `toWeakSpaceCLM`: The identity mapping as a continuous linear map `E β†’L[π•œ] WeakSpace π•œ E`. + +## References + +* [H. H. Schaefer, *Topological Vector Spaces*][schaefer1966] + +## Tags + +weak topology, duality +-/ + +@[expose] public section + +noncomputable section + +open Filter Topology + +variable {Ξ± π•œ 𝕝 E F : Type*} + +/-- The weak topology is the topology coarsest topology on `E` such that all functionals +`fun x => v x` are continuous. -/ +def WeakSpace (π•œ E) [CommSemiring π•œ] [TopologicalSpace π•œ] [ContinuousAdd π•œ] + [ContinuousConstSMul π•œ π•œ] [AddCommMonoid E] [Module π•œ E] [TopologicalSpace E] := + WeakBilin (topDualPairing π•œ E).flip +deriving AddCommMonoid, Module π•œ, TopologicalSpace, ContinuousAdd + +section Semiring + +variable [CommSemiring π•œ] [TopologicalSpace π•œ] [ContinuousAdd π•œ] +variable [ContinuousConstSMul π•œ π•œ] +variable [AddCommMonoid E] [Module π•œ E] [TopologicalSpace E] + +namespace WeakSpace + +instance instModule' [CommSemiring 𝕝] [Module 𝕝 E] : Module 𝕝 (WeakSpace π•œ E) := + inferInstanceAs <| Module 𝕝 (WeakBilin (topDualPairing π•œ E).flip) + +instance instIsScalarTower [CommSemiring 𝕝] [Module 𝕝 π•œ] [Module 𝕝 E] [IsScalarTower 𝕝 π•œ E] : + IsScalarTower 𝕝 π•œ (WeakSpace π•œ E) := + WeakBilin.instIsScalarTower (topDualPairing π•œ E).flip + +instance instContinuousSMul [ContinuousSMul π•œ π•œ] : ContinuousSMul π•œ (WeakSpace π•œ E) := + WeakBilin.instContinuousSMul _ + +variable [AddCommMonoid F] [Module π•œ F] [TopologicalSpace F] + +/-- A continuous linear map from `E` to `F` is still continuous when `E` and `F` are equipped with +their weak topologies. -/ +def map (f : E β†’L[π•œ] F) : WeakSpace π•œ E β†’L[π•œ] WeakSpace π•œ F := + { f with + cont := + WeakBilin.continuous_of_continuous_eval _ fun l => WeakBilin.eval_continuous _ (l ∘L f) } + +theorem map_apply (f : E β†’L[π•œ] F) (x : E) : WeakSpace.map f x = f x := + rfl + +@[simp] +theorem coe_map (f : E β†’L[π•œ] F) : (WeakSpace.map f : E β†’ F) = f := + rfl + +end WeakSpace + +variable (π•œ E) in +/-- There is a canonical map `E β†’ WeakSpace π•œ E` (the "identity" +mapping). It is a linear equivalence. -/ +def toWeakSpace : E ≃ₗ[π•œ] WeakSpace π•œ E := LinearEquiv.refl π•œ E + +variable (π•œ E) in +/-- For a topological vector space `E`, "identity mapping" `E β†’ WeakSpace π•œ E` is continuous. +This definition implements it as a continuous linear map. -/ +def toWeakSpaceCLM : E β†’L[π•œ] WeakSpace π•œ E where + __ := toWeakSpace π•œ E + cont := by + apply WeakBilin.continuous_of_continuous_eval + exact ContinuousLinearMap.continuous + +variable (π•œ E) in +@[simp] +theorem toWeakSpaceCLM_eq_toWeakSpace (x : E) : + toWeakSpaceCLM π•œ E x = toWeakSpace π•œ E x := by rfl + +theorem toWeakSpaceCLM_bijective : + Function.Bijective (toWeakSpaceCLM π•œ E) := + (toWeakSpace π•œ E).bijective + +/-- The canonical map from `WeakSpace π•œ E` to `E` is an open map. -/ +theorem isOpenMap_toWeakSpace_symm : IsOpenMap (toWeakSpace π•œ E).symm := + IsOpenMap.of_inverse (toWeakSpaceCLM π•œ E).cont + (toWeakSpace π•œ E).left_inv (toWeakSpace π•œ E).right_inv + +/-- A set in `E` which is open in the weak topology is open. -/ +theorem WeakSpace.isOpen_of_isOpen (V : Set E) + (hV : IsOpen ((toWeakSpaceCLM π•œ E) '' V : Set (WeakSpace π•œ E))) : IsOpen V := by + simpa [Set.image_image] using isOpenMap_toWeakSpace_symm _ hV + +end Semiring + +section Ring + +namespace WeakSpace + +variable [CommRing π•œ] [TopologicalSpace π•œ] [IsTopologicalAddGroup π•œ] [ContinuousConstSMul π•œ π•œ] +variable [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [IsTopologicalAddGroup E] + +instance instAddCommGroup : AddCommGroup (WeakSpace π•œ E) := + inferInstanceAs <| AddCommGroup (WeakBilin (topDualPairing π•œ E).flip) + +instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakSpace π•œ E) := + WeakBilin.instIsTopologicalAddGroup (topDualPairing π•œ E).flip + +end WeakSpace + +end Ring