OAI/Combinatorics/Progressions/FixedDensity/RankwiseBundleEnvelopeSelection.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.bundleRankwiseDensityFloor line 11
  2. theorem OAI.Erdos3.FixedDensity.bundleRankwiseDensityFloor_zero line 16
  3. theorem OAI.Erdos3.FixedDensity.bundleRankwiseDensityFloor_succ line 21
  4. theorem OAI.Erdos3.FixedDensity.bundleRankwiseDensityFloor_pos line 26
  5. theorem OAI.Erdos3.FixedDensity.bundleRankwiseDensityFloor_le line 35
  6. theorem OAI.Erdos3.FixedDensity.bundleRankwiseDensityFloor_antitone line 50
  7. def OAI.Erdos3.FixedDensity.bundleRankwiseStepIncrement line 57
  8. def OAI.Erdos3.FixedDensity.bundleRankwiseNextRow line 67
  9. def OAI.Erdos3.FixedDensity.bundleRankwiseEnvelopeError line 76
  10. theorem OAI.Erdos3.FixedDensity.bundleRankwiseNextRow_zero line 84
  11. theorem OAI.Erdos3.FixedDensity.bundleRankwiseNextRow_succ line 90
  12. theorem OAI.Erdos3.FixedDensity.bundleRankwiseEnvelopeError_zero_order line 99
  13. theorem OAI.Erdos3.FixedDensity.bundleRankwiseEnvelopeError_succ_order line 105
  14. theorem OAI.Erdos3.FixedDensity.bundleRankwiseStepIncrement_nonneg line 112
  15. theorem OAI.Erdos3.FixedDensity.bundleRankwiseNextRow_nonneg line 122
  16. theorem OAI.Erdos3.FixedDensity.bundleRankwiseEnvelopeError_nonneg line 136
  17. theorem OAI.Erdos3.FixedDensity.bundleRankwiseEnvelopeError_zero_card line 152
  18. theorem OAI.Erdos3.FixedDensity.bundleRankwiseEnvelopeError_monotone_card line 158
  19. theorem OAI.Erdos3.FixedDensity.bundleRankwiseEnvelopeError_le_succ_order line 175
  20. theorem OAI.Erdos3.FixedDensity.bundleRankwiseEnvelopeError_monotone_order line 186
  21. theorem OAI.Erdos3.FixedDensity.bundleRankwiseEnvelopeError_isEnvelope line 192
  22. theorem OAI.Erdos3.FixedDensity.bundleRankwiseNextRow_zero_parameters line 236
  23. theorem OAI.Erdos3.FixedDensity.bundleRankwiseEnvelopeError_zero_parameters line 249
  24. theorem OAI.Erdos3.FixedDensity.continuous_bundleRankwiseNextRow line 263
  25. theorem OAI.Erdos3.FixedDensity.continuous_bundleRankwiseEnvelopeError line 285
  26. def OAI.Erdos3.FixedDensity.bundleRankwiseScaledDefect line 305
  27. def OAI.Erdos3.FixedDensity.bundleRankwiseScaledUniformity line 309
  28. theorem OAI.Erdos3.FixedDensity.continuous_bundleRankwiseScaledDefect line 314
  29. theorem OAI.Erdos3.FixedDensity.continuous_bundleRankwiseScaledUniformity line 320
  30. theorem OAI.Erdos3.FixedDensity.bundleRankwiseScaledDefect_zero line 327
  31. theorem OAI.Erdos3.FixedDensity.bundleRankwiseScaledUniformity_zero line 333
  32. theorem OAI.Erdos3.FixedDensity.tendsto_bundleRankwiseScaledEnvelopeError_zero line 338
  33. theorem OAI.Erdos3.FixedDensity.exists_bundleRankwiseScaledEnvelopeError_lt line 363
  34. theorem OAI.Erdos3.FixedDensity.exists_bundleRankwiseScaledEnvelopeError_lt_half line 434
  35. def OAI.Erdos3.FixedDensity.bundleReverseDoublingHorizon line 459
  36. theorem OAI.Erdos3.FixedDensity.bundleReverseDoublingHorizon_two_mul_succ line 463
  37. theorem OAI.Erdos3.FixedDensity.bundleReverseDoublingHorizon_le_zero line 472
  38. theorem OAI.Erdos3.FixedDensity.bundleRankwiseStepIncrement_le_of_lower_le line 481
  39. theorem OAI.Erdos3.FixedDensity.bundleRankwiseEnvelopeError_le_finiteBudget line 533
  40. theorem OAI.Erdos3.FixedDensity.bundleRankwiseEnvelopeError_le_reverseDoublingBudget line 635
  41. theorem OAI.Erdos3.FixedDensity.bundleRankwiseEnvelope_and_error_lt_half_of_reverseDoublingBudget line 661