OAI/Geometry/LatticeCovering/CircuitErrors.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.SimplexYoung.affineCircuitVolumeSum_le_rational line 35
  2. lemma OAI.SingleLatticeCovering.SimplexYoung.affineCircuit_real_term line 41
  3. lemma OAI.SingleLatticeCovering.SimplexYoung.finite_circuitTerm_series_le line 56
  4. lemma OAI.SingleLatticeCovering.SimplexYoung.rank_two_source line 69
  5. theorem OAI.SingleLatticeCovering.SimplexYoung.continuum_circuit_error_source line 109
  6. theorem OAI.SingleLatticeCovering.ConvexGrid.eventually_primeGridVoid_source line 147
  7. instance OAI.SingleLatticeCovering.RogersPreparation.lattice_vadd_invariant line 199
  8. def OAI.SingleLatticeCovering.RogersPreparation.periodize line 205
  9. def OAI.SingleLatticeCovering.RogersPreparation.pointCount line 208
  10. def OAI.SingleLatticeCovering.RogersPreparation.cell line 211
  11. lemma OAI.SingleLatticeCovering.RogersPreparation.cell_fundamental line 214
  12. lemma OAI.SingleLatticeCovering.RogersPreparation.cell_measurable line 218
  13. lemma OAI.SingleLatticeCovering.RogersPreparation.cell_volume_ne_zero line 221
  14. lemma OAI.SingleLatticeCovering.RogersPreparation.cell_volume_ne_top line 224
  15. lemma OAI.SingleLatticeCovering.RogersPreparation.measurable_periodize line 227
  16. lemma OAI.SingleLatticeCovering.RogersPreparation.integral_periodize line 232
  17. def OAI.SingleLatticeCovering.RogersPreparation.translateLaw line 249
  18. instance OAI.SingleLatticeCovering.RogersPreparation.translateLaw_probability line 252
  19. lemma OAI.SingleLatticeCovering.RogersPreparation.integral_pointCount line 258
  20. lemma OAI.SingleLatticeCovering.RogersPreparation.pointCount_eq_zero line 268
  21. lemma OAI.SingleLatticeCovering.RogersPreparation.periodize_periodic line 301
  22. lemma OAI.SingleLatticeCovering.RogersPreparation.periodize_mul line 314
  23. lemma OAI.SingleLatticeCovering.RogersPreparation.integral_periodize_mul line 327
  24. lemma OAI.SingleLatticeCovering.RogersPreparation.pointCount_second_moment line 340
  25. lemma OAI.SingleLatticeCovering.RogersPreparation.finite_point_support line 362
  26. lemma OAI.SingleLatticeCovering.RogersPreparation.integral_periodic_shift line 386
  27. lemma OAI.SingleLatticeCovering.RogersPreparation.integral_torus_shift line 395
  28. lemma OAI.SingleLatticeCovering.RogersPreparation.translateLaw_preserving line 409
  29. lemma OAI.SingleLatticeCovering.RogersPreparation.hole_eq_zero_count_probability line 433
  30. def OAI.SingleLatticeCovering.PrimeKernel.tailForm line 462
  31. lemma OAI.SingleLatticeCovering.PrimeKernel.tailForm_update line 465
  32. lemma OAI.SingleLatticeCovering.PrimeKernel.tailForm_add line 472
  33. lemma OAI.SingleLatticeCovering.PrimeKernel.tailForm_smul line 475
  34. def OAI.SingleLatticeCovering.PrimeKernel.coordinates line 480
  35. def OAI.SingleLatticeCovering.PrimeKernel.basis line 517
  36. lemma OAI.SingleLatticeCovering.PrimeKernel.basis_repr line 520
  37. lemma OAI.SingleLatticeCovering.PrimeKernel.basis_apply line 525
  38. def OAI.SingleLatticeCovering.PrimeKernel.lattice line 538
  39. instance OAI.SingleLatticeCovering.PrimeKernel.lattice_discrete line 541
  40. instance OAI.SingleLatticeCovering.PrimeKernel.lattice_full line 544
  41. lemma OAI.SingleLatticeCovering.PrimeKernel.covolume_lattice line 548
  42. lemma OAI.SingleLatticeCovering.PrimeKernel.integer_mem_iff_dvd line 568
  43. lemma OAI.SingleLatticeCovering.PrimeKernel.exists_integer_of_mem line 595
  44. lemma OAI.SingleLatticeCovering.PrimeKernel.mem_lattice_iff line 613
  45. lemma OAI.SingleLatticeCovering.PrimeKernel.integer_mem_iff_congruence line 623