ReturnMapFixedPoint.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed point from the return map's radius estimates

The finite-bin noncompactness estimate and the proved condensing fixed-point theorem discharge the analytic step from the elementary geometric data. Continuity is needed only on the actual invariant closed convex set.

theorem OAI.Tingley.exists_fixedPoint_of_return_estimate line 22

Source documentation

The radius bounds and two-point estimate imply an actual fixed point. The hypotheses contain neither a noncompactness estimate nor a fixed-point principle: both are supplied by the preceding constructive proofs.

theorem exists_fixedPoint_of_return_estimate
    {C : Set X} {g : X → X} {p s u r : X → ℝ} {t M : ℝ}
    (ht0 : 0 < t) (ht1 : t < 1) (hM : 0 < M)
    (hCne : C.Nonempty) (hCclosed : IsClosed C)
    (hCb : Bornology.IsBounded C) (hCconvex : Convex ℝ C)
    (hg : ContinuousOn g C) (hgC : Set.MapsTo g C C)
    (hbounds : ∀ v ∈ C,
      (1 - t ≤ p v ∧ p v ≤ 1 + t) ∧
      (1 - t ≤ s v ∧ s v ≤ 1 + t) ∧
      (1 - t ≤ u v ∧ u v ≤ 1 + t) ∧
      (1 - t ≤ r v ∧ r v ≤ 1 + t))
    (hs : ∀ v ∈ C, s v = p v + M)
…