FixedPoint.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Fixed points of continuous maps on compact convex sets of real-valued functions.

def OAI.MatrixMultiplication.AuxiliarySeparation.weightSimplex line 13
theorem OAI.MatrixMultiplication.AuxiliarySeparation.weightSimplex_convex line 16
theorem OAI.MatrixMultiplication.AuxiliarySeparation.weightSimplex_compact line 26

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_approximate_fixedPoint_of_weights line 47

Source documentation

A finite continuous system of barycentric weights gives an approximate fixed point. The approximation is measured on any prescribed finite set of coordinates.

theorem exists_approximate_fixedPoint_of_weights
    {I J : Type*} [Fintype J] [Nonempty J]
    {K : Set (I → ℝ)} (hK : Convex ℝ K) (f : C(K, K))
    (a : J → K) (w : J → C(K, ℝ))
    (hw0 : ∀ j x, 0 ≤ w j x) (hw1 : ∀ x, ∑ j, w j x = 1)
    (s : Finset I) (ε : ℝ)
    (hclose : ∀ x j, w j x ≠ 0 → ∀ i ∈ s, |(a j).val i - x.val i| ≤ ε) :
    ∃ x : K, ∀ i ∈ s, |(f x).val i - x.val i| ≤ ε := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_finite_partition_weights line 102
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_finite_partition_weights_nonempty line 145
theorem OAI.MatrixMultiplication.AuxiliarySeparation.compact_approx_limit line 159
theorem OAI.MatrixMultiplication.AuxiliarySeparation.compact_convex_fixedPoint line 202
Source documentation
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 compact_convex_fixedPoint {I : Type*} {K : Set (I → ℝ)}
    (hKcompact : IsCompact K) (hKconvex : Convex ℝ K) (hKne : K.Nonempty)
    (f : C(K, K)) : ∃ x : K, f x = x := by
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.compact_convex_fixedPoint_of_continuous line 219

Source documentation

An unbundled form of the product-space fixed-point theorem.

theorem compact_convex_fixedPoint_of_continuous {I : Type*} {K : Set (I → ℝ)}
    (hKcompact : IsCompact K) (hKconvex : Convex ℝ K) (hKne : K.Nonempty)
    (f : K → K) (hf : Continuous f) : ∃ x : K, f x = x :=
…