OAI/Geometry/LatticeCovering/MeanHoles.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleLatticeCovering.PrimeKernel.liftCoeff line 42
  2. lemma OAI.SingleLatticeCovering.PrimeKernel.modForm_liftCoeff line 45
  3. def OAI.SingleLatticeCovering.PrimeKernel.finResidue line 55
  4. lemma OAI.SingleLatticeCovering.PrimeKernel.card_badOffsets line 61
  5. abbrev OAI.SingleLatticeCovering.PrimeKernel.ensembleFull line 75
  6. def OAI.SingleLatticeCovering.PrimeKernel.meanPrimeHole line 78
  7. lemma OAI.SingleLatticeCovering.PrimeKernel.meanPrimeHole_le_grid line 81
  8. lemma OAI.SingleLatticeCovering.PrimeKernel.fintype_sum_irrel line 106
  9. lemma OAI.SingleLatticeCovering.PrimeKernel.fullMiss_eq_avoidance line 114
  10. lemma OAI.SingleLatticeCovering.PrimeKernel.meanFull_generic line 136
  11. lemma OAI.SingleLatticeCovering.PrimeKernel.meanFull_integerGrid line 146
  12. lemma OAI.SingleLatticeCovering.PrimeKernel.scaleFactor_eq_primeScale_inv line 152
  13. lemma OAI.SingleLatticeCovering.PrimeKernel.gridMap_eq_scaledIntegerPoint line 157
  14. lemma OAI.SingleLatticeCovering.PrimeKernel.gridUnitCell_norm_le line 164
  15. lemma OAI.SingleLatticeCovering.PrimeKernel.eventually_grid_thick line 170
  16. lemma OAI.SingleLatticeCovering.AffineVoid.conditioning_factor_tendsto line 195
  17. lemma OAI.SingleLatticeCovering.AffineVoid.eventually_factor_mul_lt line 213
  18. theorem OAI.SingleLatticeCovering.PrimeKernel.eventually_meanPrimeHole_centered_source line 227
  19. lemma OAI.SingleLatticeCovering.Horizontal.FullLattice.hole_vadd line 276
  20. lemma OAI.SingleLatticeCovering.PrimeKernel.meanPrimeHole_vadd line 295
  21. theorem OAI.SingleLatticeCovering.PrimeKernel.eventually_meanPrimeHole_source line 303
  22. lemma OAI.SingleLatticeCovering.PrimeKernel.ensembleFull_covolume line 334
  23. lemma OAI.SingleLatticeCovering.PrimeKernel.meanPrimeHole_le_one line 338
  24. theorem OAI.SingleLatticeCovering.PrimeKernel.eventually_meanPrimeHole_all line 357
  25. lemma OAI.SingleLatticeCovering.PrimeKernel.exists_le_finite_average line 381
  26. lemma OAI.SingleLatticeCovering.PrimeKernel.weighted_meanPrimeHole_sample line 390
  27. theorem OAI.SingleLatticeCovering.PrimeKernel.common_horizontal_source line 408
  28. theorem OAI.SingleLatticeCovering.PrimeKernel.scaled_common_horizontal_source line 476
  29. theorem OAI.SingleLatticeCovering.PrimeKernel.common_horizontal_from_circuits line 504
  30. theorem OAI.SingleLatticeCovering.Assembly.sections_and_circuits_cover line 546
  31. theorem OAI.SingleLatticeCovering.Assembly.eventual_main_reduction_circuits line 631