MinimalInvariant.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A genuine minimal invariant set

The order is reverse inclusion among the nonempty norm-closed convex invariant subsets of a separable invariant set. Intersections of chains are nonempty in the actual weak topology. No weak continuity of the nonexpansive map is used: invariance passes to intersections pointwise.

theorem OAI.ReflexiveFixedPoints.nonempty_sInter_of_weaklyCompact_chain line 27

Source documentation

The weak compactness argument used for the lower bound of a chain.

theorem nonempty_sInter_of_weaklyCompact_chain
    {c : Set (Set X)} (hne : c.Nonempty) (hc : IsChain (· ⊆ ·) c)
    (hcompact : ∀ s ∈ c, WeaklyCompact s)
    (hclosed : ∀ s ∈ c, WeaklyClosed s)
    (hnonempty : ∀ s ∈ c, s.Nonempty) : (⋂₀ c).Nonempty := by
…

Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact, OAI.ReflexiveFixedPoints.WeaklyClosed

theorem OAI.ReflexiveFixedPoints.exists_minimalInvariantData_of_counterexample line 53

Source documentation

Restricting an actual fixed-point-free nonexpansive selfmap gives minimal invariant data in the same ambient space and the same norm.

theorem exists_minimalInvariantData_of_counterexample
    (hX : CanonicallyReflexive X) {C : Set X}
    (hne : C.Nonempty) (hclosed : IsClosed C)
    (hbounded : Bornology.IsBounded C) (hconvex : Convex ℝ C)
    (F : C → C) (hF : LipschitzWith 1 F) (hno : ∀ x : C, F x ≠ x) :
    ∃ D : MinimalInvariantData (X := X), D.K ⊆ C := by
…

Mentions: OAI.ReflexiveFixedPoints.CanonicallyReflexive, OAI.ReflexiveFixedPoints.MinimalInvariantData