OAI/Geometry/LatticeCovering/Concentration.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.Folded.law_real_of_subset line 17
  2. def OAI.SingleLatticeCovering.Folded.centralInterval line 31
  3. lemma OAI.SingleLatticeCovering.Folded.centralInterval_subset line 33
  4. lemma OAI.SingleLatticeCovering.Folded.centralInterval_volume line 40
  5. lemma OAI.SingleLatticeCovering.Folded.centralInterval_probability line 50
  6. def OAI.SingleLatticeCovering.Folded.cubeLaw line 73
  7. lemma OAI.SingleLatticeCovering.Folded.log_folded line 75
  8. lemma OAI.SingleLatticeCovering.Folded.folded_chebyshev line 79
  9. lemma OAI.SingleLatticeCovering.Folded.central_count_tail line 89
  10. lemma OAI.SingleLatticeCovering.pi_withDensity_ofReal line 117
  11. def OAI.SingleLatticeCovering.Folded.cube line 141
  12. lemma OAI.SingleLatticeCovering.Folded.continuous_folded line 143
  13. lemma OAI.SingleLatticeCovering.Folded.cubeLaw_density line 147
  14. lemma OAI.SingleLatticeCovering.Folded.cube_integral line 159
  15. lemma OAI.SingleLatticeCovering.Folded.cubeLaw_real line 167
  16. lemma OAI.SingleLatticeCovering.Folded.cubeLaw_isProbability line 179
  17. lemma OAI.SingleLatticeCovering.Folded.continuous_good_mass line 185
  18. def OAI.SingleLatticeCovering.ConstructionA.generator line 231
  19. def OAI.SingleLatticeCovering.ConstructionA.matrix line 233
  20. lemma OAI.SingleLatticeCovering.ConstructionA.det_matrix line 236
  21. lemma OAI.SingleLatticeCovering.ConstructionA.independent_matrix line 244
  22. def OAI.SingleLatticeCovering.ConstructionA.basis line 252
  23. lemma OAI.SingleLatticeCovering.ConstructionA.basis_apply line 259
  24. lemma OAI.SingleLatticeCovering.ConstructionA.basis_pivot line 264
  25. lemma OAI.SingleLatticeCovering.ConstructionA.basis_other line 269
  26. def OAI.SingleLatticeCovering.ConstructionA.lattice line 277
  27. instance OAI.SingleLatticeCovering.ConstructionA.lattice_discrete line 280
  28. instance OAI.SingleLatticeCovering.ConstructionA.lattice_full line 284
  29. lemma OAI.SingleLatticeCovering.ConstructionA.covolume_lattice line 288
  30. lemma OAI.SingleLatticeCovering.ConstructionA.generator_mem line 297
  31. lemma OAI.SingleLatticeCovering.ConstructionA.integer_mem line 302
  32. lemma OAI.SingleLatticeCovering.ConstructionA.mem_lattice_iff line 339
  33. def OAI.SingleLatticeCovering.ConstructionA.residue line 376
  34. def OAI.SingleLatticeCovering.ConstructionA.codeLattice line 380
  35. lemma OAI.SingleLatticeCovering.ConstructionA.lattice_eq_codeLattice line 395
  36. lemma OAI.SingleLatticeCovering.ConstructionA.normalized_lift line 432
  37. theorem OAI.SingleLatticeCovering.ConstructionA.line_lattice line 462
  38. def OAI.SingleLatticeCovering.ConstructionA.floorVector line 479
  39. def OAI.SingleLatticeCovering.ConstructionA.anchor line 480
  40. def OAI.SingleLatticeCovering.ConstructionA.integerLift line 481
  41. def OAI.SingleLatticeCovering.ConstructionA.gridCell line 483
  42. def OAI.SingleLatticeCovering.ConstructionA.cellPoint line 486
  43. lemma OAI.SingleLatticeCovering.ConstructionA.residue_integerLift line 489
  44. lemma OAI.SingleLatticeCovering.ConstructionA.cellPoint_mem line 494
  45. lemma OAI.SingleLatticeCovering.ConstructionA.cell_residual line 502
  46. lemma OAI.SingleLatticeCovering.ConstructionA.cell_residual_mem_grid line 512
  47. lemma OAI.SingleLatticeCovering.ConstructionA.gridCell_subset_cube line 524
  48. lemma OAI.SingleLatticeCovering.ConstructionA.integer_code_mem line 537
  49. lemma OAI.SingleLatticeCovering.ConstructionA.cell_bits line 545
  50. lemma OAI.SingleLatticeCovering.ConstructionA.gridCell_eq_pi line 568
  51. lemma OAI.SingleLatticeCovering.ConstructionA.gridCell_measurable line 574
  52. lemma OAI.SingleLatticeCovering.ConstructionA.floorVector_gridCell line 578
  53. lemma OAI.SingleLatticeCovering.ConstructionA.gridCell_disjoint line 591
  54. lemma OAI.SingleLatticeCovering.ConstructionA.anchor_floorVector line 601
  55. lemma OAI.SingleLatticeCovering.ConstructionA.cube_mem_gridCell line 614
  56. lemma OAI.SingleLatticeCovering.ConstructionA.gridCell_iUnion line 627
  57. lemma OAI.SingleLatticeCovering.ConstructionA.gridCell_volume line 637
  58. lemma OAI.SingleLatticeCovering.ConstructionA.gridCell_volume_real line 642
  59. lemma OAI.SingleLatticeCovering.ConstructionA.integral_gridCells line 647