F-spaces

DefinitionSpaces of type (F)#✓fully proved

A real vector space \(E\) with a topology is of type (F) when addition \(E \times E \to E\) and scalar multiplication \(\mathbb{R} \times E \to E\) are continuous and there is a metric \(d\) on \(E\) that is translation invariant, \(d(x + z, y + z) = d(x, y)\) for all \(x, y, z \in E\), that induces the topology of \(E\), and that is complete: every Cauchy sequence for \(d\) converges for \(d\).

def IsTypeF (E : Type) [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] : Prop :=
  ∃ d : E → E → ℝ, (∀ x y, 0 ≤ d x y) ∧ (∀ x y, d x y = 0 ↔ x = y) ∧
    (∀ x y, d x y = d y x) ∧ (∀ x y z, d x z ≤ d x y + d y z) ∧
    (∀ x y z, d (x + z) (y + z) = d x y) ∧
    (∀ U : Set E, IsOpen U ↔ ∀ x ∈ U, ∃ ε > 0, ∀ y, d y x < ε → y ∈ U) ∧
    (∀ x : ℕ → E, (∀ ε > 0, ∃ N, ∀ m n, m ≥ N → n ≥ N → d (x m) (x n) < ε) →
      ∃ y, ∀ ε > 0, ∃ N, ∀ n, n ≥ N → d (x n) y < ε) ∧
    Continuous (fun p : E × E => p.1 + p.2) ∧ Continuous fun p : ℝ × E => p.1 • p.2

Used by 1

Used byScottish Book Problem 15.1

DefinitionSpheres in the ray sense#✓fully proved

Let \(E\) be a real vector space. A set \(K \subseteq E\) is a sphere when \(0 \notin K\) and for every \(x \ne 0\) in \(E\) there is exactly one real \(t > 0\) with \(t x \in K\); that is, every open ray from the origin meets \(K\) exactly once.

def IsSphere (E : Type) [AddCommGroup E] [Module ℝ E] (K : Set E) : Prop :=
  0 ∉ K ∧ ∀ x : E, x ≠ 0 → ∃! t : ℝ, 0 < t ∧ t • x ∈ K

Used by 1

Used byScottish Book Problem 15.1

DefinitionSequentially bounded sets#✓fully proved

Let \(E\) be a real vector space with a topology. A set \(R \subseteq E\) is bounded when for every sequence \((x_n)\) of points of \(R\) and every sequence \((t_n)\) of real numbers with \(t_n \to 0\), the sequence \((t_n x_n)\) tends to \(0\) in \(E\).

This is the definition of boundedness as printed in the statement of Scottish Book Problem 15.1.

def IsBoundedSet (E : Type) [TopologicalSpace E] [AddCommGroup E] [Module ℝ E]
    (R : Set E) : Prop :=
  ∀ (x : ℕ → E) (t : ℕ → ℝ), (∀ n, x n ∈ R) →
    Filter.Tendsto t Filter.atTop (nhds 0) →
    Filter.Tendsto (fun n => t n • x n) Filter.atTop (nhds 0)

Used by 1

Used byScottish Book Problem 15.1

DefinitionSpaces of type (B)#✓fully proved

A real vector space \(E\) with a topology is of type (B) when there is a function \(\|\cdot\| : E \to \mathbb{R}\) with \(\|x\| \ge 0\), with \(\|x\| = 0\) exactly when \(x = 0\), with \(\|x + y\| \le \|x\| + \|y\|\) and with \(\|a x\| = |a| \, \|x\|\) for all \(x, y \in E\) and \(a \in \mathbb{R}\), such that a set \(U \subseteq E\) is open exactly when every \(x \in U\) has an \(\varepsilon > 0\) with \(y \in U\) whenever \(\|y - x\| < \varepsilon\), and such that every Cauchy sequence for \(\|\cdot\|\) converges in \(E\) for \(\|\cdot\|\).

