CompactApproximation.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Finite-net approximate fixed points on a compact convex set

The coefficient map is the explicit normalization of the weights max (δ - dist (P i) y) 0. The simplex fixed point is applied to this actual map composed with the actual barycenter and the given self-map.

def OAI.Tingley.compactNetWeight line 28
def OAI.Tingley.compactNetTotal line 31
def OAI.Tingley.compactNetCoefficients line 34
theorem OAI.Tingley.compactNetWeight_nonneg line 38
theorem OAI.Tingley.compactNetWeight_pos line 42
theorem OAI.Tingley.compactNetTotal_pos line 47
theorem OAI.Tingley.compactNetCoefficients_nonneg line 56
theorem OAI.Tingley.compactNetCoefficients_sum line 62
theorem OAI.Tingley.compactNetCoefficients_pos line 70
theorem OAI.Tingley.compactNetCoefficients_active line 76
def OAI.Tingley.compactNetCoefficientMap line 84
theorem OAI.Tingley.continuous_compactNetCoefficientMap line 91
def OAI.Tingley.compactNetBarycenter line 103
theorem OAI.Tingley.compactNetBarycenter_mem line 106
theorem OAI.Tingley.continuous_compactNetBarycenter line 111
theorem OAI.Tingley.compactNet_sum_sub_lt line 119
Source documentation
The normalized finite-net average is strictly less than the net radius away from its argument. Zero weights are allowed.
```
theorem compactNet_sum_sub_lt {P : ι → E} {δ : ℝ} {y : E}
    (hnet : ∃ i, dist (P i) y < δ) :
    ‖(∑ i, compactNetCoefficients P δ y i • P i) - y‖ < δ := by
…
```
Mentions: OAI.Tingley.compactNetCoefficients

theorem OAI.Tingley.exists_approximate_fixedPoint_of_isCompact_convex line 152

Source documentation

The simplex theorem, applied to the actual normalized net weights, produces approximate fixed points for any compact convex self-map.

theorem exists_approximate_fixedPoint_of_isCompact_convex
    {K : Set E} (hK : IsCompact K) (hne : K.Nonempty) (hconv : Convex ℝ K)
    {g : E → E} (hg : ContinuousOn g K) (hmap : MapsTo g K K)
    {δ : ℝ} (hδ : 0 < δ) : ∃ x ∈ K, ‖x - g x‖ < δ := by
…