OAI/Geometry/LatticeCovering/CircuitSums.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SingleLatticeCovering.CircuitGridSum.eventually_sum_normalized_circuits_le line 30
  2. lemma OAI.SingleLatticeCovering.PrimitiveCircuit.integer_relation_of_rat_dependence line 94
  3. lemma OAI.SingleLatticeCovering.PrimitiveCircuit.primitive_normalize line 119
  4. lemma OAI.SingleLatticeCovering.PrimitiveCircuit.coefficients_nonzero_of_delete_independent line 144
  5. theorem OAI.SingleLatticeCovering.PrimitiveCircuit.exists_primitive_circuit_relation line 169
  6. lemma OAI.SingleLatticeCovering.RogersPreparation.int_det_abs_le line 186
  7. lemma OAI.SingleLatticeCovering.RogersPreparation.intCast_eq_zero_small line 191
  8. lemma OAI.SingleLatticeCovering.RogersPreparation.det_mod_eq_zero_small line 200
  9. lemma OAI.SingleLatticeCovering.RogersPreparation.det_mod_ne_zero_small line 209
  10. lemma OAI.SingleLatticeCovering.RogersPreparation.exists_column_minor line 224
  11. lemma OAI.SingleLatticeCovering.RogersPreparation.rowIndependent_of_column_minor line 244
  12. lemma OAI.SingleLatticeCovering.RogersPreparation.rowIndependent_iff_column_minor line 250
  13. lemma OAI.SingleLatticeCovering.RogersPreparation.rowIndependent_mod_iff_rat line 257
  14. def OAI.SingleLatticeCovering.AffineCircuit.integerRows line 279
  15. def OAI.SingleLatticeCovering.AffineCircuit.IsCircuit line 283
  16. lemma OAI.SingleLatticeCovering.AffineCircuit.rowIndependent_real_iff_rat line 288
  17. lemma OAI.SingleLatticeCovering.AffineCircuit.IsCircuit.real_delete line 297
  18. lemma OAI.SingleLatticeCovering.AffineCircuit.IsCircuit.primitive_relation line 305
  19. def OAI.SingleLatticeCovering.AffineCircuit.circuits line 316
  20. lemma OAI.SingleLatticeCovering.AffineCircuit.mem_circuits line 320
  21. def OAI.SingleLatticeCovering.AffineCircuit.coefficientCircuits line 325
  22. lemma OAI.SingleLatticeCovering.AffineCircuit.mem_coefficientCircuits line 330
  23. lemma OAI.SingleLatticeCovering.AffineCircuit.circuits_covered line 337
  24. def OAI.SingleLatticeCovering.CircuitEnumeration.Enumerations line 357
  25. instance OAI.SingleLatticeCovering.CircuitEnumeration.(instance at line 360) line 360
  26. lemma OAI.SingleLatticeCovering.CircuitEnumeration.card_enumerations line 364
  27. def OAI.SingleLatticeCovering.CircuitEnumeration.orderedCircuit line 376
  28. lemma OAI.SingleLatticeCovering.CircuitEnumeration.orderedCircuit_injective line 380
  29. theorem OAI.SingleLatticeCovering.CircuitEnumeration.factorial_count_le line 409
  30. theorem OAI.SingleLatticeCovering.CircuitEnumeration.card_mul_le_tsum_cover line 422
  31. theorem OAI.SingleLatticeCovering.CircuitEnumeration.factorial_weight_le_tsum line 443
  32. lemma OAI.SingleLatticeCovering.AffineCircuit.coefficient_counts_summable line 466
  33. theorem OAI.SingleLatticeCovering.AffineCircuit.eventually_circuit_count_le line 487
  34. theorem OAI.SingleLatticeCovering.CircuitEnumeration.factorial_count_le_map line 515
  35. def OAI.SingleLatticeCovering.BrokenCircuit.Active line 542
  36. def OAI.SingleLatticeCovering.BrokenCircuit.NoBrokenCircuit line 545
  37. lemma OAI.SingleLatticeCovering.BrokenCircuit.active_mono line 548
  38. lemma OAI.SingleLatticeCovering.BrokenCircuit.NoBrokenCircuit.mono line 556
  39. lemma OAI.SingleLatticeCovering.BrokenCircuit.NoBrokenCircuit.linearIndepOn line 562
  40. lemma OAI.SingleLatticeCovering.BrokenCircuit.active_zero line 581
  41. lemma OAI.SingleLatticeCovering.BrokenCircuit.nbc_insert_least_zero line 591
  42. theorem OAI.SingleLatticeCovering.BrokenCircuit.cone_partial_sum line 620
  43. def OAI.SingleLatticeCovering.BrokenCircuit.zeroFamily line 675
  44. def OAI.SingleLatticeCovering.BrokenCircuit.nbcFaces line 679
  45. def OAI.SingleLatticeCovering.BrokenCircuit.nbcValue line 683
  46. def OAI.SingleLatticeCovering.BrokenCircuit.avoidanceIndicator line 686
  47. lemma OAI.SingleLatticeCovering.BrokenCircuit.mem_zeroFamily line 690
  48. lemma OAI.SingleLatticeCovering.BrokenCircuit.mem_nbcFaces line 695
  49. theorem OAI.SingleLatticeCovering.BrokenCircuit.nbc_alternating_bound line 702
  50. lemma OAI.SingleLatticeCovering.BrokenCircuit.nbc_even_bound line 754
  51. lemma OAI.SingleLatticeCovering.BrokenCircuit.nbc_odd_bound line 760
  52. lemma OAI.SingleLatticeCovering.BrokenCircuit.mulVec_surjective_of_rowIndependent line 775
  53. lemma OAI.SingleLatticeCovering.BrokenCircuit.card_fiber_mul_card_of_surjective line 797
  54. lemma OAI.SingleLatticeCovering.BrokenCircuit.fiber_ratio_of_surjective line 809
  55. def OAI.SingleLatticeCovering.BrokenCircuit.vectorAverage line 828
  56. lemma OAI.SingleLatticeCovering.BrokenCircuit.independent_joint_probability line 831
  57. lemma OAI.SingleLatticeCovering.BrokenCircuit.vectorAverage_mono line 859
  58. lemma OAI.SingleLatticeCovering.BrokenCircuit.vectorAverage_sum line 865
  59. lemma OAI.SingleLatticeCovering.BrokenCircuit.vectorAverage_const_mul line 870
  60. lemma OAI.SingleLatticeCovering.BrokenCircuit.vectorAverage_zero line 876
  61. lemma OAI.SingleLatticeCovering.BrokenCircuit.nbcFaces_zero_eq line 879
  62. lemma OAI.SingleLatticeCovering.BrokenCircuit.nbcValue_eq line 891
  63. def OAI.SingleLatticeCovering.BrokenCircuit.nbcPolynomial line 897
  64. lemma OAI.SingleLatticeCovering.BrokenCircuit.average_nbcValue line 903
  65. theorem OAI.SingleLatticeCovering.BrokenCircuit.average_avoidance_even_le line 926
  66. theorem OAI.SingleLatticeCovering.BrokenCircuit.average_avoidance_odd_ge line 932