OAI/Geometry/LatticeCovering/Shears.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleLatticeCovering.Shear.Pattern.slice line 16
  2. lemma OAI.SingleLatticeCovering.Shear.Pattern.mem_slice line 21
  3. lemma OAI.SingleLatticeCovering.Shear.Pattern.slice_image line 35
  4. lemma OAI.SingleLatticeCovering.Shear.Pattern.slice_union line 50
  5. lemma OAI.SingleLatticeCovering.Shear.Pattern.slice_mono line 56
  6. lemma OAI.SingleLatticeCovering.Shear.Pattern.slice_split_left line 60
  7. lemma OAI.SingleLatticeCovering.Shear.Pattern.slice_split_right line 64
  8. lemma OAI.SingleLatticeCovering.Shear.Pattern.height_mono line 68
  9. lemma OAI.SingleLatticeCovering.Shear.Pattern.height_split line 74
  10. lemma OAI.SingleLatticeCovering.Shear.Pattern.mono_base_unique line 81
  11. lemma OAI.SingleLatticeCovering.Shear.Pattern.mono_ne_split line 87
  12. lemma OAI.SingleLatticeCovering.Shear.Pattern.split_base_unique line 101
  13. lemma OAI.SingleLatticeCovering.Shear.Pattern.points_injective line 118
  14. def OAI.SingleLatticeCovering.Shear.UniqueLabels line 161
  15. def OAI.SingleLatticeCovering.Shear.SuffixBinary line 167
  16. def OAI.SingleLatticeCovering.Shear.SourcePattern line 171
  17. lemma OAI.SingleLatticeCovering.Shear.Pattern.UniqueLabels_slice line 175
  18. lemma OAI.SingleLatticeCovering.Shear.Pattern.SuffixBinary_slice line 181
  19. lemma OAI.SingleLatticeCovering.Shear.Pattern.suffix_last_bound line 198
  20. lemma OAI.SingleLatticeCovering.Shear.Pattern.slice_partition line 206
  21. lemma OAI.SingleLatticeCovering.Shear.Pattern.exists_tree line 229
  22. def OAI.SingleLatticeCovering.Shear.encodeFamily line 276
  23. lemma OAI.SingleLatticeCovering.Shear.mem_encodeFamily line 280
  24. lemma OAI.SingleLatticeCovering.Shear.encodeFamily_card_le line 284
  25. def OAI.SingleLatticeCovering.Shear.SourceSliceClosed line 291
  26. lemma OAI.SingleLatticeCovering.Shear.encodeFamily_sliceClosed line 294
  27. theorem OAI.SingleLatticeCovering.Shear.source_simultaneous_shear line 324
  28. lemma OAI.SingleLatticeCovering.Shear.source_card_le_two_pow line 353
  29. lemma OAI.SingleLatticeCovering.Shear.small_subsets_card line 361
  30. def OAI.SingleLatticeCovering.Shear.alphabetPoints line 404
  31. lemma OAI.SingleLatticeCovering.Shear.mem_alphabetPoints line 408
  32. def OAI.SingleLatticeCovering.Shear.allPatterns line 413
  33. lemma OAI.SingleLatticeCovering.Shear.mem_allPatterns line 418
  34. lemma OAI.SingleLatticeCovering.Shear.allPatterns_sliceClosed line 424
  35. lemma OAI.SingleLatticeCovering.Shear.allPatterns_card_bound line 438
  36. lemma OAI.SingleLatticeCovering.Shear.allPatterns_total_bound line 447
  37. lemma OAI.SingleLatticeCovering.Completion.add_eq_univ_of_measure_sum line 482
  38. lemma OAI.SingleLatticeCovering.Completion.preimage_image_eq_kernel_union line 502
  39. lemma OAI.SingleLatticeCovering.Completion.measure_image_le_kernel line 515
  40. lemma OAI.SingleLatticeCovering.Completion.measureReal_image_le_kernel line 524
  41. abbrev OAI.SingleLatticeCovering.Completion.Torus line 533
  42. def OAI.SingleLatticeCovering.Completion.torusMeasure line 535
  43. instance OAI.SingleLatticeCovering.Completion.torusMeasure_haar line 537
  44. instance OAI.SingleLatticeCovering.Completion.torusMeasure_probability line 540
  45. lemma OAI.SingleLatticeCovering.Completion.real_nsmul_regular line 543
  46. lemma OAI.SingleLatticeCovering.Completion.circle_torsion_card line 548
  47. lemma OAI.SingleLatticeCovering.Completion.torus_torsion_card line 557
  48. lemma OAI.SingleLatticeCovering.Completion.torus_measure_image_nsmul line 576
  49. abbrev OAI.SingleLatticeCovering.Completion.RealSpace line 600
  50. def OAI.SingleLatticeCovering.Completion.latticeBasis line 602
  51. def OAI.SingleLatticeCovering.Completion.latticeProjection line 608
  52. lemma OAI.SingleLatticeCovering.Completion.latticeProjection_surjective line 619
  53. lemma OAI.SingleLatticeCovering.Completion.latticeProjection_eq_zero_iff line 632
  54. lemma OAI.SingleLatticeCovering.Completion.latticeProjection_image_eq_univ_iff line 654
  55. def OAI.SingleLatticeCovering.Completion.holeProportion line 677
  56. lemma OAI.SingleLatticeCovering.Completion.projection_dilate_nsmul line 681
  57. theorem OAI.SingleLatticeCovering.Completion.completion line 697
  58. def OAI.SingleLatticeCovering.Completion.contractLattice line 724
  59. instance OAI.SingleLatticeCovering.Completion.contractLattice_discrete line 728
  60. instance OAI.SingleLatticeCovering.Completion.contractLattice_fullSpan line 734
  61. lemma OAI.SingleLatticeCovering.Completion.mem_contractLattice line 741
  62. lemma OAI.SingleLatticeCovering.Completion.contractLattice_covolume line 745
  63. lemma OAI.SingleLatticeCovering.Completion.cover_contractLattice line 763
  64. lemma OAI.SingleLatticeCovering.Completion.one_add_inv_pow_le_exp line 778
  65. lemma OAI.SingleLatticeCovering.Completion.small_hole_strict line 786
  66. theorem OAI.SingleLatticeCovering.Completion.complete_almost_cover line 805