OAI/Analysis/LipschitzFree/Coordinates.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Signed evaluation coefficients and finite-support projections

  1. def OAI.DiscreteFree.dualPairing line 17
  2. theorem OAI.DiscreteFree.dualPairing_apply line 20
  3. theorem OAI.DiscreteFree.dualPairing_delta line 21
  4. theorem OAI.DiscreteFree.dualPairing_bound line 23
  5. theorem OAI.DiscreteFree.Lip0.zero_apply line 27
  6. theorem OAI.DiscreteFree.Lip0.add_apply line 28
  7. theorem OAI.DiscreteFree.Lip0.smul_apply line 29
  8. def OAI.DiscreteFree.Lip0.center line 31
  9. theorem OAI.DiscreteFree.Lip0.center_apply line 35
  10. theorem OAI.DiscreteFree.Lip0.center_norm_le line 39
  11. theorem OAI.DiscreteFree.bounded_test_lipschitz line 50
  12. theorem OAI.DiscreteFree.sum_point_test line 61
  13. def OAI.DiscreteFree.indicator line 72
  14. theorem OAI.DiscreteFree.indicator_apply line 81
  15. def OAI.DiscreteFree.coordinate line 83
  16. theorem OAI.DiscreteFree.coordinate_delta line 85
  17. theorem OAI.DiscreteFree.coordinate_base line 87
  18. theorem OAI.DiscreteFree.sum_abs_coordinate_le line 92
  19. def OAI.DiscreteFree.supportProjection line 122
  20. theorem OAI.DiscreteFree.supportProjection_apply line 125
  21. theorem OAI.DiscreteFree.supportProjection_delta line 129
  22. theorem OAI.DiscreteFree.supportProjection_bound line 139