def AdmitsBanachNorm (E : Type) [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] : Prop :=
  ∃ normFn : E → ℝ, (∀ x, 0 ≤ normFn x) ∧ (∀ x, normFn x = 0 ↔ x = 0) ∧
    (∀ x y, normFn (x + y) ≤ normFn x + normFn y) ∧
    (∀ (a : ℝ) (x : E), normFn (a • x) = |a| * normFn x) ∧
    (∀ U : Set E, IsOpen U ↔ ∀ x ∈ U, ∃ ε > 0, ∀ y, normFn (y - x) < ε → y ∈ U) ∧
    (∀ x : ℕ → E, (∀ ε > 0, ∃ N, ∀ m n, m ≥ N → n ≥ N → normFn (x m - x n) < ε) →
      ∃ y, ∀ ε > 0, ∃ N, ∀ n, n ≥ N → normFn (x n - y) < ε)

Used by 1

Used byScottish Book Problem 15.1

DefinitionScottish Book Problem 15.1#✓fully proved

The claim of Mazur and Orlicz that every real vector space \(E\) with a topology that is of type (F) and contains a bounded sphere is of type (B).

def ScottishBookProblem15Point1Claim : Prop :=
  ∀ (E : Type) [TopologicalSpace E] [AddCommGroup E] [Module ℝ E],
    IsTypeF E → (∃ K : Set E, IsSphere E K ∧ IsBoundedSet E K) → AdmitsBanachNorm E

Uses 4 · Used by 1

Statement usesSpaces of type (B) · Sequentially bounded sets · Spheres in the ray sense · Spaces of type (F)

Used byNegative answer to Scottish Book Problem 15.1

TheoremNegative answer to Scottish Book Problem 15.1#●ready to prove

The Mazur–Orlicz claim of Problem 15.1 is false: there is a real vector space \(E\) with a topology that is of type (F) and contains a bounded sphere, but is not of type (B).

theorem_wanted boundedSphereFImpliesB_refuted : ¬ ScottishBookProblem15Point1Claim

Sources

• S. Mazur and W. Orlicz, Problem 15.1 of the Scottish Book; the typescript itself records the negative answer (Ad 15.1, Mazur, May 1 1937) with the spaces ℓ ^ p and L ^ p for 0 < p < 1, with quasi-norm given by the sum (respectively integral) of |·| ^ p, as counterexamples: they are of type (F), possess a bounded sphere, and are not normable, hence not of type (B).

Uses 1

Statement usesScottish Book Problem 15.1

DefinitionSpaces of type (F) in Scottish Book Problem 26#✓fully proved

A real vector space \(E\) with a topology is of type (F) if there is a metric \(d\) on \(E\) that induces its topology, is translation invariant, \(d(x + z, y + z) = d(x, y)\) for all \(x, y, z \in E\), and is complete, and if addition \(E \times E \to E\) and scalar multiplication \(\mathbb{R} \times E \to E\) are continuous.

def IsTypeF (E : Type) [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] : Prop :=
  ∃ d : E → E → ℝ, (∀ x y, 0 ≤ d x y) ∧ (∀ x y, d x y = 0 ↔ x = y) ∧
    (∀ x y, d x y = d y x) ∧ (∀ x y z, d x z ≤ d x y + d y z) ∧
    (∀ x y z, d (x + z) (y + z) = d x y) ∧
    (∀ U : Set E, IsOpen U ↔ ∀ x ∈ U, ∃ ε > 0, ∀ y, d y x < ε → y ∈ U) ∧
    (∀ x : ℕ → E, (∀ ε > 0, ∃ N, ∀ m n, m ≥ N → n ≥ N → d (x m) (x n) < ε) →
      ∃ y, ∀ ε > 0, ∃ N, ∀ n, n ≥ N → d (x n) y < ε) ∧
    Continuous (fun p : E × E => p.1 + p.2) ∧ Continuous fun p : ℝ × E => p.1 • p.2

Used by 1

Used bySpaces of type \(\{F_o\}\)

DefinitionBounded sets in Scottish Book Problem 26#✓fully proved

Let \(E\) be a real vector space with a topology. A set \(R \subseteq E\) is bounded if for every sequence \((x_n)_{n \ge 0}\) of points of \(R\) and every real sequence \((t_n)_{n \ge 0}\) with \(t_n \to 0\), we have \(t_n x_n \to 0\) in \(E\).

