OAI/Geometry/CAT0Fillings/Reconstruction/AtomGraphs.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CAT0Fillings.SliceReconstruction.zeroChart_exists_supported_atom line 16
  2. theorem OAI.CAT0Fillings.SliceReconstruction.integerRectifiable_zero_distinct_representation line 26
  3. def OAI.CAT0Fillings.SliceReconstruction.atomicTent line 62
  4. lemma OAI.CAT0Fillings.SliceReconstruction.atomicTent_lipschitz line 66
  5. lemma OAI.CAT0Fillings.SliceReconstruction.atomicTent_unit_bound line 76
  6. lemma OAI.CAT0Fillings.SliceReconstruction.atomicTent_center line 84
  7. lemma OAI.CAT0Fillings.SliceReconstruction.atomicTent_near line 88
  8. lemma OAI.CAT0Fillings.SliceReconstruction.atomicTent_far line 93
  9. lemma OAI.CAT0Fillings.SliceReconstruction.matched_atom_distance_le line 98
  10. def OAI.CAT0Fillings.SliceReconstruction.UnitRepresentation line 151
  11. abbrev OAI.CAT0Fillings.SliceReconstruction.AtomCode line 155
  12. abbrev OAI.CAT0Fillings.SliceReconstruction.AtomCode.size line 157
  13. abbrev OAI.CAT0Fillings.SliceReconstruction.AtomCode.weights line 158
  14. abbrev OAI.CAT0Fillings.SliceReconstruction.AtomCode.centers line 159
  15. abbrev OAI.CAT0Fillings.SliceReconstruction.AtomCode.radius line 160
  16. def OAI.CAT0Fillings.SliceReconstruction.AtomCode.Valid line 162
  17. lemma OAI.CAT0Fillings.SliceReconstruction.atomCode_countable line 168
  18. lemma OAI.CAT0Fillings.SliceReconstruction.exists_separated_center_code line 171
  19. lemma OAI.CAT0Fillings.SliceReconstruction.unitRepresentation_matched_distance line 210
  20. def OAI.CAT0Fillings.SliceReconstruction.atomDomain line 263
  21. lemma OAI.CAT0Fillings.SliceReconstruction.atomDomain_subset line 270
  22. lemma OAI.CAT0Fillings.SliceReconstruction.isCompact_atomDomain line 275
  23. lemma OAI.CAT0Fillings.SliceReconstruction.integral_mem_atomDomain line 309
  24. def OAI.CAT0Fillings.SliceReconstruction.selectedAtom line 323
  25. lemma OAI.CAT0Fillings.SliceReconstruction.selectedAtom_spec line 328
  26. lemma OAI.CAT0Fillings.SliceReconstruction.selectedAtom_lipschitz line 334