OAI/Geometry/LatticeCovering/CircuitLattices.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SingleLatticeCovering.CircuitArithmetic.integerLattice line 24
  2. def OAI.SingleLatticeCovering.CircuitArithmetic.integerCoordinates line 27
  3. lemma OAI.SingleLatticeCovering.CircuitArithmetic.integerCoordinates_cast line 30
  4. lemma OAI.SingleLatticeCovering.CircuitArithmetic.integerLattice_covolume line 35
  5. def OAI.SingleLatticeCovering.CircuitArithmetic.congruenceKernel line 42
  6. lemma OAI.SingleLatticeCovering.CircuitArithmetic.congruenceKernel_le line 45
  7. instance OAI.SingleLatticeCovering.CircuitArithmetic.congruenceKernel_discrete line 50
  8. lemma OAI.SingleLatticeCovering.CircuitArithmetic.mem_congruenceKernel_iff line 55
  9. instance OAI.SingleLatticeCovering.CircuitArithmetic.congruenceKernel_full line 66
  10. lemma OAI.SingleLatticeCovering.CircuitArithmetic.congruenceKernel_relIndex line 86
  11. theorem OAI.SingleLatticeCovering.CircuitArithmetic.congruenceKernel_covolume line 99
  12. def OAI.SingleLatticeCovering.CircuitArithmetic.relationForm line 114
  13. lemma OAI.SingleLatticeCovering.CircuitArithmetic.relationForm_surjective line 125
  14. lemma OAI.SingleLatticeCovering.CircuitArithmetic.primitive_relation_surjective line 139
  15. lemma OAI.SingleLatticeCovering.CircuitArithmetic.primitive_relation_covolume line 152
  16. lemma OAI.SingleLatticeCovering.CircuitGrid.exists_column_basis line 167
  17. lemma OAI.SingleLatticeCovering.CircuitGrid.count_of_spanning_columns line 181
  18. theorem OAI.SingleLatticeCovering.CircuitGrid.array_count_of_spanning_columns line 200
  19. lemma OAI.SingleLatticeCovering.CircuitGrid.mulVec_surjective_of_rowIndependent line 232
  20. def OAI.SingleLatticeCovering.CircuitGrid.affineRows line 257
  21. lemma OAI.SingleLatticeCovering.CircuitGrid.span_affine_columns line 260
  22. lemma OAI.SingleLatticeCovering.CircuitGrid.integer_array_count line 266
  23. theorem OAI.SingleLatticeCovering.CircuitGrid.integer_affine_grid_count line 294
  24. lemma OAI.SingleLatticeCovering.CircuitGrid.relation_zero_mod line 323
  25. lemma OAI.SingleLatticeCovering.CircuitGrid.projected_relation_mem line 332
  26. theorem OAI.SingleLatticeCovering.CircuitGrid.full_circuit_grid_bound line 348
  27. lemma OAI.SingleLatticeCovering.CircuitGrid.gcd_permute line 404
  28. theorem OAI.SingleLatticeCovering.CircuitGrid.full_circuit_grid_bound_at line 412
  29. lemma OAI.SingleLatticeCovering.CircuitWeight.tsum_int_inv_sq_le_four line 453
  30. lemma OAI.SingleLatticeCovering.CircuitWeight.int_circuit_weight_le_sq line 466
  31. lemma OAI.SingleLatticeCovering.CircuitWeight.tsum_ennreal_int_circuit_weight_le line 475
  32. lemma OAI.SingleLatticeCovering.CircuitWeight.tsum_ennreal_fin_prod line 485
  33. theorem OAI.SingleLatticeCovering.CircuitWeight.tsum_integerCircuitWeight_le line 498
  34. lemma OAI.SingleLatticeCovering.CircuitWeight.height_weight_le line 507
  35. lemma OAI.SingleLatticeCovering.CircuitWeight.summable_circuit_weight line 524
  36. theorem OAI.SingleLatticeCovering.CircuitGrid.normalized_circuit_grid_domination line 544
  37. theorem OAI.SingleLatticeCovering.CircuitLimit.eventually_tsum_le_of_dominated_comparison line 588