Banach–Alaoglu theorem

DefinitionWeak-star polar#✓fully proved

For a real topological vector space \(E\) and a subset \(s \subseteq E\), the weak-star polar of \(s\) is the set of continuous linear functionals \(\varphi\) on \(E\), viewed as elements of the weak dual of \(E\), such that \(|\varphi(x)| \le 1\) for every \(x \in s\).

def weakStarPolar (E : Type*) [AddCommGroup E] [Module ℝ E] [TopologicalSpace E]
    [ContinuousAdd E] [ContinuousSMul ℝ E] (s : Set E) : Set (WeakDual ℝ E) :=
  {φ | ∀ x ∈ s, ‖φ x‖ ≤ 1}

Used by 1

Used byBanach–Alaoglu–Bourbaki theorem

TheoremBanach–Alaoglu–Bourbaki theorem#●ready to prove

Let \(E\) be a real locally convex topological vector space and let \(U\) be a neighbourhood of \(0\) in \(E\). Then the weak-star polar of \(U\) is compact in the weak dual of \(E\), that is, in the space of continuous linear functionals on \(E\) with the weak-star topology.

public theorem_wanted banach_alaoglu_bourbaki (E : Type*) [AddCommGroup E] [Module ℝ E]
    [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E]
    [LocallyConvexSpace ℝ E] (U : Set E) (_hU : U ∈ 𝓝 (0 : E)) :
    IsCompact (weakStarPolar E U)

Sources

• N. Bourbaki, Espaces vectoriels topologiques; the normed case is L. Alaoglu, Ann. of Math. 41 (1940). Listed as §137 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem banach_alaoglu_bourbaki of the lean-eval benchmark.

Uses 1

Statement usesWeak-star polar

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.