OAI/Analysis/Nonexpansive/Diametral.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The Goebel–Karlovitz diameter lemma

The proof uses actual eventual-radius sublevel sets in place of numerical limsups. Their closedness, convexity, and invariance are proved below. Weak compactness supplies a cluster point in actual weakly closed norm balls.

  1. theorem OAI.ReflexiveFixedPoints.NormalizedMinimalData.image_hull_eq line 31

    Source documentation

    The image of a minimal invariant set has the whole set as its closed convex hull.

    theorem image_hull_eq (D : NormalizedMinimalData (X := X)) :
…

    Mentions: OAI.ReflexiveFixedPoints.NormalizedMinimalData

  2. def OAI.ReflexiveFixedPoints.NormalizedMinimalData.eventualRadius line 49
  3. theorem OAI.ReflexiveFixedPoints.NormalizedMinimalData.eventualRadius_closed line 53
  4. theorem OAI.ReflexiveFixedPoints.NormalizedMinimalData.eventualRadius_convex line 66
  5. theorem OAI.ReflexiveFixedPoints.NormalizedMinimalData.eventualRadius_invariant line 80
  6. theorem OAI.ReflexiveFixedPoints.NormalizedMinimalData.weak_closedBall line 96
  7. def OAI.ReflexiveFixedPoints.NormalizedMinimalData.centerSet line 102
  8. theorem OAI.ReflexiveFixedPoints.NormalizedMinimalData.centerSet_invariant line 105
  9. theorem OAI.ReflexiveFixedPoints.NormalizedMinimalData.one_le_radius_of_bounded_afps line 123
  10. theorem OAI.ReflexiveFixedPoints.NormalizedMinimalData.diametral line 175

    Source documentation

    Every approximate fixed point sequence is diametral at every point of the minimal set.

    theorem diametral (D : NormalizedMinimalData (X := X)) (u : ℕ → D.K)
…

    Mentions: OAI.ReflexiveFixedPoints.NormalizedMinimalData