OAI/Analysis/C0Absorption/Triangular.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.absorptionMap line 19
  2. theorem OAI.C0Absorption.absorption_onto line 22
  3. theorem OAI.C0Absorption.absorption_upper line 35
  4. theorem OAI.C0Absorption.absorption_inverse_bound line 60
  5. theorem OAI.C0Absorption.normalize_norm_le_one line 109
  6. theorem OAI.C0Absorption.normalization_bound line 114
  7. def OAI.C0Absorption.normalizedBall line 134
  8. def OAI.C0Absorption.zeroBall line 137
  9. theorem OAI.C0Absorption.normalizedBall_zero line 139
  10. def OAI.C0Absorption.radialLift line 143
  11. theorem OAI.C0Absorption.radialLift_zero line 146
  12. theorem OAI.C0Absorption.norm_pointMap_le_one line 149
  13. theorem OAI.C0Absorption.radialLift_lipschitz line 159
  14. theorem OAI.C0Absorption.radialLift_homogeneous line 188