English
A continuous map f on X×Y with values in a uniformly structured V can be uniformly approximated by finite sums of tensors of the form f_x g_y, i.e., there exist n and families g_i, h_i that make f(x,y) close in the uniformity sense to ∑ g_i(x) h_i(y) for all x,y.
Русский
Пусть f: X×Y → V непрерывна; тогда f может быть приблизительно аппроксимирована конечной суммой тензоров f(x,y) ≈ ∑ g_i(x) h_i(y) в рамкахuniformity пространства V.
LaTeX
$$$\\exists n\\, (g: Fin n \\to C(X, \\mathbb{R}))\\, (h: Fin n \\to C(Y, V))\\; \\forall x,y, (f(x,y), \\sum_i g_i(x) \\cdot h_i(y)) \\in S$$$
Lean4
/-- A continuous function on `X × Y`, taking values in an `R`-module with a uniform structure,
can be uniformly approximated by sums of functions of the form `(x, y) ↦ f x • g y`.
Note that no continuity properties are assumed either for multiplication on `R`, or for the scalar
multiplication of `R` on `V`. -/
theorem exists_finite_sum_smul_approximation_of_mem_uniformity [TopologicalSpace R] [MonoidWithZero R]
[MulActionWithZero R V] (f : C(X × Y, V)) (hS : S ∈ 𝓤 V) :
∃ (n : ℕ) (g : Fin n → C(X, R)) (h : Fin n → C(Y, V)), ∀ x y, (f (x, y), ∑ i, g i x • h i y) ∈ S :=
by
have hS' : {(f, g) | ∀ y, (f y, g y) ∈ S} ∈ 𝓤 C(Y, V) :=
(mem_compactConvergence_entourage_iff _).mpr
⟨_, _, isCompact_univ, hS, by simp only [Set.mem_univ, true_implies, subset_refl]⟩
obtain ⟨n, U, v, hv⟩ :=
exists_finite_sum_const_indicator_approximation_of_mem_nhds_diagonal f.curry (nhdsSet_diagonal_le_uniformity hS')
refine ⟨n, fun i ↦ ⟨_, (U i).isClopen.continuous_indicator <| continuous_const (y := 1)⟩, v, fun x y ↦ ?_⟩
convert hv x y using 2
simp only [sum_apply]
congr 1 with i
by_cases hi : x ∈ U i <;> simp [hi]
