A generalized Kelley cover

The countable cover below is the explicit Archimedean hypothesis used in the reconstructed infinite theorem. Each layer is a closed convex upper set over the weak-comparison cone and is bounded away from zero. Hahn--Banach supplies one positive separator per nonempty layer.

structure Scott1964.MeasurementStructures.Probability.Infinite.KelleyCover {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (C : ProperCone ℝ E) (S : Set E) : Type u_1

Countable Kelley cover of strict-comparison vectors above a closed weak comparison cone.

• layer : ℕ → Set E

  Closed convex layers separating the strict comparisons from zero.

• strictInCone : S ⊆ ↑C
• covers : S ⊆ ⋃ (n : ℕ), self.layer n
• convex (n : ℕ) : Convex ℝ (self.layer n)
• closed (n : ℕ) : IsClosed (self.layer n)
• avoidsZero (n : ℕ) : 0 ∉ self.layer n
• upper (n : ℕ) : ConeUpperSet C (self.layer n)

theorem Scott1964.MeasurementStructures.Probability.Infinite.KelleyCover.exists_separator_family {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [LocallyConvexSpace ℝ E] {C : ProperCone ℝ E} {S : Set E} (h : KelleyCover C S) : ∃ (f : ℕ → StrongDual ℝ E), (∀ (n : ℕ), ∀ c ∈ C, 0 ≤ (f n) c) ∧ ∀ (n : ℕ), ∀ x ∈ h.layer n, 0 < (f n) x

Hahn--Banach produces a positive separator for every layer, with the zero functional used harmlessly on empty layers.

theorem Scott1964.MeasurementStructures.Probability.Infinite.KelleyCover.exists_combined_separator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [LocallyConvexSpace ℝ E] {C : ProperCone ℝ E} {S : Set E} (h : KelleyCover C S) : ∃ (F : StrongDual ℝ E), (∀ c ∈ C, 0 ≤ F c) ∧ ∀ x ∈ S, 0 < F x

A summable positive combination of the layer separators is nonnegative on the weak cone and strictly positive on every covered strict vector.