OAI/Analysis/LipschitzFree/SignedTests.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Signed variation, scalar extension, and incidence averaging

  1. def OAI.DiscreteFree.Exceptional line 18
  2. theorem OAI.DiscreteFree.exceptional_unique line 21
  3. theorem OAI.DiscreteFree.exceptional_of_extensions line 26
  4. def OAI.DiscreteFree.totalVariation line 46
  5. def OAI.DiscreteFree.variationOn line 48
  6. def OAI.DiscreteFree.pairing line 52
  7. theorem OAI.DiscreteFree.pairing_error_le line 54
  8. theorem OAI.DiscreteFree.opposing_pairing_lower line 72
  9. theorem OAI.DiscreteFree.bounded_scalar_extension line 100
  10. theorem OAI.DiscreteFree.opposing_scalar_extension line 117
  11. theorem OAI.DiscreteFree.sum_variationOn_le line 174
  12. theorem OAI.DiscreteFree.variationOn_nonneg line 193
  13. theorem OAI.DiscreteFree.variationOn_le line 200
  14. theorem OAI.DiscreteFree.signed_incidence_obstruction line 207