OAI/Combinatorics/Progressions/Lattices/AllocatedModularRankAffineProbability.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.modularAffineSpatial_power_ratio_le line 13
  2. theorem OAI.Erdos3.modularRankSmallBallExponent_le_half line 29
  3. theorem OAI.Erdos3.modularAffineSpatial_sqrt_le_tag line 39
  4. theorem OAI.Erdos3.modularAffineSpatial_gcd_cost_le_sqrt line 48
  5. theorem OAI.Erdos3.modularAffineSpatial_gcd_cost_le_tag line 58
  6. theorem OAI.Erdos3.designatedPolynomial_affine_linearRow_zero_probability_le line 78
  7. theorem OAI.Erdos3.designatedPolynomial_expected_affine_linearRow_zero_le line 105
  8. theorem OAI.Erdos3.affineCoefficientArray_update line 129
  9. theorem OAI.Erdos3.vectorDesignatedRankFailureProbability_affine_mean_le line 141
  10. theorem OAI.Erdos3.vectorDesignatedRankFailureProbability_affine_mean_le_of_unit line 176
  11. def OAI.Erdos3.affineSpatialCoefficients line 204
  12. theorem OAI.Erdos3.vectorDesignatedRankFailureProbability_affineSpatial_zero_mean_le line 209
  13. theorem OAI.Erdos3.affineSpatialCoefficients_eq_self line 245
  14. theorem OAI.Erdos3.vectorDesignatedRankFailureProbability_affineSpatial_mean_le line 252
  15. theorem OAI.Erdos3.taggedVectorDesignatedRank_affineSpatial_exceptional_probability line 290
  16. theorem OAI.Erdos3.scalarCoefficientBad_affineSpatial_probability_eq line 419
  17. theorem OAI.Erdos3.scalarCoefficientBad_affineSpatial_probability line 442
  18. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceIsSpatial line 482
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceIsSpatial_degree line 487
  20. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceAffineCoefficients line 495
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceAffineCoefficients_spatial line 502
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceAffineCoefficients_nonspatial line 509
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceAffineCoefficients_intCast line 516
  24. def OAI.Erdos3.VectorPolynomial.allocatedMixedAffineSelectedValues line 527
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedAffineSelectedValues_cast line 536
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedAffineSelectedValues_natCast line 550
  27. def OAI.Erdos3.VectorPolynomial.allocatedFullSmoothAffine line 577
  28. def OAI.Erdos3.VectorPolynomial.allocatedSelectedNoiseOffset line 584
  29. def OAI.Erdos3.VectorPolynomial.allocatedSelectedSmoothAffine line 591
  30. theorem OAI.Erdos3.VectorPolynomial.allocatedFullSmoothAffine_extend line 599
  31. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedSelectedValues_affine line 626
  32. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedFullArray_affine_refresh_selected line 638
  33. theorem OAI.Erdos3.VectorPolynomial.allocatedFullSmoothAffine_intCast line 660
  34. theorem OAI.Erdos3.VectorPolynomial.affine_uniform_eventProbability_le_instances line 681
  35. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceNaturalStride line 693
  36. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceAffineCoefficients_eq_scalar line 698
  37. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceModulusBad_affine_probability line 736