The topological strong dual of a module

Main definitions

• strongDualPairing: The strong dual pairing as a bilinear form.
• StrongDual.polar: Given a subset s in a monoid M (over a commutative ring R), the polar polar R s is the subset of StrongDual R M consisting of those functionals which evaluate to something of norm at most one at all points z ∈ s.
• StrongDual.polarSubmodule: Given a subset s in a monoid M (over a field 𝕜) closed under scalar multiplication, the polar polarSubmodule 𝕜 s is the submodule of StrongDual 𝕜 M consisting of those functionals which evaluate to zero at all points z ∈ s.

References

• [Conway, John B., A course in functional analysis][conway1990]

Tags

StrongDual, polar

def strongDualPairing (R : Type u_1) [CommSemiring R] [TopologicalSpace R] (M : Type u_2) [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousAdd R] [ContinuousConstSMul R R] : StrongDual R M →ₗ[R] M →ₗ[R] R

The StrongDual pairing as a bilinear form.

Equations

• strongDualPairing R M = ContinuousLinearMap.coeLM R

@[deprecated strongDualPairing (since := "2025-08-3")]

def StrongDual.NormedSpace.dualPairing (R : Type u_1) [CommSemiring R] [TopologicalSpace R] (M : Type u_2) [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousAdd R] [ContinuousConstSMul R R] : StrongDual R M →ₗ[R] M →ₗ[R] R

Alias of strongDualPairing.

---

The StrongDual pairing as a bilinear form.

Equations

• StrongDual.NormedSpace.dualPairing = strongDualPairing

@[simp]

theorem StrongDual.dualPairing_apply (R : Type u_1) [CommSemiring R] [TopologicalSpace R] (M : Type u_2) [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousAdd R] [ContinuousConstSMul R R] {v : StrongDual R M} {x : M} : ((strongDualPairing R M) v) x = v x

@[deprecated StrongDual.dualPairing_apply (since := "2025-08-3")]

theorem StrongDual.NormedSpace.dualPairing_apply (R : Type u_1) [CommSemiring R] [TopologicalSpace R] (M : Type u_2) [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousAdd R] [ContinuousConstSMul R R] {v : StrongDual R M} {x : M} : ((strongDualPairing R M) v) x = v x

Alias of StrongDual.dualPairing_apply.

theorem StrongDual.dualPairing_separatingLeft (R : Type u_1) (M : Type u_2) [SeminormedCommRing R] [TopologicalSpace M] [AddCommGroup M] [Module R M] : (strongDualPairing R M).SeparatingLeft

@[deprecated StrongDual.dualPairing_separatingLeft (since := "2025-08-3")]

theorem StrongDual.NormedSpace.dualPairing_separatingLeft (R : Type u_1) (M : Type u_2) [SeminormedCommRing R] [TopologicalSpace M] [AddCommGroup M] [Module R M] : (strongDualPairing R M).SeparatingLeft

Alias of StrongDual.dualPairing_separatingLeft.

def StrongDual.polar (R : Type u_1) [NormedCommRing R] {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] [Module R M] : Set M → Set (StrongDual R M)

Given a subset s in a monoid M (over a commutative ring R), the polar polar R s is the subset of StrongDual R M consisting of those functionals which evaluate to something of norm at most one at all points z ∈ s.

Equations

• StrongDual.polar R = (strongDualPairing R M).flip.polar

@[deprecated StrongDual.polar (since := "2025-08-3")]

def NormedSpace.polar (R : Type u_1) [NormedCommRing R] {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] [Module R M] : Set M → Set (StrongDual R M)

Alias of StrongDual.polar.

---

Given a subset s in a monoid M (over a commutative ring R), the polar polar R s is the subset of StrongDual R M consisting of those functionals which evaluate to something of norm at most one at all points z ∈ s.

Equations

• NormedSpace.polar = StrongDual.polar

def StrongDual.polarSubmodule (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] [Module 𝕜 M] {S : Type u_3} [SetLike S M] [SMulMemClass S 𝕜 M] (m : S) : Submodule 𝕜 (StrongDual 𝕜 M)

Given a subset s in a monoid M (over a field 𝕜) closed under scalar multiplication, the polar polarSubmodule 𝕜 s is the submodule of StrongDual 𝕜 M consisting of those functionals which evaluate to zero at all points z ∈ s.

Equations

• StrongDual.polarSubmodule 𝕜 m = (strongDualPairing 𝕜 M).flip.polarSubmodule m

@[deprecated StrongDual.polarSubmodule (since := "2025-08-3")]

def NormedSpace.polarSubmodule (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] [Module 𝕜 M] {S : Type u_3} [SetLike S M] [SMulMemClass S 𝕜 M] (m : S) : Submodule 𝕜 (StrongDual 𝕜 M)

Alias of StrongDual.polarSubmodule.

---

Given a subset s in a monoid M (over a field 𝕜) closed under scalar multiplication, the polar polarSubmodule 𝕜 s is the submodule of StrongDual 𝕜 M consisting of those functionals which evaluate to zero at all points z ∈ s.

Equations

• NormedSpace.polarSubmodule = StrongDual.polarSubmodule

