Locally convex topological modules

A LocallyConvexSpace is a topological semimodule over an ordered semiring in which any point admits a neighborhood basis made of convex sets, or equivalently, in which convex neighborhoods of a point form a neighborhood basis at that point.

In a module, this is equivalent to 0 satisfying such properties.

Main results

• locallyConvexSpace_iff_zero : in a module, local convexity at zero gives local convexity everywhere
• WithSeminorms.locallyConvexSpace : a topology generated by a family of seminorms is locally convex (in Analysis.LocallyConvex.WithSeminorms)
• NormedSpace.locallyConvexSpace : a normed space is locally convex (in Analysis.LocallyConvex.WithSeminorms)

TODO

• define a structure LocallyConvexFilterBasis, extending ModuleFilterBasis, for filter bases generating a locally convex topology

class LocallyConvexSpace (𝕜 : Type u_1) (E : Type u_2) [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : Prop

A LocallyConvexSpace is a topological semimodule over an ordered semiring in which convex neighborhoods of a point form a neighborhood basis at that point.

• convex_basis (x : E) : (nhds x).HasBasis (fun (s : Set E) => s ∈ nhds x ∧ Convex 𝕜 s) id

theorem locallyConvexSpace_iff (𝕜 : Type u_1) (E : Type u_2) [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : LocallyConvexSpace 𝕜 E ↔ ∀ (x : E), (nhds x).HasBasis (fun (s : Set E) => s ∈ nhds x ∧ Convex 𝕜 s) id

theorem LocallyConvexSpace.ofBases (𝕜 : Type u_1) (E : Type u_2) [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] {ι : Type u_3} (b : E → ι → Set E) (p : E → ι → Prop) (hbasis : ∀ (x : E), (nhds x).HasBasis (p x) (b x)) (hconvex : ∀ (x : E) (i : ι), p x i → Convex 𝕜 (b x i)) : LocallyConvexSpace 𝕜 E

theorem LocallyConvexSpace.convex_basis_zero (𝕜 : Type u_1) (E : Type u_2) [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [LocallyConvexSpace 𝕜 E] : (nhds 0).HasBasis (fun (s : Set E) => s ∈ nhds 0 ∧ Convex 𝕜 s) id

theorem locallyConvexSpace_iff_exists_convex_subset (𝕜 : Type u_1) (E : Type u_2) [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : LocallyConvexSpace 𝕜 E ↔ ∀ (x : E), ∀ U ∈ nhds x, ∃ S ∈ nhds x, Convex 𝕜 S ∧ S ⊆ U

theorem LocallyConvexSpace.ofBasisZero (𝕜 : Type u_1) (E : Type u_2) [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] {ι : Type u_3} (b : ι → Set E) (p : ι → Prop) (hbasis : (nhds 0).HasBasis p b) (hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)) : LocallyConvexSpace 𝕜 E

theorem locallyConvexSpace_iff_zero (𝕜 : Type u_1) (E : Type u_2) [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] : LocallyConvexSpace 𝕜 E ↔ (nhds 0).HasBasis (fun (s : Set E) => s ∈ nhds 0 ∧ Convex 𝕜 s) id

theorem locallyConvexSpace_iff_exists_convex_subset_zero (𝕜 : Type u_1) (E : Type u_2) [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] : LocallyConvexSpace 𝕜 E ↔ ∀ U ∈ nhds 0, ∃ S ∈ nhds 0, Convex 𝕜 S ∧ S ⊆ U

@[instance 100]

instance LocallyConvexSpace.toLocPathConnectedSpace (E : Type u_2) [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] : LocPathConnectedSpace E

theorem Convex.locPathConnectedSpace (E : Type u_2) [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {S : Set E} (hS : Convex ℝ S) : LocPathConnectedSpace ↑S

Convex subsets of locally convex spaces are locally path-connected.

theorem LocallyConvexSpace.convex_open_basis_zero (𝕜 : Type u_1) (E : Type u_2) [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [LocallyConvexSpace 𝕜 E] : (nhds 0).HasBasis (fun (s : Set E) => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) id

theorem Disjoint.exists_open_convexes {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [LocallyConvexSpace 𝕜 E] {s t : Set E} (disj : Disjoint s t) (hs₁ : Convex 𝕜 s) (hs₂ : IsCompact s) (ht₁ : Convex 𝕜 t) (ht₂ : IsClosed t) : ∃ (u : Set E) (v : Set E), IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

In a locally convex space, every two disjoint convex sets such that one is compact and the other is closed admit disjoint convex open neighborhoods.

theorem exists_open_convex_of_not_mem {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [LocallyConvexSpace 𝕜 E] {s : Set E} {x : E} (hx : x ∉ s) (hsconv : Convex 𝕜 s) (hsclosed : IsClosed s) : ∃ (U : Set E) (V : Set E), IsOpen U ∧ IsOpen V ∧ Convex 𝕜 U ∧ Convex 𝕜 V ∧ x ∈ U ∧ s ⊆ V ∧ Disjoint U V

In a locally convex space, every point x and closed convex set s ∌ x admit disjoint convex open neighborhoods.

theorem locallyConvexSpace_sInf {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E] [Module 𝕜 E] {ts : Set (TopologicalSpace E)} (h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E) : LocallyConvexSpace 𝕜 E

theorem locallyConvexSpace_iInf {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E] [Module 𝕜 E] {ts' : ι → TopologicalSpace E} (h' : ∀ (i : ι), LocallyConvexSpace 𝕜 E) : LocallyConvexSpace 𝕜 E

theorem locallyConvexSpace_inf {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E] [Module 𝕜 E] {t₁ t₂ : TopologicalSpace E} (h₁ : LocallyConvexSpace 𝕜 E) (h₂ : LocallyConvexSpace 𝕜 E) : LocallyConvexSpace 𝕜 E

theorem locallyConvexSpace_induced {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] {t : TopologicalSpace F} [LocallyConvexSpace 𝕜 F] (f : E →ₗ[𝕜] F) : LocallyConvexSpace 𝕜 E

instance Pi.locallyConvexSpace {𝕜 : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] {ι : Type u_5} {X : ι → Type u_6} [(i : ι) → AddCommMonoid (X i)] [(i : ι) → TopologicalSpace (X i)] [(i : ι) → Module 𝕜 (X i)] [∀ (i : ι), LocallyConvexSpace 𝕜 (X i)] : LocallyConvexSpace 𝕜 ((i : ι) → X i)

instance Prod.locallyConvexSpace {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace E] [TopologicalSpace F] [LocallyConvexSpace 𝕜 E] [LocallyConvexSpace 𝕜 F] : LocallyConvexSpace 𝕜 (E × F)

instance LinearOrderedSemiring.toLocallyConvexSpace {R : Type u_1} [TopologicalSpace R] [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [OrderTopology R] : LocallyConvexSpace R R

theorem Convex.eventually_nhdsWithin_segment {E : Type u_1} {𝕜 : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [LocallyConvexSpace 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x₀ : E} (hx₀s : x₀ ∈ s) {p : E → Prop} (h : ∀ᶠ (x : E) in nhdsWithin x₀ s, p x) : ∀ᶠ (x : E) in nhdsWithin x₀ s, ∀ y ∈ segment 𝕜 x₀ x, p y