This sequential definition is the one printed in the problem statement.

def IsBoundedSet (E : Type) [TopologicalSpace E] [AddCommGroup E] [Module ℝ E]
    (R : Set E) : Prop :=
  ∀ (x : ℕ → E) (t : ℕ → ℝ), (∀ n, x n ∈ R) →
    Filter.Tendsto t Filter.atTop (nhds 0) →
    Filter.Tendsto (fun n => t n • x n) Filter.atTop (nhds 0)

Used by 1

Used byScottish Book Problem 26 (Mazur and Orlicz's claim)

DefinitionSpaces of type \(\{F_o\}\)#✓fully proved

A real vector space \(E\) with a topology is of type \(\{F_o\}\) if it is of type (F) and, for every sequence \((x_n)_{n \ge 0}\) in \(E\) with \(x_n \to 0\) and every real sequence \((t_n)_{n \ge 0}\) with \(\sum_n |t_n| < \infty\), the series \(\sum_n t_n x_n\) converges in \(E\).

def IsTypeFo (E : Type) [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] : Prop :=
  IsTypeF E ∧ ∀ (x : ℕ → E) (t : ℕ → ℝ),
    Filter.Tendsto x Filter.atTop (nhds 0) → Summable (fun n => |t n|) →
    ∃ y, Filter.Tendsto (fun N => ∑ n ∈ Finset.range N, t n • x n)
      Filter.atTop (nhds y)

Uses 1 · Used by 1

Statement usesSpaces of type (F) in Scottish Book Problem 26

Used byScottish Book Problem 26 (Mazur and Orlicz's claim)

DefinitionScottish Book Problem 26 (Mazur and Orlicz's claim)#✓fully proved

The claim that for every real vector space \(E\) with a topology that is of type \(\{F_o\}\) and every sequence \((F_n)_{n \ge 0}\) of linear functionals \(E \to \mathbb{R}\), if \(F_n \to 0\) uniformly on every bounded set \(R \subseteq E\), then there is an open set \(U \subseteq E\) containing \(0\) on which \(F_n \to 0\) uniformly.

Here \(F_n \to 0\) uniformly on a set \(S\) means that for every \(\varepsilon > 0\) there is \(N\) with \(|F_n(x)| < \varepsilon\) for all \(n \ge N\) and all \(x \in S\). The \(F_n\) are only assumed linear, not continuous.

def ScottishBookProblem26Claim : Prop :=
  ∀ (E : Type) [TopologicalSpace E] [AddCommGroup E] [Module ℝ E],
    IsTypeFo E →
    ∀ (F : ℕ → E →ₗ[ℝ] ℝ),
      (∀ R : Set E, IsBoundedSet E R →
        ∀ ε > 0, ∃ N, ∀ n, n ≥ N → ∀ x ∈ R, |F n x| < ε) →
      ∃ U : Set E, IsOpen U ∧ (0 : E) ∈ U ∧
        ∀ ε > 0, ∃ N, ∀ n, n ≥ N → ∀ x ∈ U, |F n x| < ε

Uses 2 · Used by 1

Statement usesBounded sets in Scottish Book Problem 26 · Spaces of type \(\{F_o\}\)

Used byMazur and Orlicz's Problem 26 has a negative answer

TheoremMazur and Orlicz's Problem 26 has a negative answer#●ready to prove

The claim of Scottish Book Problem 26 is false: there are a real vector space \(E\) with a topology, of type \(\{F_o\}\), and a sequence \((F_n)_{n \ge 0}\) of linear functionals \(E \to \mathbb{R}\) that converges to \(0\) uniformly on every bounded subset of \(E\) but does not converge to \(0\) uniformly on any open set containing \(0\).

theorem_wanted foBoundedUniformNeighborhood_refuted : ¬ ScottishBookProblem26Claim

Sources

• S. Mazur and W. Orlicz, Problem 26 of the Scottish Book (prize: one small beer); the typescript itself records the answer on the same page: "Ad 26, The answer is negative. M. Eidelheit, June 4, 1938."

Uses 1

Statement usesScottish Book Problem 26 (Mazur and Orlicz's claim)

9 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.