Fixed points of continuous maps on compact convex sets of real-valued functions.
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_approximate_fixedPoint_of_weights
{I : Type u_1}
{J : Type u_2}
[Fintype J]
[Nonempty J]
{K : Set (I → ℝ)}
(hK : Convex ℝ K)
(f : C(↑K, ↑K))
(a : J → ↑K)
(w : J → C(↑K, ℝ))
(hw0 : ∀ (j : J) (x : ↑K), 0 ≤ (w j) x)
(hw1 : ∀ (x : ↑K), ∑ j : J, (w j) x = 1)
(s : Finset I)
(ε : ℝ)
(hclose : ∀ (x : ↑K) (j : J), (w j) x ≠ 0 → ∀ i ∈ s, |↑(a j) i - ↑x i| ≤ ε)
:
A finite continuous system of barycentric weights gives an approximate fixed point. The approximation is measured on any prescribed finite set of coordinates.
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.compact_approx_limit
{I : Type u_1}
{K : Set (I → ℝ)}
(hK : IsCompact K)
(_hne : K.Nonempty)
(f : ↑K → I → ℝ)
(hf : Continuous f)
(happrox : ∀ (s : Finset I) (ε : ℝ), 0 < ε → ∃ (x : ↑K), ∀ i ∈ s, |f x i - ↑x i| ≤ ε)
:
∃ (x : ↑K), f x = ↑x
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.compact_convex_fixedPoint
{I : Type u_1}
{K : Set (I → ℝ)}
(hKcompact : IsCompact K)
(hKconvex : Convex ℝ K)
(hKne : K.Nonempty)
(f : C(↑K, ↑K))
:
∃ (x : ↑K), f x = x
Schauder--Tychonoff for an arbitrary product of real lines. Compactness of the set, rather than finite dimensionality of the ambient space, is the hypothesis.
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.compact_convex_fixedPoint_of_continuous
{I : Type u_1}
{K : Set (I → ℝ)}
(hKcompact : IsCompact K)
(hKconvex : Convex ℝ K)
(hKne : K.Nonempty)
(f : ↑K → ↑K)
(hf : Continuous f)
:
∃ (x : ↑K), f x = x
An unbundled form of the product-space fixed-point theorem.