theorem StrongDual.polarSubmodule_eq_polar (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (m : SubMulAction 𝕜 E) : ↑(polarSubmodule 𝕜 m) = polar 𝕜 ↑m

@[deprecated StrongDual.polarSubmodule_eq_polar (since := "2025-08-3")]

theorem NormedSpace.polarSubmodule_eq_polar (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (m : SubMulAction 𝕜 E) : ↑(StrongDual.polarSubmodule 𝕜 m) = StrongDual.polar 𝕜 ↑m

Alias of StrongDual.polarSubmodule_eq_polar.

theorem StrongDual.mem_polar_iff (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {x' : StrongDual 𝕜 E} (s : Set E) : x' ∈ polar 𝕜 s ↔ ∀ z ∈ s, ‖x' z‖ ≤ 1

@[deprecated StrongDual.mem_polar_iff (since := "2025-08-3")]

theorem NormedSpace.mem_polar_iff (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {x' : StrongDual 𝕜 E} (s : Set E) : x' ∈ StrongDual.polar 𝕜 s ↔ ∀ z ∈ s, ‖x' z‖ ≤ 1

Alias of StrongDual.mem_polar_iff.

theorem StrongDual.polarSubmodule_eq_setOf (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {S : Type u_3} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) : ↑(polarSubmodule 𝕜 m) = {y : StrongDual 𝕜 E | ∀ x ∈ m, y x = 0}

@[deprecated StrongDual.polarSubmodule_eq_setOf (since := "2025-08-3")]

theorem NormedSpace.polarSubmodule_eq_setOf (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {S : Type u_3} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) : ↑(StrongDual.polarSubmodule 𝕜 m) = {y : StrongDual 𝕜 E | ∀ x ∈ m, y x = 0}

Alias of StrongDual.polarSubmodule_eq_setOf.

theorem StrongDual.mem_polarSubmodule (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {S : Type u_3} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) (y : StrongDual 𝕜 E) : y ∈ polarSubmodule 𝕜 m ↔ ∀ x ∈ m, y x = 0

@[deprecated StrongDual.mem_polarSubmodule (since := "2025-08-3")]

theorem NormedSpace.mem_polarSubmodule (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {S : Type u_3} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) (y : StrongDual 𝕜 E) : y ∈ StrongDual.polarSubmodule 𝕜 m ↔ ∀ x ∈ m, y x = 0

Alias of StrongDual.mem_polarSubmodule.

@[simp]

theorem StrongDual.zero_mem_polar (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (s : Set E) : 0 ∈ polar 𝕜 s

@[deprecated StrongDual.zero_mem_polar (since := "2025-08-3")]

theorem NormedSpace.zero_mem_polar (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (s : Set E) : 0 ∈ StrongDual.polar 𝕜 s

Alias of StrongDual.zero_mem_polar.

theorem StrongDual.polar_nonempty (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (s : Set E) : (polar 𝕜 s).Nonempty

@[deprecated StrongDual.polar_nonempty (since := "2025-08-3")]

theorem NormedSpace.polar_nonempty (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (s : Set E) : (StrongDual.polar 𝕜 s).Nonempty

Alias of StrongDual.polar_nonempty.

@[simp]

theorem StrongDual.polar_empty (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] : polar 𝕜 ∅ = Set.univ

@[deprecated StrongDual.polar_empty (since := "2025-08-3")]

theorem NormedSpace.polar_empty (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] : StrongDual.polar 𝕜 ∅ = Set.univ

Alias of StrongDual.polar_empty.

@[simp]

theorem StrongDual.polar_singleton (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {a : E} : polar 𝕜 {a} = {x : StrongDual 𝕜 E | ‖x a‖ ≤ 1}

@[deprecated StrongDual.polar_singleton (since := "2025-08-3")]

theorem NormedSpace.polar_singleton (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {a : E} : StrongDual.polar 𝕜 {a} = {x : StrongDual 𝕜 E | ‖x a‖ ≤ 1}

Alias of StrongDual.polar_singleton.

theorem StrongDual.mem_polar_singleton (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {a : E} (y : StrongDual 𝕜 E) : y ∈ polar 𝕜 {a} ↔ ‖y a‖ ≤ 1

@[deprecated StrongDual.mem_polar_singleton (since := "2025-08-3")]

theorem NormedSpace.mem_polar_singleton (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {a : E} (y : StrongDual 𝕜 E) : y ∈ StrongDual.polar 𝕜 {a} ↔ ‖y a‖ ≤ 1

Alias of StrongDual.mem_polar_singleton.

theorem StrongDual.polar_zero (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] : polar 𝕜 {0} = Set.univ

@[deprecated StrongDual.polar_zero (since := "2025-08-3")]

theorem NormedSpace.polar_zero (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] : StrongDual.polar 𝕜 {0} = Set.univ

Alias of StrongDual.polar_zero.

@[simp]

theorem StrongDual.polar_univ (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] : polar 𝕜 Set.univ = {0}

@[deprecated StrongDual.polar_univ (since := "2025-08-3")]

theorem NormedSpace.polar_univ (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] : StrongDual.polar 𝕜 Set.univ = {0}

Alias of StrongDual.polar_univ.