OAI/Combinatorics/Progressions/Estimates/QuantitativeNoninjectivity.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.noninjectivityIndicator line 13
  2. theorem OAI.Erdos3.noninjectivityIndicator_nonneg line 16
  3. theorem OAI.Erdos3.noninjectivityIndicator_postcompose line 21
  4. theorem OAI.Erdos3.noninjectivityIndicator_le_pairs line 28
  5. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_fintype_sum line 53
  6. theorem OAI.Erdos3.FiniteProbabilityWeights.noninjectivity_le line 59
  7. theorem OAI.Erdos3.FiniteProbabilityWeights.reweightPositive_noninjectivity_le line 78
  8. def OAI.Erdos3.BooleanCubeKernel.jointIntegerPhysicalSite line 106
  9. theorem OAI.Erdos3.BooleanCubeKernel.jointIntegerPhysicalSite_cast line 110
  10. theorem OAI.Erdos3.BooleanCubeKernel.jointIntegerPhysicalSite_mem_box line 118
  11. theorem OAI.Erdos3.BooleanCubeKernel.noninjectivityIndicator_joint line 130
  12. def OAI.Erdos3.BooleanCubeKernel.rowDifferenceCoefficients line 147
  13. theorem OAI.Erdos3.BooleanCubeKernel.rowDifferenceCoefficients_linear line 151
  14. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_site_collision_le line 163
  15. theorem OAI.Erdos3.integerArrayLinearForm_add line 202
  16. theorem OAI.Erdos3.BooleanCubeKernel.anchored_selectedResidue_site_collision_le line 209
  17. theorem OAI.Erdos3.BooleanCubeKernel.noninjectivityIndicator_centered line 257
  18. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_distinct_collision_le line 264
  19. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_noninjectivity_le line 285
  20. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_tilted_noninjectivity_le line 302
  21. theorem OAI.Erdos3.BooleanCubeKernel.anchored_selectedResidue_distinct_collision_le line 342
  22. theorem OAI.Erdos3.BooleanCubeKernel.anchored_selectedResidue_noninjectivity_le line 363
  23. theorem OAI.Erdos3.BooleanCubeKernel.anchored_selectedResidue_tilted_noninjectivity_le line 380
  24. theorem OAI.Erdos3.BooleanCubeKernel.anchored_selectedResidue_tilted_collision_small line 423
  25. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_tilted_collision_small line 459