OAI/Geometry/LatticeCovering/BrokenCircuits.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleLatticeCovering.BrokenCircuit.minimalObstructions line 32
  2. lemma OAI.SingleLatticeCovering.BrokenCircuit.mem_minimalObstructions line 36
  3. lemma OAI.SingleLatticeCovering.BrokenCircuit.exists_minimalObstruction line 41
  4. lemma OAI.SingleLatticeCovering.BrokenCircuit.sum_powerset_pow_card line 52
  5. lemma OAI.SingleLatticeCovering.BrokenCircuit.sum_supersets_pow_card line 58
  6. theorem OAI.SingleLatticeCovering.BrokenCircuit.bad_subset_sum_le line 96
  7. def OAI.SingleLatticeCovering.BrokenCircuit.truncatedFacesPolynomial line 138
  8. def OAI.SingleLatticeCovering.BrokenCircuit.binomialPolynomial line 141
  9. lemma OAI.SingleLatticeCovering.BrokenCircuit.unrestricted_polynomial_eq line 144
  10. lemma OAI.SingleLatticeCovering.BrokenCircuit.truncated_defect_le_bad_sum line 175
  11. theorem OAI.SingleLatticeCovering.BrokenCircuit.truncated_defect_le line 196
  12. lemma OAI.SingleLatticeCovering.BrokenCircuit.minimalObstruction_linearIndepOn line 214
  13. theorem OAI.SingleLatticeCovering.BrokenCircuit.minimalObstruction_has_circuit line 231
  14. def OAI.SingleLatticeCovering.BrokenCircuit.finiteCircuitError line 282
  15. lemma OAI.SingleLatticeCovering.BrokenCircuit.nbcPolynomial_defect_bound line 287
  16. theorem OAI.SingleLatticeCovering.BrokenCircuit.finite_field_void_upper line 298
  17. theorem OAI.SingleLatticeCovering.BrokenCircuit.finite_field_void_lower line 306
  18. theorem OAI.SingleLatticeCovering.BrokenCircuit.minimalObstruction_circuit line 326
  19. theorem OAI.SingleLatticeCovering.BrokenCircuit.enumerated_circuit line 368
  20. def OAI.SingleLatticeCovering.PrimeCircuit.homogeneousRow line 431
  21. lemma OAI.SingleLatticeCovering.PrimeCircuit.integerRows_bound line 434
  22. lemma OAI.SingleLatticeCovering.PrimeCircuit.mapped_integerRows line 441
  23. theorem OAI.SingleLatticeCovering.PrimeCircuit.obstruction_factorial_count line 448
  24. lemma OAI.SingleLatticeCovering.BrokenCircuit.minimalObstruction_two_le line 494
  25. lemma OAI.SingleLatticeCovering.PrimeCircuit.homogeneousRow_injective line 519
  26. lemma OAI.SingleLatticeCovering.PrimeCircuit.obstruction_two_le line 536
  27. lemma OAI.SingleLatticeCovering.PrimeCircuit.sum_pow_card_eq line 552
  28. theorem OAI.SingleLatticeCovering.PrimeCircuit.finiteCircuitError_le line 568
  29. def OAI.SingleLatticeCovering.ConvexGrid.scaledIntegerPoint line 617
  30. def OAI.SingleLatticeCovering.ConvexGrid.gridSet line 619
  31. lemma OAI.SingleLatticeCovering.ConvexGrid.scaledPoint_injective line 622
  32. lemma OAI.SingleLatticeCovering.ConvexGrid.integerPoint_mem_lattice line 629
  33. lemma OAI.SingleLatticeCovering.ConvexGrid.gridSet_finite line 635
  34. def OAI.SingleLatticeCovering.ConvexGrid.integerGrid line 645
  35. lemma OAI.SingleLatticeCovering.ConvexGrid.mem_integerGrid line 649
  36. lemma OAI.SingleLatticeCovering.ConvexGrid.card_integerGrid line 655
  37. theorem OAI.SingleLatticeCovering.ConvexGrid.normalized_card_limit line 681
  38. lemma OAI.SingleLatticeCovering.ConvexGrid.grid_uniform_bound line 690