OAI/Combinatorics/Progressions/Lattices/ContainedFullIntervalResidueIdentity.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.principalResidueWeights_cube_support line 24
  2. def OAI.Erdos3.containedProgressionResidueLaw line 32
  3. theorem OAI.Erdos3.containedProgressionResidueLaw_mean line 35
  4. theorem OAI.Erdos3.containedProgressionResidueLaw_support line 43
  5. theorem OAI.Erdos3.containedProgressionResidueLaw_matrix line 59
  6. theorem OAI.Erdos3.containedProgressionResidueLaw_label_eq line 84
  7. theorem OAI.Erdos3.FiniteProbabilityWeights.toPMF_injective line 111
  8. def OAI.Erdos3.principalResidueNormalizedSource line 131
  9. theorem OAI.Erdos3.principalResidueNormalizedSource_toPMF line 138
  10. theorem OAI.Erdos3.principalResidueNormalizedSource_source line 145
  11. theorem OAI.Erdos3.principalResidueNormalizedSource_primitive line 152
  12. theorem OAI.Erdos3.principalResidueWeights_normalized_law line 159
  13. theorem OAI.Erdos3.principalResidueWeights_eq_normalized_pi line 171
  14. theorem OAI.Erdos3.principalResidueWeights_normalized_blocks line 178
  15. theorem OAI.Erdos3.principalTuple_complex_disintegrate_normalized line 189
  16. theorem OAI.Erdos3.principalResidueWeights_axis_pair_law line 224
  17. theorem OAI.Erdos3.principalResidueWeights_axis_block_law line 233
  18. theorem OAI.Erdos3.principalResidueWeights_axis_integer_law line 246
  19. def OAI.Erdos3.principalResidueAxisJetPMF line 263
  20. theorem OAI.Erdos3.principalResidueWeightedAxis_jet_sum_law line 271
  21. def OAI.Erdos3.principalResidueAxisGridDensity line 308
  22. theorem OAI.Erdos3.principalResidueAxisGridDensity_eq_normalized line 313
  23. theorem OAI.Erdos3.principalResidueAxisGridDensity_error_of_tail line 328
  24. theorem OAI.Erdos3.fullIntervalProgression_eq line 354
  25. theorem OAI.Erdos3.fullIntervalProgression_subset line 358
  26. theorem OAI.Erdos3.fullIntervalProgression_card line 362
  27. theorem OAI.Erdos3.containedProgressionTupleMap_fullInterval_of_cube line 372
  28. theorem OAI.Erdos3.principalCubeWeights_fullInterval_fiberLaw line 384
  29. theorem OAI.Erdos3.containedProgressionResidueLaw_fullInterval line 394
  30. theorem OAI.Erdos3.containedSupportedProgressionLaw_fullInterval line 403
  31. theorem OAI.Erdos3.containedProgressionResidueLaw_fullInterval_eq_condition line 414
  32. theorem OAI.Erdos3.containedProgressionResidueLaw_fullInterval_integer_law line 426