OAI/Geometry/LatticeCovering/Patterns.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.Vertical.rationalAlphabet_log_card line 43
  2. lemma OAI.SingleLatticeCovering.Vertical.Chain.every_and line 60
  3. lemma OAI.SingleLatticeCovering.Vertical.Chain.denominator_log_le line 66
  4. lemma OAI.SingleLatticeCovering.Vertical.Chain.full_denominator_log_le line 77
  5. lemma OAI.SingleLatticeCovering.Vertical.Chain.alphabet_log_card line 85
  6. lemma OAI.SingleLatticeCovering.Vertical.Chain.regular_primes_log_bound line 113
  7. theorem OAI.SingleLatticeCovering.Vertical.vertical_patterns_alphabets line 135
  8. def OAI.SingleLatticeCovering.Shear.translate line 283
  9. lemma OAI.SingleLatticeCovering.Shear.measurableSet_translate line 285
  10. lemma OAI.SingleLatticeCovering.Shear.measure_translate line 288
  11. lemma OAI.SingleLatticeCovering.Shear.translate_add line 291
  12. lemma OAI.SingleLatticeCovering.Shear.translate_inter line 297
  13. lemma OAI.SingleLatticeCovering.Shear.overlap_common_translate line 300
  14. lemma OAI.SingleLatticeCovering.Shear.measurable_overlap line 304
  15. lemma OAI.SingleLatticeCovering.Shear.lintegral_overlap line 311
  16. lemma OAI.SingleLatticeCovering.Shear.simultaneous_choice line 331
  17. inductive OAI.SingleLatticeCovering.Shear.Pattern line 377
  18. def OAI.SingleLatticeCovering.Shear.Pattern.size line 385
  19. lemma OAI.SingleLatticeCovering.Shear.Pattern.size_pos line 390
  20. lemma OAI.SingleLatticeCovering.Shear.Pattern.size_le_two_pow line 396
  21. def OAI.SingleLatticeCovering.Shear.Pattern.weight line 405
  22. def OAI.SingleLatticeCovering.Shear.Pattern.labelProduct line 410
  23. lemma OAI.SingleLatticeCovering.Shear.Pattern.weight_eq line 415
  24. lemma OAI.SingleLatticeCovering.Shear.Pattern.weight_ne_zero line 428
  25. lemma OAI.SingleLatticeCovering.Shear.Pattern.weight_ne_top line 435
  26. def OAI.SingleLatticeCovering.Shear.Pattern.first line 442
  27. def OAI.SingleLatticeCovering.Shear.Pattern.second line 446
  28. def OAI.SingleLatticeCovering.Shear.Pattern.branches line 450
  29. def OAI.SingleLatticeCovering.Shear.Pattern.failure line 457
  30. lemma OAI.SingleLatticeCovering.Shear.Pattern.measurableSet_failure line 464
  31. def OAI.SingleLatticeCovering.Shear.restrictColumns line 478
  32. lemma OAI.SingleLatticeCovering.Shear.restrictColumns_snoc line 481
  33. lemma OAI.SingleLatticeCovering.Shear.restrictColumns_self line 486
  34. def OAI.SingleLatticeCovering.Shear.SliceClosed line 489
  35. theorem OAI.SingleLatticeCovering.Shear.simultaneous_shear_aux line 507
  36. theorem OAI.SingleLatticeCovering.Shear.simultaneous_shear line 569
  37. def OAI.SingleLatticeCovering.Shear.Pattern.appendPoint line 590
  38. lemma OAI.SingleLatticeCovering.Shear.Pattern.appendPoint_injective line 593
  39. lemma OAI.SingleLatticeCovering.Shear.Pattern.appendPoint_disjoint line 600
  40. def OAI.SingleLatticeCovering.Shear.Pattern.points line 612
  41. lemma OAI.SingleLatticeCovering.Shear.Pattern.points_card line 619
  42. lemma OAI.SingleLatticeCovering.Shear.Pattern.points_nonempty line 629
  43. lemma OAI.SingleLatticeCovering.Shear.Pattern.labelProduct_eq_prod line 633
  44. def OAI.SingleLatticeCovering.Shear.Pattern.linearShift line 650
  45. lemma OAI.SingleLatticeCovering.Shear.Pattern.linearShift_snoc line 652
  46. lemma OAI.SingleLatticeCovering.Shear.Pattern.mem_failure_iff line 658
  47. lemma OAI.SingleLatticeCovering.Shear.Pattern.failure_eq_intersection line 680