CondensingFixedPoint.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed points from a Kuratowski contraction

The compact invariant set is the intersection of the actual iterated closed-convex images. All of its required properties are proved from the original closed bounded convex invariant set and the all-subsets estimate.

theorem OAI.Tingley.exists_fixedPoint_of_kuratowski_contraction line 26

Source documentation

A continuous self-map satisfying the actual all-subsets Kuratowski contraction has a fixed point. No compactness premise on C is required.

theorem exists_fixedPoint_of_kuratowski_contraction
    {C : Set E} (hne : C.Nonempty) (hclosed : IsClosed C)
    (hbounded : Bornology.IsBounded C) (hconv : Convex ℝ C)
    {g : E → E} (hg : ContinuousOn g C) (hmap : MapsTo g C C)
    {γ : ℝ} (hγ0 : 0 ≤ γ) (hγ1 : γ < 1)
    (hχ : ∀ H : Set E, H ⊆ C → chi (g '' H) ≤ γ * chi H) :
    ∃ x ∈ C, g x = x := by
…

Mentions: OAI.Tingley.chi

theorem OAI.Tingley.continuous_condensing_fixedPoint line 56

Source documentation

The subtype formulation measures the actual ambient images of subsets of the carrier, and transports them through the explicit ambient map.

theorem continuous_condensing_fixedPoint
    {C : Set E} (hne : C.Nonempty) (hclosed : IsClosed C)
    (hbounded : Bornology.IsBounded C) (hconv : Convex ℝ C)
    (g : C → C) (hg : Continuous g) {γ : ℝ} (hγ0 : 0 ≤ γ) (hγ1 : γ < 1)
    (hχ : ∀ H : Set C,
      chi ((fun x : C => (g x : E)) '' H) ≤ γ * chi (Subtype.val '' H)) :
    ∃ x, g x = x := by
…

Mentions: OAI.Tingley.chi