OAI/Combinatorics/Progressions/Lattices/CubeResidueSupport.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerScalarCubeValue line 18
  2. def OAI.Erdos3.IntegerScalarCube line 21
  3. abbrev OAI.Erdos3.IntegerScalarCubeBox line 24
  4. def OAI.Erdos3.integerScalarCubeSet line 27
  5. theorem OAI.Erdos3.mem_integerScalarCubeSet line 32
  6. theorem OAI.Erdos3.integerScalarCube_coordinates line 38
  7. theorem OAI.Erdos3.integerScalarCubeValue_cast line 50
  8. theorem OAI.Erdos3.integerScalarCube_small_positive line 55
  9. def OAI.Erdos3.integerScalarCubeBoxZero line 82
  10. theorem OAI.Erdos3.integerScalarCubeSet_nonempty line 85
  11. theorem OAI.Erdos3.integerScalarCubeBox_card line 92
  12. theorem OAI.Erdos3.integerScalarCubeSet_card_lower line 99
  13. theorem OAI.Erdos3.nat_div_half_lower line 119
  14. theorem OAI.Erdos3.integerScalarCube_iff_supported line 127
  15. def OAI.Erdos3.integerScalarCubeEquiv line 139
  16. def OAI.Erdos3.integerScalarCubeReference line 160
  17. theorem OAI.Erdos3.integerScalarCubeReference_mass line 165
  18. theorem OAI.Erdos3.integerScalarCubeReference_mass_pos line 172
  19. def OAI.Erdos3.integerScalarCubeDensityCap line 178
  20. theorem OAI.Erdos3.integerScalarCubeDensityCap_pos line 181
  21. theorem OAI.Erdos3.integerScalarCubeReference_mass_lower line 186
  22. def OAI.Erdos3.integerScalarCubeWeights line 212
  23. theorem OAI.Erdos3.integerScalarCubeWeights_weight_le line 218
  24. def OAI.Erdos3.scalarCubeResidueSet line 231
  25. theorem OAI.Erdos3.mem_scalarCubeResidueSet line 236
  26. theorem OAI.Erdos3.scalarResiduePoint_bound line 242
  27. theorem OAI.Erdos3.scalarResiduePoint_cast line 249
  28. theorem OAI.Erdos3.scalarCubeResidueSet_card_lower line 254
  29. theorem OAI.Erdos3.integerScalarCubeWeights_root_bounds line 295
  30. theorem OAI.Erdos3.integerScalarCubePi_root_bounds line 308
  31. theorem OAI.Erdos3.integerScalarCubePi_root_real_bounds line 319
  32. theorem OAI.Erdos3.affineKernelEndpoint_error line 329
  33. theorem OAI.Erdos3.affineKernelEndpoint_error_nat line 342
  34. def OAI.Erdos3.scalarCubeDifferenceMatrix line 357
  35. def OAI.Erdos3.scalarCubeLargeCokernelEvent line 361
  36. theorem OAI.Erdos3.scalarCube_largeCokernel_probability_le line 366
  37. theorem OAI.Erdos3.integerScalarCubeWeights_mean line 400
  38. theorem OAI.Erdos3.integerScalarCubeWeights_supported_mean line 407
  39. def OAI.Erdos3.scalarCubeResidueDensityCap line 420
  40. theorem OAI.Erdos3.scalarCubeResidueDensityCap_pos line 423
  41. theorem OAI.Erdos3.scalarCubeResidueReference_mass_lower line 428
  42. theorem OAI.Erdos3.scalarCubeResidue_mass_lower line 462
  43. theorem OAI.Erdos3.scalarCubeResidue_mass_pos line 471
  44. def OAI.Erdos3.scalarCubeResidueWeights line 482
  45. theorem OAI.Erdos3.scalarCubeResidueWeights_mean line 491
  46. theorem OAI.Erdos3.scalarCubeResidueWeights_weight_le line 502
  47. theorem OAI.Erdos3.scalarCubeResidue_pi_eventProbability_le line 515
  48. theorem OAI.Erdos3.scalarCubeResidueWeights_support line 535
  49. theorem OAI.Erdos3.scalarCubeResiduePi_support line 547
  50. theorem OAI.Erdos3.scalarCubeResiduePi_condition line 562