OAI/Geometry/LatticeCovering/Completion.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.Completion.projection_mem_image_iff line 12
  2. lemma OAI.SingleLatticeCovering.Completion.projection_image_eq_univ line 25
  3. lemma OAI.SingleLatticeCovering.Completion.projection_scalar_image line 42
  4. theorem OAI.SingleLatticeCovering.Completion.completion_with_projection line 55
  5. theorem OAI.SingleLatticeCovering.Completion.complete_almost_cover_projection line 84
  6. lemma OAI.SingleLatticeCovering.Shear.source_pattern_mono line 118
  7. lemma OAI.SingleLatticeCovering.Shear.retained_load line 128
  8. lemma OAI.SingleLatticeCovering.Shear.retain_source_pattern line 142
  9. lemma OAI.SingleLatticeCovering.Shear.finite_weight_load_bounds line 163
  10. lemma OAI.SingleLatticeCovering.Shear.exponential_pattern_bound line 178
  11. def OAI.SingleLatticeCovering.Vertical.labelPattern line 206
  12. lemma OAI.SingleLatticeCovering.Vertical.mem_labelPattern line 212
  13. lemma OAI.SingleLatticeCovering.Vertical.labelPattern_source line 218
  14. lemma OAI.SingleLatticeCovering.Vertical.sum_labelPattern line 231
  15. lemma OAI.SingleLatticeCovering.Vertical.labelPattern_card line 239
  16. lemma OAI.SingleLatticeCovering.Vertical.suffix_card_le line 246
  17. lemma OAI.SingleLatticeCovering.Vertical.labelPattern_mem_all line 256
  18. lemma OAI.SingleLatticeCovering.Vertical.retained_mem_all line 268
  19. theorem OAI.SingleLatticeCovering.Vertical.section_labeled_retained line 287
  20. def OAI.SingleLatticeCovering.CoverGeometry.columnMap line 351
  21. lemma OAI.SingleLatticeCovering.CoverGeometry.columnMap_apply line 357
  22. abbrev OAI.SingleLatticeCovering.CoverGeometry.joinedLattice line 360
  23. lemma OAI.SingleLatticeCovering.CoverGeometry.joined_point_mem line 365
  24. lemma OAI.SingleLatticeCovering.CoverGeometry.joined_covolume line 375
  25. def OAI.SingleLatticeCovering.CoverGeometry.horizontalHole line 385
  26. lemma OAI.SingleLatticeCovering.CoverGeometry.covered_of_section line 393
  27. lemma OAI.SingleLatticeCovering.CoverGeometry.horizontal_hole_subset line 414
  28. instance OAI.SingleLatticeCovering.CoverGeometry.torusMeasure_neg line 441
  29. theorem OAI.SingleLatticeCovering.CoverGeometry.finite_family_lattice_shear line 447
  30. lemma OAI.SingleLatticeCovering.CoverGeometry.add_lattice_cover_iff line 513
  31. lemma OAI.SingleLatticeCovering.CoverGeometry.horizontalHole_reduce line 528
  32. theorem OAI.SingleLatticeCovering.CoverGeometry.all_height_hole_bound line 553
  33. def OAI.SingleLatticeCovering.CoverGeometry.appendTorus line 587
  34. lemma OAI.SingleLatticeCovering.CoverGeometry.appendTorus_surjective line 600
  35. lemma OAI.SingleLatticeCovering.CoverGeometry.appendTorus_measurePreserving line 603
  36. def OAI.SingleLatticeCovering.CoverGeometry.productProjection line 613
  37. lemma OAI.SingleLatticeCovering.CoverGeometry.productProjection_apply line 643
  38. lemma OAI.SingleLatticeCovering.CoverGeometry.productProjection_append line 650
  39. lemma OAI.SingleLatticeCovering.CoverGeometry.productProjection_surjective line 658
  40. lemma OAI.SingleLatticeCovering.CoverGeometry.productProjection_eq_zero_iff line 669
  41. def OAI.SingleLatticeCovering.CoverGeometry.joinedProjection line 685
  42. lemma OAI.SingleLatticeCovering.CoverGeometry.joinedProjection_surjective line 694
  43. lemma OAI.SingleLatticeCovering.CoverGeometry.joinedProjection_eq_zero_iff line 701
  44. lemma OAI.SingleLatticeCovering.CoverGeometry.joinedProjection_append line 708