OAI/Combinatorics/Progressions/Linear/AllocatedModularRankBadProduct.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.homogeneousComponent_map_ringHom line 17
  2. theorem OAI.Erdos3.modularBoundedCoefficientPolynomial_map line 23
  3. theorem OAI.Erdos3.modularUnselectedCoefficientPolynomial_map line 29
  4. theorem OAI.Erdos3.restrictedUnselectedTop_map line 36
  5. theorem OAI.Erdos3.restrictedMonomialSumTop_map line 47
  6. theorem OAI.Erdos3.canonicalSelectedTopResidual_map line 66
  7. theorem OAI.Erdos3.canonicalSelectedLongTopResidual_map line 74
  8. theorem OAI.Erdos3.canonicalSelectedLongTopResidual_integer_reduce line 83
  9. def OAI.Erdos3.VectorPolynomial.allocatedTaggedRankIntegerResidual line 108
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedTaggedRankIntegerResidual_reduce line 131
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedTaggedRankPolynomial_eq_integer_designated line 164
  12. def OAI.Erdos3.VectorPolynomial.allocatedTaggedRankFailureProbability line 201
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedTaggedRankFailureProbability_eq_designated line 217
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedTaggedRank_exceptional_probability line 235
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedTaggedRank_exceptional_probability_uniform line 272
  16. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceRankPolynomial line 303
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceRankPolynomial_eq_actual line 321
  18. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceRankFailureProbability line 340
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceRankFailureProbability_eq_designated line 356
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceRank_exceptional_probability line 378
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceRank_exceptional_probability_uniform line 418
  22. abbrev OAI.Erdos3.VectorPolynomial.AllocatedCongruenceScalarIndex line 462
  23. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceRankBlockFamily line 466
  24. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceRankIntegerResidualFamily line 477
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceRankFailureProbability_eq_integer_model line 503
  26. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceModulusBad line 518
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceModulusBad_iff_scalarCoefficientBad line 527
  28. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceRankBad line 540
  29. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceRankBad_eq_smoothCoefficientRankBad line 545
  30. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceModulusBad_good line 558
  31. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceRankBad_good line 568
  32. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceRankPolynomial_original line 601
  33. theorem OAI.Erdos3.VectorPolynomial.uniform_eventProbability_le_instances line 631
  34. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceModulusBad_probability line 665
  35. theorem OAI.Erdos3.VectorPolynomial.mixed_uniform_eventProbability_le_instances line 706
  36. def OAI.Erdos3.VectorPolynomial.allocatedMixedModulusBad line 738
  37. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedModulusBad_probability line 744
  38. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedRankBad_eq line 761
  39. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedRank_primePower_event line 773
  40. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedRank_bad_product_probability line 804
  41. theorem OAI.Erdos3.VectorPolynomial.exists_early_allocatedMixedRank_bad_product_cutoff line 836