Stone--Weierstrass on products

This file packages the subalgebra of real continuous functions on a finite product generated by one-coordinate functions. It proves that this subalgebra separates points, and hence is uniformly dense when the factor is compact.

Membership in PiContinuousMap.coordinateSubalgebra expresses precisely that a function is obtained from one-coordinate functions using finitely many constants, sums, and products. Thus the approximation theorem is a reusable bundled form of finite-product test function density.

The coordinate pullback of a function in C₀(α, ℝ) need not itself vanish at infinity on the whole product. Accordingly, coordinateC0Subalgebra is a subalgebra of continuous maps; the C₀ designation records its one-coordinate generators, not its ambient carrier.

def MarkovProcess.PiContinuousMap.coordinate {I : Type u_1} {α : Type u_2} [TopologicalSpace α] (i : I) (f : C(α, ℝ)) : C(I → α, ℝ)

Pull a continuous function on one factor back along a coordinate projection.

Equations

• MarkovProcess.PiContinuousMap.coordinate i f = f.comp { toFun := fun (x : I → α) => x i, continuous_toFun := ⋯ }

@[simp]

theorem MarkovProcess.PiContinuousMap.coordinate_apply {I : Type u_1} {α : Type u_2} [TopologicalSpace α] (i : I) (f : C(α, ℝ)) (x : I → α) : (coordinate i f) x = f (x i)

def MarkovProcess.PiContinuousMap.coordinateSubalgebra {I : Type u_1} {α : Type u_2} [TopologicalSpace α] : Subalgebra ℝ C(I → α, ℝ)

The algebra generated by pullbacks of continuous functions from individual factors.

Equations

• MarkovProcess.PiContinuousMap.coordinateSubalgebra = Algebra.adjoin ℝ {g : C(I → α, ℝ) | ∃ (i : I) (f : C(α, ℝ)), g = MarkovProcess.PiContinuousMap.coordinate i f}

theorem MarkovProcess.PiContinuousMap.coordinate_mem_coordinateSubalgebra {I : Type u_1} {α : Type u_2} [TopologicalSpace α] (i : I) (f : C(α, ℝ)) : coordinate i f ∈ coordinateSubalgebra

def MarkovProcess.PiContinuousMap.coordinateC0Subalgebra {I : Type u_1} {α : Type u_2} [TopologicalSpace α] : Subalgebra ℝ C(I → α, ℝ)

The algebra generated by coordinate pullbacks of functions vanishing at infinity.

Equations

• MarkovProcess.PiContinuousMap.coordinateC0Subalgebra = Algebra.adjoin ℝ {g : C(I → α, ℝ) | ∃ (i : I) (f : ZeroAtInftyContinuousMap α ℝ), g = MarkovProcess.PiContinuousMap.coordinate i ↑f}

theorem MarkovProcess.PiContinuousMap.coordinate_c0_mem_coordinateC0Subalgebra {I : Type u_1} {α : Type u_2} [TopologicalSpace α] (i : I) (f : ZeroAtInftyContinuousMap α ℝ) : coordinate i ↑f ∈ coordinateC0Subalgebra

theorem MarkovProcess.PiContinuousMap.coordinateSubalgebra_separatesPoints {I : Type u_1} {α : Type u_2} [TopologicalSpace α] [T35Space α] : coordinateSubalgebra.SeparatesPoints

If continuous real functions separate points of the factor, the algebra generated by one-coordinate functions separates points of every product.

theorem MarkovProcess.PiContinuousMap.coordinateC0Subalgebra_separatesPoints {I : Type u_1} {α : Type u_2} [TopologicalSpace α] [T3Space α] [LocallyCompactSpace α] : coordinateC0Subalgebra.SeparatesPoints

On a locally compact regular factor, one-coordinate C₀ functions already separate points of every product.

theorem MarkovProcess.PiContinuousMap.exists_coordinateC0Subalgebra_near_on_isCompact {I : Type u_1} {α : Type u_2} [TopologicalSpace α] [T3Space α] [LocallyCompactSpace α] (f : C(I → α, ℝ)) {K : Set (I → α)} (hK : IsCompact K) {epsilon : ℝ} (hepsilon : 0 < epsilon) : ∃ g ∈ coordinateC0Subalgebra, ∀ x ∈ K, ‖g x - f x‖ < epsilon

On every compact subset of a product, restrictions of globally continuous functions can be approximated uniformly by algebraic combinations of one-coordinate C₀ functions.

theorem MarkovProcess.PiContinuousMap.coordinateSubalgebra_topologicalClosure_eq_top {I : Type u_1} {α : Type u_2} [TopologicalSpace α] [T35Space α] [CompactSpace α] : coordinateSubalgebra.topologicalClosure = ⊤

Finite algebraic combinations of one-coordinate continuous functions are uniformly dense in the continuous real functions on a compact finite product.

theorem MarkovProcess.PiContinuousMap.exists_coordinateSubalgebra_near {I : Type u_1} {α : Type u_2} [TopologicalSpace α] [T35Space α] [CompactSpace α] (f : C(I → α, ℝ)) {epsilon : ℝ} (hepsilon : 0 < epsilon) : ∃ (g : ↥coordinateSubalgebra), ‖↑g - f‖ < epsilon

Epsilon form of finite-product test-function density.