OAI/Analysis/Nonexpansive/Resolvents.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Resolvents of an actual nonexpansive selfmap

The affine contraction is constructed on the norm-metric subtype of the closed convex set. Its fixed point is supplied by the Banach contraction theorem. The resulting resolvents are nonexpansive in their anchor, have the exact displacement coefficient n - 1, and have defect at most 1/n when all distances in the set are at most one.

  1. def OAI.ReflexiveFixedPoints.ResolventConstruction.step line 31
  2. theorem OAI.ReflexiveFixedPoints.ResolventConstruction.step_contracting line 36
  3. def OAI.ReflexiveFixedPoints.ResolventConstruction.atWeight line 58
  4. theorem OAI.ReflexiveFixedPoints.ResolventConstruction.atWeight_equation line 66
  5. theorem OAI.ReflexiveFixedPoints.ResolventConstruction.atWeight_unique line 77
  6. theorem OAI.ReflexiveFixedPoints.ResolventConstruction.atWeight_nonexpansive line 88
  7. theorem OAI.ReflexiveFixedPoints.ResolventConstruction.atWeight_defect_le line 127
  8. theorem OAI.ReflexiveFixedPoints.ResolventConstruction.atWeight_displacement_le line 145
  9. theorem OAI.ReflexiveFixedPoints.ResolventConstruction.weight_pos line 178
  10. theorem OAI.ReflexiveFixedPoints.ResolventConstruction.weight_le_one line 182
  11. def OAI.ReflexiveFixedPoints.resolvent line 190
  12. theorem OAI.ReflexiveFixedPoints.resolvent_equation line 195
  13. theorem OAI.ReflexiveFixedPoints.resolvent_unique line 202
  14. theorem OAI.ReflexiveFixedPoints.resolvent_one line 208
  15. theorem OAI.ReflexiveFixedPoints.resolvent_nonexpansive line 215
  16. theorem OAI.ReflexiveFixedPoints.resolvent_defect_le line 220
  17. theorem OAI.ReflexiveFixedPoints.resolvent_displacement_le line 231