OAI/Combinatorics/Progressions/Polynomial/PolynomialCoordinatePartition.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.schmidtStepFactor line 15
  2. theorem OAI.Erdos3.schmidtStepFactor_bounds line 19
  3. theorem OAI.Erdos3.schmidt_step_epsilon_bounds line 54
  4. theorem OAI.Erdos3.schmidt_step_epsilon_budget line 59
  5. theorem OAI.Erdos3.schmidtRadiusFactor_mono line 74
  6. theorem OAI.Erdos3.schmidtStepFactor_mono line 82
  7. def OAI.Erdos3.schmidtMassMultiplier line 108
  8. def OAI.Erdos3.schmidtMassCeiling line 111
  9. theorem OAI.Erdos3.schmidtMassMultiplier_ge_one line 114
  10. theorem OAI.Erdos3.schmidtMassCeiling_ge line 125
  11. theorem OAI.Erdos3.schmidtMassBudget_closes line 129
  12. def OAI.Erdos3.schmidtDegreeConstant line 182
  13. theorem OAI.Erdos3.schmidt_uniform_cost_bounds line 186
  14. theorem OAI.Erdos3.schmidt_primitive_dilation_room line 243
  15. theorem OAI.Erdos3.exists_schmidt_dilated_mean_transfer line 278
  16. theorem OAI.Erdos3.PolynomialIntervalPowerBound.dimension_reduction line 353
  17. theorem OAI.Erdos3.one_le_power_mul_of_one_le_mul line 435
  18. theorem OAI.Erdos3.PolynomialIntervalPowerBound.gaussian_mean_iteration line 443
  19. theorem OAI.Erdos3.PolynomialIntervalPowerBound.gaussian_mean_lower_bound line 530
  20. theorem OAI.Erdos3.schmidt_gaussian_mean_lower_bound line 557
  21. def OAI.Erdos3.schmidtMeanDenominator line 580
  22. theorem OAI.Erdos3.schmidtMeanDenominator_pos line 584
  23. theorem OAI.Erdos3.exists_positive_lattice_approx_of_gaussian_mean line 596
  24. theorem OAI.Erdos3.PolynomialIntervalPowerBound.lattice_recurrence line 614
  25. def OAI.Erdos3.schmidtRecurrenceExponent line 636
  26. theorem OAI.Erdos3.schmidt_recurrence_mass_bounds line 638
  27. theorem OAI.Erdos3.schmidt_recurrence_denominator_bound line 678
  28. theorem OAI.Erdos3.monomial_recurrence_tail_budget line 724
  29. theorem OAI.Erdos3.schmidt_recurrence_numeric_conditions line 764
  30. def OAI.Erdos3.schmidtRecurrenceBase line 793
  31. theorem OAI.Erdos3.schmidtRecurrenceBase_bounds line 796
  32. theorem OAI.Erdos3.PolynomialIntervalPowerBound.simultaneous_monomial_recurrence_at_scale line 810
  33. theorem OAI.Erdos3.PolynomialIntervalPowerBound.simultaneous_monomial_recurrence line 837
  34. theorem OAI.Erdos3.simultaneous_monomial_recurrence line 861
  35. theorem OAI.Erdos3.PolynomialIntervalPowerBound.polynomial_coordinate_reduction line 884
  36. theorem OAI.Erdos3.PolynomialIntervalPowerBound.polynomial_progression_reduction line 942
  37. def OAI.Erdos3.PolynomialCoordinatePartitionBound line 1004
  38. theorem OAI.Erdos3.polynomialCoordinatePartitionBound_zero line 1014
  39. theorem OAI.Erdos3.PolynomialCoordinatePartitionBound.step line 1030
  40. theorem OAI.Erdos3.exists_polynomial_coordinate_partition_bound line 1110