Annihilators and the bipolar theorem
DefinitionTopological annihilator#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), with continuous dual \(E^*\). The topological annihilator of a subspace \(S\) of \(E\) is the subspace of \(E^*\) consisting of the continuous linear functionals \(f\) with \(f(x) = 0\) for all \(x \in S\).
def topologicalAnnihilator (S : Submodule 𝕜 E) : Submodule 𝕜 (E →L[𝕜] 𝕜) where
carrier := { f | ∀ x ∈ S, f x = 0 }
zero_mem' := fun _ _ => by simp
add_mem' := fun hf hg x hx => by simp [hf x hx, hg x hx]
smul_mem' := fun c f hf x hx => by simp [hf x hx]Used by 12
DefinitionTopological coannihilator#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), with continuous dual \(E^*\). The topological coannihilator of a subspace \(\Phi\) of \(E^*\) is the subspace of \(E\) consisting of the vectors \(x\) with \(f(x) = 0\) for all \(f \in \Phi\).
def topologicalCoannihilator (Φ : Submodule 𝕜 (E →L[𝕜] 𝕜)) : Submodule 𝕜 E where
carrier := { x | ∀ f ∈ Φ, f x = 0 }
zero_mem' := fun _ _ => by simp
add_mem' := fun hx hy f hf => by simp [hx f hf, hy f hf]
smul_mem' := fun c x hx f hf => by simp [hx f hf]Used by 9
TheoremMembership in the topological annihilator#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), let \(S\) be a subspace of \(E\), and let \(f : E \to \mathbb{K}\) be a continuous linear functional. Then \(f\) lies in the topological annihilator of \(S\) if and only if \(f(x) = 0\) for every \(x \in S\).
theorem mem_topologicalAnnihilator {S : Submodule 𝕜 E} {f : E →L[𝕜] 𝕜} :
f ∈ S.topologicalAnnihilator ↔ ∀ x ∈ S, f x = 0Uses 1 · Used by 6
TheoremMembership in the topological coannihilator#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), let \(\Phi\) be a subspace of the continuous dual of \(E\), and let \(x \in E\). Then \(x\) lies in the topological coannihilator of \(\Phi\) if and only if \(f(x) = 0\) for every \(f \in \Phi\).
theorem mem_topologicalCoannihilator {Φ : Submodule 𝕜 (E →L[𝕜] 𝕜)} {x : E} :
x ∈ Φ.topologicalCoannihilator ↔ ∀ f ∈ Φ, f x = 0Uses 1 · Used by 5
TheoremThe topological annihilator reverses inclusion#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), and let \(S \subseteq T\) be subspaces of \(E\). Then the topological annihilator of \(T\) is contained in the topological annihilator of \(S\).
theorem topologicalAnnihilator_anti {S T : Submodule 𝕜 E} (h : S ≤ T) :
T.topologicalAnnihilator ≤ S.topologicalAnnihilatorUses 2 · Used by 1
TheoremThe topological coannihilator is antitone#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), with continuous dual \(E^*\). If \(\Phi \subseteq \Psi\) are subspaces of \(E^*\), then the topological coannihilator of \(\Psi\) is contained in the topological coannihilator of \(\Phi\).
theorem topologicalCoannihilator_anti {Φ Ψ : Submodule 𝕜 (E →L[𝕜] 𝕜)} (h : Φ ≤ Ψ) :
Ψ.topologicalCoannihilator ≤ Φ.topologicalCoannihilatorUses 2
TheoremTopological annihilator of the zero subspace#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\). The topological annihilator of the zero subspace of \(E\) is the whole continuous dual of \(E\).
@[simp]
theorem topologicalAnnihilator_bot :
(⊥ : Submodule 𝕜 E).topologicalAnnihilator = ⊤Uses 1
TheoremTopological annihilator of the whole space#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), with continuous dual \(E^*\). The topological annihilator of \(E\), viewed as a subspace of itself, is the zero subspace of \(E^*\): a continuous linear functional vanishing everywhere on \(E\) is zero.
@[simp]
theorem topologicalAnnihilator_top :
(⊤ : Submodule 𝕜 E).topologicalAnnihilator = ⊥Uses 2 · Used by 1
TheoremTopological coannihilator of the zero subspace#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), with continuous dual \(E^*\). The topological coannihilator of the zero subspace of \(E^*\) is all of \(E\).
@[simp]
theorem topologicalCoannihilator_bot :
(⊥ : Submodule 𝕜 (E →L[𝕜] 𝕜)).topologicalCoannihilator = ⊤Uses 1 · Used by 1
TheoremTopological coannihilator of the whole dual#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), with continuous dual \(E^*\). The topological coannihilator of \(E^*\) itself is the zero subspace of \(E\): a vector killed by every continuous linear functional is zero.
The proof uses the Hahn–Banach norming functional.
theorem topologicalCoannihilator_top :
(⊤ : Submodule 𝕜 (E →L[𝕜] 𝕜)).topologicalCoannihilator = ⊥Uses 2
TheoremA subspace lies in its double annihilator#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\). Every subspace \(S\) of \(E\) is contained in the topological coannihilator of the topological annihilator of \(S\).
theorem le_topologicalCoannihilator_topologicalAnnihilator (S : Submodule 𝕜 E) :
S ≤ S.topologicalAnnihilator.topologicalCoannihilatorUses 4 · Used by 1
TheoremTopological annihilator of the closure#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). For every subspace \(S\) of \(E\), the topological annihilator of the topological closure \(\overline{S}\) equals the topological annihilator of \(S\): a continuous linear functional vanishing on \(S\) vanishes on \(\overline{S}\).
theorem topologicalAnnihilator_topologicalClosure (S : Submodule 𝕜 E) :
S.topologicalClosure.topologicalAnnihilator = S.topologicalAnnihilatorUses 3 · Used by 3
TheoremSeparation#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), let \(S\) be a subspace of \(E\), and let \(x \in E\) lie outside the topological closure of \(S\). Then some continuous linear functional \(f\) in the topological annihilator of \(S\) satisfies \(f(x) \neq 0\).
theorem exists_mem_topologicalAnnihilator_apply_ne_zero {S : Submodule 𝕜 E} {x : E}
(hx : x ∉ S.topologicalClosure) :
∃ f ∈ S.topologicalAnnihilator, f x ≠ 0Uses 3 · Used by 2
TheoremSeparation, normalized#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), let \(S\) be a subspace of \(E\), and let \(x \in E\) lie outside the topological closure of \(S\). Then some continuous linear functional \(f\) in the topological annihilator of \(S\) satisfies \(f(x) = 1\).
theorem exists_mem_topologicalAnnihilator_apply_eq_one {S : Submodule 𝕜 E} {x : E}
(hx : x ∉ S.topologicalClosure) :
∃ f ∈ S.topologicalAnnihilator, f x = 1Uses 2
TheoremBipolar theorem#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) and let \(S\) be a subspace of \(E\). The topological coannihilator of the topological annihilator of \(S\), that is, the subspace of vectors of \(E\) killed by every continuous linear functional vanishing on \(S\), is the topological closure of \(S\).
theorem topologicalAnnihilator_topologicalCoannihilator_eq_topologicalClosure
(S : Submodule 𝕜 E) :
S.topologicalAnnihilator.topologicalCoannihilator = S.topologicalClosureUses 6 · Used by 2
TheoremDensity criterion via the annihilator#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), and let \(S\) be a subspace of \(E\). The topological annihilator of \(S\) is the zero subspace of the continuous dual of \(E\) if and only if \(S\) is dense in \(E\).
TheoremThe annihilator determines the closure#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), and let \(S\) and \(T\) be subspaces of \(E\). Then \(S\) and \(T\) have the same topological annihilator if and only if they have the same topological closure.
theorem topologicalAnnihilator_eq_iff_topologicalClosure_eq {S T : Submodule 𝕜 E} :
S.topologicalAnnihilator = T.topologicalAnnihilator ↔
S.topologicalClosure = T.topologicalClosureUses 4
TheoremTopological annihilator of a sum of subspaces#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), and let \(S\) and \(T\) be subspaces of \(E\). The topological annihilator of \(S + T\) is the intersection of the topological annihilators of \(S\) and \(T\).
theorem topologicalAnnihilator_sup (S T : Submodule 𝕜 E) :
(S ⊔ T).topologicalAnnihilator =
S.topologicalAnnihilator ⊓ T.topologicalAnnihilatorUses 2
TheoremTopological coannihilator of a sum of subspaces#✓fully proved
Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), with continuous dual \(E^*\). For subspaces \(\Phi\) and \(\Psi\) of \(E^*\), the topological coannihilator of their supremum \(\Phi + \Psi\) is the intersection of the topological coannihilators of \(\Phi\) and \(\Psi\).
theorem topologicalCoannihilator_sup (Φ Ψ : Submodule 𝕜 (E →L[𝕜] 𝕜)) :
(Φ ⊔ Ψ).topologicalCoannihilator =
Φ.topologicalCoannihilator ⊓ Ψ.topologicalCoannihilatorUses 2
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.