OAI/Combinatorics/Progressions/Lattices/ScalarResidueInteriorCell.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.paddedIntegerPoint line 13
  2. theorem OAI.Erdos3.paddedIntegerPoint_injective line 16
  3. theorem OAI.Erdos3.paddedIntegerPoint_covers line 25
  4. theorem OAI.Erdos3.sum_eq_sum_of_cover_and_support line 37
  5. theorem OAI.Erdos3.expect_eq_card_ratio_mul_expect line 52
  6. def OAI.Erdos3.residueCellLength line 70
  7. def OAI.Erdos3.residueCellCount line 72
  8. theorem OAI.Erdos3.residueCellCount_pos line 74
  9. theorem OAI.Erdos3.residueCellCount_padding line 77
  10. theorem OAI.Erdos3.residueCellLength_bounds line 93
  11. theorem OAI.Erdos3.residueCellLength_stride_mesh line 127
  12. def OAI.Erdos3.scalarResidueGridPoint line 146
  13. def OAI.Erdos3.scalarResidueGridOffset line 149
  14. def OAI.Erdos3.scalarResidueGridScale line 152
  15. theorem OAI.Erdos3.scalarResidueGridScale_pos line 155
  16. theorem OAI.Erdos3.scalarResidueGrid_normalized line 160
  17. theorem OAI.Erdos3.integerScalarCube_iff_normalized line 171
  18. theorem OAI.Erdos3.scalarResidueGridPoint_residue line 192
  19. theorem OAI.Erdos3.scalarResidueGridPoint_injective line 198
  20. theorem OAI.Erdos3.scalarResidueGridPoint_surjective line 206
  21. def OAI.Erdos3.scalarCubeResidueGridEquiv line 217
  22. theorem OAI.Erdos3.scalarCubeResidueGridEquiv_apply line 250
  23. theorem OAI.Erdos3.scalarCubeResidueWeights_grid_mean line 255
  24. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_im line 292
  25. theorem OAI.Erdos3.scalarCubeResidueWeights_grid_complexMean line 297
  26. theorem OAI.Erdos3.residue_index_bounds line 319
  27. theorem OAI.Erdos3.scalarCubeResidueGrid_index_bounds line 336
  28. theorem OAI.Erdos3.scalarCubeResidueGrid_padded_cover line 347
  29. theorem OAI.Erdos3.scalarCubeResidueWeights_riemann line 366
  30. def OAI.Erdos3.paddedResidueOffset line 395
  31. def OAI.Erdos3.paddedResidueStep line 399
  32. theorem OAI.Erdos3.paddedResidueCoordinates_eq line 402
  33. theorem OAI.Erdos3.scalarCubeResidueGrid_card line 414
  34. def OAI.Erdos3.scalarCubeResidueCutoffBudget line 432
  35. theorem OAI.Erdos3.scalarCubeResidueCutoff_loss line 438
  36. theorem OAI.Erdos3.scalarCubeResidueCutoff_bias line 469
  37. def OAI.Erdos3.paddedResidueDensityFactor line 495
  38. def OAI.Erdos3.paddedResidueDensityCap line 500
  39. theorem OAI.Erdos3.scalarCubeResidue_card_pos line 503
  40. theorem OAI.Erdos3.paddedResidueDensityFactor_pos line 517
  41. theorem OAI.Erdos3.paddedResidueDensityFactor_le line 525
  42. theorem OAI.Erdos3.scalarCubeResidueWeights_padded_mean line 566
  43. theorem OAI.Erdos3.scalarCubeResidueWeights_padded_bias line 617
  44. theorem OAI.Erdos3.scalarCubeResidue_exists_interior_cell line 652