OAI/Analysis/Nonexpansive/TerminalSequence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

One common terminal sequence for all fixed generated maps

The terminal sequence uses zero-based indices. All quantitative estimates retain the denominator j+1. The sequence is constructed once. Every fixed finite family of generated maps has total displacement tending to zero along this same sequence.

  1. def OAI.ReflexiveFixedPoints.terminalSequence line 29
  2. theorem OAI.ReflexiveFixedPoints.terminalSequence_defect_le line 33
  3. theorem OAI.ReflexiveFixedPoints.terminalSequence_defect_tendsto line 42
  4. theorem OAI.ReflexiveFixedPoints.terminalSequence_displacement_le line 52
  5. theorem OAI.ReflexiveFixedPoints.terminalSequence_generated_displacement line 67
  6. theorem OAI.ReflexiveFixedPoints.terminalSequence_generated_displacement_tendsto line 79
  7. theorem OAI.ReflexiveFixedPoints.terminalSequence_finite_displacement_tendsto line 95
  8. theorem OAI.ReflexiveFixedPoints.terminalSequence_eventually_finite_displacement_lt line 108
  9. theorem OAI.ReflexiveFixedPoints.terminalSequence_exists_common_index line 121