OAI/Analysis/LipschitzEquivalence/MolecularApproximation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LipschitzCounterexample.FreeSpace.molecule line 13
  2. theorem OAI.LipschitzCounterexample.FreeSpace.norm_point_sub line 15
  3. theorem OAI.LipschitzCounterexample.FreeSpace.norm_molecule_le line 19
  4. theorem OAI.LipschitzCounterexample.FreeSpace.molecule_self line 25
  5. theorem OAI.LipschitzCounterexample.FreeSpace.supported_unitBall_subset_closure_convexHull_molecules line 27
  6. structure OAI.LipschitzCounterexample.FreeSpace.MolecularData line 61
  7. def OAI.LipschitzCounterexample.FreeSpace.MolecularData.vector line 69
  8. def OAI.LipschitzCounterexample.FreeSpace.MolecularData.cost line 70
  9. theorem OAI.LipschitzCounterexample.FreeSpace.MolecularData.cost_nonneg line 72
  10. theorem OAI.LipschitzCounterexample.FreeSpace.MolecularData.norm_vector_le_cost line 78
  11. theorem OAI.LipschitzCounterexample.FreeSpace.exists_molecular_approx line 85