SeparableInvariant.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A separable closed convex invariant subset

Starting at one point, repeatedly adjoin its current set's image and take the closed convex hull. The closure of the increasing union is invariant. The map always has domain C; no ambient extension is used.

def OAI.ReflexiveFixedPoints.separableInvariantStage line 26

Source documentation

The successive closed convex hulls used in the separable reduction.

private def separableInvariantStage (C : Set X) (F : C → C) (a : X) : ℕ → Set X
  | 0 => {a}
  | n + 1 => closure (convexHull ℝ
      (separableInvariantStage C F a n ∪
        (fun x : C => (F x : X)) ''
          ((Subtype.val : C → X) ⁻¹' separableInvariantStage C F a n)))

/-- Every nonempty closed bounded convex set with a nonexpansive self-map
contains a nonempty closed bounded convex separable invariant subset. -/

theorem OAI.ReflexiveFixedPoints.exists_separable_invariant_subset line 35

Source documentation

Every nonempty closed bounded convex set with a nonexpansive self-map contains a nonempty closed bounded convex separable invariant subset.

theorem exists_separable_invariant_subset {C : Set X}
    (hne : C.Nonempty) (hclosed : IsClosed C) (hbounded : Bornology.IsBounded C)
    (hconvex : Convex ℝ C) (F : C → C) (hF : LipschitzWith 1 F) :
    ∃ S : Set X, S ⊆ C ∧ S.Nonempty ∧ IsClosed S ∧ Bornology.IsBounded S ∧
      Convex ℝ S ∧ IsSeparable S ∧ InvariantSubset C F S := by
…

Mentions: OAI.ReflexiveFixedPoints.InvariantSubset