theorem LinearMap.absorbent_polar_iff_isVonNBounded {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {s : Set (WeakBilin B)} : Absorbent 𝕜 ((WeakBilin.pairing B).polar s) ↔ Bornology.IsVonNBounded 𝕜 s

theorem LinearMap.isVonNBounded_of_absorbent_polar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {s : Set (WeakBilin B)} : Absorbent 𝕜 ((WeakBilin.pairing B).polar s) → Bornology.IsVonNBounded 𝕜 s

Alias of the forward direction of LinearMap.absorbent_polar_iff_isVonNBounded.

theorem LinearMap.absorbent_polar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {s : Set (WeakBilin B)} : Bornology.IsVonNBounded 𝕜 s → Absorbent 𝕜 ((WeakBilin.pairing B).polar s)

Alias of the reverse direction of LinearMap.absorbent_polar_iff_isVonNBounded.

def LinearMap.nhdsPolars {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [TopologicalSpace E] : Set (Set F)

The collection of polars of neighborhoods of zero.

Equations

• B.nhdsPolars = B.polar '' (nhds 0).sets

theorem LinearMap.nonempty_nhdsPolars {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} [TopologicalSpace E] : B.nhdsPolars.Nonempty

theorem LinearMap.directedOn_nhdsPolars {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} [TopologicalSpace E] : DirectedOn (fun (x1 x2 : Set F) => x1 ⊆ x2) B.nhdsPolars

theorem LinearMap.nhdsPolars_mem_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} [TopologicalSpace E] {s : Set F} : s ∈ B.nhdsPolars ↔ ∃ u ∈ nhds 0, B.polar u = s

theorem LinearMap.polar_mem_nhdsPolars {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} [TopologicalSpace E] {s : Set E} (hs : s ∈ nhds 0) : B.polar s ∈ B.nhdsPolars

theorem LinearMap.IsCompatibleDual.isCompact_polar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [ProperSpace 𝕜] [TopologicalSpace F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [h : B.IsCompatibleDual] [hB : B.flip.IsWeak] {s : Set E} (s_nhds : s ∈ nhds 0) : IsCompact (B.polar s)

instance LinearMap.instIsCompatibleDualWeakBilinFlipPairing {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [B.IsCompatibleDual] : (WeakBilin.pairing B.flip).flip.IsCompatibleDual

theorem LinearMap.IsCompatibleDual.isVonNBounded_polar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [ProperSpace 𝕜] [TopologicalSpace F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [h : B.IsCompatibleDual] [hB : B.flip.IsWeak] {s : Set E} (s_nhds : s ∈ nhds 0) : Bornology.IsVonNBounded 𝕜 (B.polar s)

def PolarTopology {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (𝔖 : Set (Set F)) : Type u_2

PolarTopology B 𝔖, where B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜 is a type synonym for E where the topology is induced by B when we equip F → 𝕜 with the topology of uniform convergence on the collection of sets 𝔖 : Set (Set F)).

Equations

• PolarTopology B 𝔖 = E

@[implicit_reducible]

instance instAddCommGroupPolarTopology {𝕜 : Type u_2} {E : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (𝔖 : Set (Set F)) : AddCommGroup (PolarTopology B 𝔖)

Equations

• instAddCommGroupPolarTopology B 𝔖 = instAddCommGroupPolarTopology._aux_1 B 𝔖

@[implicit_reducible]

instance instModulePolarTopology {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {𝕝 : Type u_4} [CommRing 𝕝] [Module 𝕝 E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (𝔖 : Set (Set F)) : Module 𝕝 (PolarTopology B 𝔖)

Equations

• instModulePolarTopology B 𝔖 = instModulePolarTopology._aux_1 B 𝔖

instance instIsScalarTowerPolarTopology {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {𝕝 : Type u_4} [CommRing 𝕝] [Module 𝕝 E] [SMul 𝕝 𝕜] [IsScalarTower 𝕝 𝕜 E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (𝔖 : Set (Set F)) : IsScalarTower 𝕝 𝕜 (PolarTopology B 𝔖)

def PolarTopology.linearEquiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} : PolarTopology B 𝔖 ≃ₗ[𝕜] E

The canonical equivalence between PolarTopology B 𝔖 and E.

Equations

• PolarTopology.linearEquiv = LinearEquiv.refl 𝕜 (PolarTopology B 𝔖)

@[reducible, inline]

abbrev PolarTopology.bilin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (𝔖 : Set (Set F)) : F →ₗ[𝕜] PolarTopology B 𝔖 →ₗ[𝕜] 𝕜

Variant of B.flip with the type synonym PolarTopology B 𝔖 in place of E.

Equations

• PolarTopology.bilin B 𝔖 = ((PolarTopology.linearEquiv.symm.arrowCongr (LinearEquiv.refl 𝕜 (F →ₗ[𝕜] 𝕜))) B).flip

theorem PolarTopology.bilin_apply_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} (y : F) (x : PolarTopology B 𝔖) : ((bilin B 𝔖) y) x = (B (linearEquiv x)) y

def PolarTopology.toUniformOnFun {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} : PolarTopology B 𝔖 →ₗ[𝕜] UniformOnFun F 𝕜 𝔖

Linear equivalence of PolarTopology B 𝔖 with F →ᵤ[𝔖] 𝕜.

Equations

• PolarTopology.toUniformOnFun = (PolarTopology.linearEquiv.symm.arrowCongr (UniformOnFun.toFunLinearEquiv 𝔖).symm) ((LinearMap.compRight 𝕜 (LinearMap.ltoFun 𝕜 F 𝕜 𝕜)) B)

@[simp]

theorem PolarTopology.toUniformOnFun_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} (x : PolarTopology B 𝔖) : toUniformOnFun x = (UniformOnFun.ofFun 𝔖) ⇑(B x)

noncomputable def PolarTopology.toUniformConvergenceCLM {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] : PolarTopology B 𝔖 →ₗ[𝕜] UniformConvergenceCLM (RingHom.id 𝕜) 𝕜 𝔖

The linear map from PolarTopology B 𝔖 into the space of continuous linear maps on F (where F is equipped with the weak topology induced by B.flip) equipped with the topology of uniform convergence on 𝔖 : Set (Set F).

Equations

• PolarTopology.toUniformConvergenceCLM = (PolarTopology.linearEquiv.symm.arrowCongr (ContinuousLinearMap.toUniformConvergenceCLM (RingHom.id 𝕜) 𝕜 𝔖)) (B.toCLMRight ⋯)

@[simp]

theorem PolarTopology.toUniformConvergenceCLM_apply_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] (x : PolarTopology B 𝔖) (y : F) : (toUniformConvergenceCLM x) y = (B x) y

@[implicit_reducible]

noncomputable instance PolarTopology.instUniformSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (𝔖 : Set (Set F)) [TopologicalSpace F] [B.flip.IsWeak] : UniformSpace (PolarTopology B 𝔖)

Equations

• PolarTopology.instUniformSpace B 𝔖 = UniformSpace.comap (⇑PolarTopology.toUniformConvergenceCLM) inferInstance

@[implicit_reducible]

noncomputable instance PolarTopology.instTopologicalSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (𝔖 : Set (Set F)) [TopologicalSpace F] [B.flip.IsWeak] : TopologicalSpace (PolarTopology B 𝔖)

Equations

• PolarTopology.instTopologicalSpace B 𝔖 = TopologicalSpace.induced (⇑PolarTopology.toUniformConvergenceCLM) inferInstance

instance PolarTopology.instIsUniformAddGroup {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (𝔖 : Set (Set F)) [TopologicalSpace F] [B.flip.IsWeak] : IsUniformAddGroup (PolarTopology B 𝔖)

theorem PolarTopology.isUniformInducing_toUniformConvergenceCLM {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (𝔖 : Set (Set F)) [TopologicalSpace F] [B.flip.IsWeak] : IsUniformInducing ⇑toUniformConvergenceCLM

instance PolarTopology.instContinuousConstSMul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (𝔖 : Set (Set F)) [TopologicalSpace F] [B.flip.IsWeak] : ContinuousConstSMul 𝕜 (PolarTopology B 𝔖)

theorem PolarTopology.continuousSMul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (𝔖 : Set (Set F)) [TopologicalSpace F] [B.flip.IsWeak] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [TopologicalSpace E] (h𝔖 : ∀ S ∈ 𝔖, Bornology.IsVonNBounded 𝕜 S) : ContinuousSMul 𝕜 (PolarTopology B 𝔖)

theorem PolarTopology.isUniformEmbedding_toUniformConvergenceCLM {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (𝔖 : Set (Set F)) [TopologicalSpace F] [B.flip.IsWeak] (hB : B.SeparatingLeft) : IsUniformEmbedding ⇑toUniformConvergenceCLM

theorem PolarTopology.uniformSpace_mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [TopologicalSpace F] [B.flip.IsWeak] (𝔖 𝔗 : Set (Set F)) (h𝔖𝔗 : 𝔖 ⊆ 𝔗) : instUniformSpace B 𝔗 ≤ instUniformSpace B 𝔖

theorem PolarTopology.topologicalSpace_mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [TopologicalSpace F] [B.flip.IsWeak] (𝔖 𝔗 : Set (Set F)) (h𝔖𝔗 : 𝔖 ⊆ 𝔗) : instTopologicalSpace B 𝔗 ≤ instTopologicalSpace B 𝔖

theorem PolarTopology.continuous_mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [TopologicalSpace F] [B.flip.IsWeak] (𝔖 𝔗 : Set (Set F)) (h𝔖𝔗 : 𝔖 ⊆ 𝔗) : Continuous ⇑(linearEquiv ≪≫ₗ linearEquiv.symm)

theorem PolarTopology.isUniformInducing_toUniformOnFun {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (𝔖 : Set (Set F)) [TopologicalSpace F] [B.flip.IsWeak] : IsUniformInducing ⇑toUniformOnFun

theorem PolarTopology.hasBasis_uniformity_of_basis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] {ι : Type u_4} {p : ι → Prop} {s : ι → Set (𝕜 × 𝕜)} (h : 𝔖.Nonempty) (h' : DirectedOn (fun (x1 x2 : Set F) => x1 ⊆ x2) 𝔖) (hb : (uniformity 𝕜).HasBasis p s) : (uniformity (PolarTopology B 𝔖)).HasBasis (fun (Si : Set F × ι) => Si.1 ∈ 𝔖 ∧ p Si.2) fun (Si : Set F × ι) => Prod.map ⇑toUniformOnFun ⇑toUniformOnFun ⁻¹' UniformOnFun.gen 𝔖 Si.1 (s Si.2)

theorem PolarTopology.hasBasis_uniformity {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] (h : 𝔖.Nonempty) (h' : DirectedOn (fun (x1 x2 : Set F) => x1 ⊆ x2) 𝔖) : (uniformity (PolarTopology B 𝔖)).HasBasis (fun (SV : Set F × Set (𝕜 × 𝕜)) => SV.1 ∈ 𝔖 ∧ SV.2 ∈ uniformity 𝕜) fun (SV : Set F × Set (𝕜 × 𝕜)) => Prod.map ⇑toUniformOnFun ⇑toUniformOnFun ⁻¹' UniformOnFun.gen 𝔖 SV.1 SV.2

theorem PolarTopology.hasBasis_nhds_of_basis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] {ι : Type u_4} {p : ι → Prop} {s : ι → Set (𝕜 × 𝕜)} (h : 𝔖.Nonempty) (h' : DirectedOn (fun (x1 x2 : Set F) => x1 ⊆ x2) 𝔖) (hb : (uniformity 𝕜).HasBasis p s) (y : PolarTopology B 𝔖) : (nhds y).HasBasis (fun (Si : Set F × ι) => Si.1 ∈ 𝔖 ∧ p Si.2) fun (Si : Set F × ι) => ⇑toUniformOnFun ⁻¹' {x : UniformOnFun F 𝕜 𝔖 | (x, toUniformOnFun y) ∈ UniformOnFun.gen 𝔖 Si.1 (s Si.2)}

theorem PolarTopology.tendsto_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] {α : Type u_4} {f : α → PolarTopology B 𝔖} {l : Filter α} {y : PolarTopology B 𝔖} : Filter.Tendsto f l (nhds y) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (fun (x : α) => ⇑(B (linearEquiv (f x)))) (⇑(B (linearEquiv y))) l s

noncomputable def PolarTopology.seminorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (𝔖 : Set (Set F)) [TopologicalSpace F] [B.flip.IsWeak] (s : Set F) (hs : Bornology.IsVonNBounded 𝕜 s) : Seminorm 𝕜 (PolarTopology B 𝔖)

The seminorm on PolarTopology B 𝔖 by taking for x : E the supremum of the values of B x y over all y ∈ s, where s ∈ 𝔖.

Equations

• One or more equations did not get rendered due to their size.

theorem PolarTopology.seminorm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] (s : Set F) (hs : Bornology.IsVonNBounded 𝕜 s) (x : PolarTopology B 𝔖) : (seminorm B 𝔖 s hs) x = sSup ((fun (x_1 : F) => ‖(B (linearEquiv x)) x_1‖) '' s)

theorem Bornology.IsVonNBounded.empty (𝕜 : Type u_1) (E : Type u_3) [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] : IsVonNBounded 𝕜 ∅

Alias of Bornology.isVonNBounded_empty.

@[simp]

theorem PolarTopology.seminorm_empty {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] : seminorm B 𝔖 ∅ ⋯ = 0

theorem PolarTopology.isLUB_seminorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] {s : Set F} (hs : Bornology.IsVonNBounded 𝕜 s) (hs_non : s.Nonempty) (x : PolarTopology B 𝔖) : IsLUB ((fun (x_1 : F) => ‖(B (linearEquiv x)) x_1‖) '' s) ((seminorm B 𝔖 s hs) x)

theorem PolarTopology.seminorm_apply_le_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] {s : Set F} (hs : Bornology.IsVonNBounded 𝕜 s) {r : ℝ} (hr : 0 ≤ r) (x : PolarTopology B 𝔖) : (seminorm B 𝔖 s hs) x ≤ r ↔ ∀ y ∈ s, ‖(B (linearEquiv x)) y‖ ≤ r

theorem PolarTopology.seminorm_apply_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] {s : Set F} (hs : Bornology.IsVonNBounded 𝕜 s) (x : PolarTopology B 𝔖) {y : WeakBilin B.flip} (hy : y ∈ s) : ‖(B (linearEquiv x)) y‖ ≤ (seminorm B 𝔖 s hs) x

theorem PolarTopology.seminorm_le_of_subset {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] {s t : Set F} (hs : Bornology.IsVonNBounded 𝕜 s) (ht : Bornology.IsVonNBounded 𝕜 t) (hst : s ⊆ t) : seminorm B 𝔖 s hs ≤ seminorm B 𝔖 t ht

theorem PolarTopology.seminorm_union {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] {s t : Set F} (hs : Bornology.IsVonNBounded 𝕜 s) (ht : Bornology.IsVonNBounded 𝕜 t) : seminorm B 𝔖 (s ∪ t) ⋯ = seminorm B 𝔖 s hs ⊔ seminorm B 𝔖 t ht

theorem PolarTopology.seminorm_finite_sUnion {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] {s : Set (Set F)} (hs : s.Finite) (hsbdd : ∀ t ∈ s, Bornology.IsVonNBounded 𝕜 t) : seminorm B 𝔖 (⋃₀ s) ⋯ = ⨆ (i : { t : Set F // t ∈ s }), seminorm B 𝔖 ↑i ⋯

theorem PolarTopology.continuous_seminorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] (h𝔖_non : 𝔖.Nonempty) (h𝔖_dir : DirectedOn (fun (x1 x2 : Set F) => x1 ⊆ x2) 𝔖) (s : Set F) (hs_mem : s ∈ 𝔖) (hs : Bornology.IsVonNBounded 𝕜 s) : Continuous ⇑(seminorm B 𝔖 s hs)

noncomputable def PolarTopology.seminormFamily {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (𝔖 : Set (Set F)) [TopologicalSpace F] [B.flip.IsWeak] (h𝔖 : ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 s) : SeminormFamily 𝕜 (PolarTopology B 𝔖) ↑𝔖

The natural SeminormFamily associated to PolarTopology B 𝔖.

Equations

• PolarTopology.seminormFamily B 𝔖 h𝔖 s = PolarTopology.seminorm B 𝔖 ↑s ⋯

theorem PolarTopology.seminormFamily_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] (h𝔖 : ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 s) (s : ↑𝔖) : seminormFamily B 𝔖 h𝔖 s = seminorm B 𝔖 ↑s ⋯

theorem PolarTopology.directed_seminormFamily {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] (h𝔖 : ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 s) (h𝔖_dir : DirectedOn (fun (x1 x2 : Set F) => x1 ⊆ x2) 𝔖) : Directed (fun (x1 x2 : Seminorm 𝕜 (PolarTopology B 𝔖)) => x1 ≤ x2) (seminormFamily B 𝔖 h𝔖)

theorem PolarTopology.withSeminorms {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (𝔖 : Set (Set F)) [TopologicalSpace F] [B.flip.IsWeak] (h𝔖_non : 𝔖.Nonempty) (h𝔖_dir : DirectedOn (fun (x1 x2 : Set F) => x1 ⊆ x2) 𝔖) (h𝔖 : ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 s) : WithSeminorms (seminormFamily B 𝔖 h𝔖)

theorem PolarTopology.unitClosedBall_seminorm_eq_polar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] {s : Set F} (hs : Bornology.IsVonNBounded 𝕜 s) : (seminorm B 𝔖 s hs).closedBall 0 1 = (bilin B 𝔖).polar s

theorem PolarTopology.polar_mem_nhds {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] (h𝔖_non : 𝔖.Nonempty) (h𝔖_dir : DirectedOn (fun (x1 x2 : Set F) => x1 ⊆ x2) 𝔖) (s : Set F) (hs_mem : s ∈ 𝔖) (hs : Bornology.IsVonNBounded 𝕜 s) : (bilin B 𝔖).polar s ∈ nhds 0

theorem PolarTopology.hasBasis_nhds_zero_polar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] (h𝔖_non : 𝔖.Nonempty) (h𝔖_dir : DirectedOn (fun (x1 x2 : Set F) => x1 ⊆ x2) 𝔖) (h𝔖 : ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 s) (h𝔖_scale : ∀ c > 0, ∀ s ∈ 𝔖, ∃ t ∈ 𝔖, c • s ⊆ t) : (nhds 0).HasBasis (fun (x : Set F) => x ∈ 𝔖) (bilin B 𝔖).polar

theorem PolarTopology.locallyConvexSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {𝔖 : Set (Set F)} [TopologicalSpace F] [B.flip.IsWeak] [Module ℝ E] [h : IsScalarTower ℝ 𝕜 E] (h𝔖_non : 𝔖.Nonempty) (h𝔖_dir : DirectedOn (fun (x1 x2 : Set F) => x1 ⊆ x2) 𝔖) (h𝔖 : ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 s) : LocallyConvexSpace ℝ (PolarTopology B 𝔖)

theorem PolarTopology.isVonNBounded_nhdsPolars {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} [TopologicalSpace F] [B.flip.IsWeak] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [hB : B.IsCompatibleDual] (s : Set F) (hs : s ∈ B.nhdsPolars) : Bornology.IsVonNBounded 𝕜 s

theorem PolarTopology.continuous_seminorm_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [TopologicalSpace F] [B.flip.IsWeak] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [B.IsCompatibleDual] {s : Set E} (hs1 : s ∈ nhds 0) : Continuous ⇑((seminorm B B.nhdsPolars (B.polar s) ⋯).comp ↑linearEquiv.symm)

def PolarTopology.polarTopologyNhdsPolars {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} [TopologicalSpace F] [B.flip.IsWeak] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [hLCS : LocallyConvexSpace 𝕜 E] [hB : B.IsCompatibleDual] : PolarTopology B B.nhdsPolars ≃L[𝕜] E

The continuous linear equivalence between E satisfiying B.flip.IsCompatibleDual and PolarTopology B (nhdsPolars B).

Equations

• PolarTopology.polarTopologyNhdsPolars = { toLinearEquiv := PolarTopology.linearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }