DataSeparability

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Every class of continuous forcing fields on the closed cube has a countable dense subclass

The forcing fields of Section 5.1 are continuous on the closed cube, so they are points of C(closedCubeAt y n, Vec d). That space is second countable — the closed cube is a compact second-countable locally compact space and Vec d is second countable — and second countability is inherited by every subspace, so every class of such fields, in particular the normalized one, has a countable subclass dense in it for the supremum distance. No compactness and no Arzelà–Ascoli argument is needed.

Main definitions

• extendVec y n G — the field on ℝ^d determined by a continuous field on the closed cube, through the coordinatewise retraction.

References

• ABK26, the localized error and regularity quantities of Section 5.1.

1. The field determined by a continuous field on the closed cube

noncomputable def Algsuperdiff.Section5.Support.extendVec {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (G : C(↑(closedCubeAt y n), HCPolySupport.Vec d)) : HCPolySupport.Vec d → HCPolySupport.Vec d

The forcing field determined by a continuous field on the closed cube.

Equations

• Algsuperdiff.Section5.Support.extendVec y n G x = G ⟨Algsuperdiff.Section5.Support.clampTo y n x, ⋯⟩

theorem Algsuperdiff.Section5.Support.extendVec_apply_of_mem {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} (G : C(↑(closedCubeAt y n), HCPolySupport.Vec d)) {x : HCPolySupport.Vec d} (hx : x ∈ closedCubeAt y n) : extendVec y n G x = G ⟨x, hx⟩

2. Every class has a countable dense subclass

theorem Algsuperdiff.Section5.Support.exists_countable_subset_dense {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (s : Set C(↑(closedCubeAt y n), HCPolySupport.Vec d)) : ∃ (t : Set C(↑(closedCubeAt y n), HCPolySupport.Vec d)), t.Countable ∧ t ⊆ s ∧ ∀ F ∈ s, ∀ (eps : ℝ), 0 < eps → ∃ G ∈ t, dist G F < eps

Second countability supplies the countable subclass. For every class of continuous fields on the closed cube and every member of it, some member of a fixed countable subclass is arbitrarily close in the supremum distance.