Countably many classes of unit vectors (Proposition C)

The unit vectors of a real Hilbert space fall into countably many classes such that any two vectors x, y of one class satisfy 1 + ⟪x, y⟫ ≥ η > 0 for a constant η of the class. Choose a Hilbert basis. For rationals 0 < b < a, a unit vector whose coordinates of magnitude at least a form a nonempty set S, all others having magnitude at most b, is classified by (a, b) and the sign of its coordinate at an element of S chosen by Classical.epsilon, a choice that depends only on S. Two vectors of one class differ in their supports, giving ‖x + y‖ ≥ a - b, or share the sign of a coordinate of magnitude at least a, giving ‖x + y‖ ≥ 2a.

Applied to the signs ±1 of a law in L², this gives countably many classes of vertices within which any two signs agree with probability bounded below.

theorem Erdos111.eq_zero_of_forall_inner_hilbertBasis_eq_zero {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (b : HilbertBasis ι ℝ E) {x : E} (h : ∀ (i : ι), inner ℝ (b i) x = 0) : x = 0

A vector whose coordinates in a Hilbert basis all vanish is zero.

theorem Erdos111.finite_setOf_le_abs_inner {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (b : HilbertBasis ι ℝ E) (x : E) {t : ℝ} (ht : 0 < t) : {i : ι | t ≤ |inner ℝ (b i) x|}.Finite

Only finitely many coordinates of a vector in a Hilbert basis have magnitude at least a positive t.

theorem Erdos111.exists_rat_gap {ι : Type u_1} (f : ι → ℝ) (hfin : ∀ (t : ℝ), 0 < t → {i : ι | t ≤ |f i|}.Finite) {i₀ : ι} (hi₀ : f i₀ ≠ 0) : ∃ (q : ℚ × ℚ), 0 < q.2 ∧ q.2 < q.1 ∧ (∃ (i : ι), ↑q.1 ≤ |f i|) ∧ ∀ (i : ι), |f i| < ↑q.1 → |f i| ≤ ↑q.2

A real family with a nonzero member, only finitely many of whose members exceed any positive magnitude, has rationals 0 < b < a such that some member has magnitude at least a and every member of magnitude below a has magnitude at most b.

theorem Erdos111.exists_unitVector_classes (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : ∃ (cls : E → ℕ) (η : ℕ → ℝ), (∀ (n : ℕ), 0 < η n) ∧ ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → cls x = cls y → η (cls x) ≤ 1 + inner ℝ x y

Proposition C.

theorem Erdos111.exists_sign_classes {V : Type u_1} (ν : MeasureTheory.Measure (V → Bool)) [MeasureTheory.IsProbabilityMeasure ν] : ∃ (cls : V → ℕ) (η : ℕ → NNReal), (∀ (n : ℕ), 0 < η n) ∧ ∀ (u v : V), cls u = cls v → ↑(η (cls u)) ≤ ν {ω : V → Bool | ω u = ω v}

The vertices fall into countably many classes within which any two signs agree with probability at least a positive constant of the class.