OAI/Combinatorics/Progressions/FixedDensity/SourceFullBundleRemovalParameters.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.sourceBundleDensity line 12
  2. def OAI.Erdos3.FixedDensity.sourceBundleDefectScale line 15
  3. theorem OAI.Erdos3.FixedDensity.sourceBundleDensity_pos line 19
  4. theorem OAI.Erdos3.FixedDensity.sourceBundleDensity_nonneg line 25
  5. theorem OAI.Erdos3.FixedDensity.sourceBundleDensity_le_one line 31
  6. theorem OAI.Erdos3.FixedDensity.sourceBundleDensity_antitone line 39
  7. theorem OAI.Erdos3.FixedDensity.mul_sourceBundleDensity_le line 48
  8. theorem OAI.Erdos3.FixedDensity.sourceBundleDefectScale_pos line 61
  9. theorem OAI.Erdos3.FixedDensity.sourceBundleDefectScale_nonneg line 68
  10. def OAI.Erdos3.FixedDensity.sourceBundleSelectedScale line 76
  11. theorem OAI.Erdos3.FixedDensity.sourceBundleSelectedScale_zero line 81
  12. theorem OAI.Erdos3.FixedDensity.sourceBundleSelectedScale_of_le line 86
  13. def OAI.Erdos3.FixedDensity.sourceBundleRankwiseDensity line 92
  14. def OAI.Erdos3.FixedDensity.sourceBundleRankwiseDefect line 96
  15. theorem OAI.Erdos3.FixedDensity.sourceBundleRankwiseDensity_pos line 102
  16. theorem OAI.Erdos3.FixedDensity.sourceBundleRankwiseDensity_le_one line 108
  17. theorem OAI.Erdos3.FixedDensity.sourceBundleRankwiseDefect_nonneg line 114
  18. theorem OAI.Erdos3.FixedDensity.sourceBundleRankwiseDensity_zero_le line 120
  19. theorem OAI.Erdos3.FixedDensity.le_bundleRankwiseDensityFloor_of_zero_le line 129
  20. def OAI.Erdos3.FixedDensity.sourceBundleRemovalGrowth line 139
  21. theorem OAI.Erdos3.FixedDensity.sourceBundleRemovalGrowth_apply line 152
  22. theorem OAI.Erdos3.FixedDensity.sourceBundleRemovalGrowth_polynomial_le line 158
  23. structure OAI.Erdos3.FixedDensity.SourceBundleRemovalGrowthConditions line 164
  24. theorem OAI.Erdos3.FixedDensity.exists_sourceBundleRemovalGrowthCoefficient line 171
  25. theorem OAI.Erdos3.FixedDensity.one_div_sourceBundleRemovalGrowth_le line 210
  26. theorem OAI.Erdos3.FixedDensity.sourceFullRankGap_div_sourceBundleDefectScale_sq_le line 240
  27. theorem OAI.Erdos3.FixedDensity.sqrt_sourceBundleDefectScale_sq_four_div_pow_le line 285
  28. theorem OAI.Erdos3.FixedDensity.div_pow_le_sq_of_le_scaled_pow line 323
  29. theorem OAI.Erdos3.FixedDensity.sourceBundleRankwiseEnvelope_and_error_lt_half line 337
  30. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.Certificate.scale_antitone line 435
  31. structure OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.Bounded.Certificate line 456
  32. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.Bounded.certificate_nonempty line 470