OAI/Combinatorics/Progressions/FixedDensity/SourceFullCoarseTargetRegularity.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.sourceFullCommonTolerance line 10
  2. def OAI.Erdos3.FixedDensity.sourceFullRankGap line 15
  3. theorem OAI.Erdos3.FixedDensity.sourceFullCommonTolerance_pos line 21
  4. theorem OAI.Erdos3.FixedDensity.sourceFullRankGap_pos line 29
  5. def OAI.Erdos3.FixedDensity.adaptiveSelectedCoarseLayerBound line 39
  6. structure OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule line 52
  7. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.scale_antitone line 82
  8. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.scaleFloor_le line 98
  9. structure OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.Certificate line 111
  10. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.certificate_nonempty line 149
  11. def OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.zero line 243
  12. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.certificate_nonempty_zero line 274
  13. def OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.nodeScale line 291
  14. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.nodeScale_node line 310
  15. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.nodeScale_node_last line 331
  16. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.nodeScale_node_castSucc line 352
  17. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.sourceFullCommonTolerance_nodeScale line 374
  18. def OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.lowerInitialBound line 400
  19. def OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.node line 412
  20. structure OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.Bounded line 539
  21. def OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.Bounded.castInitialBound line 554
  22. def OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.boundedZero line 571
  23. def OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.factorLowerInitialBound line 586
  24. def OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.sourceFullStageFactor line 595
  25. def OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.sourceFullStageBound line 621
  26. def OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.sourceFullStagePlan line 635
  27. def OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.sourceFullStageTolerance line 652
  28. def OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.sourceFullStageBudget line 665
  29. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.sourceFullStageFactor_zero line 679
  30. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.sourceFullStageFactor_succ line 692
  31. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.fixedUpperLayerComplexityFactor_sourceFullStageBudget line 710
  32. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.lowerInitialBound_sourceFullStageBudget line 743
  33. def OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.sourceFullStageNext line 767
  34. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.sourceFullStageNext_ceiling line 787
  35. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.sourceFullStageTolerance_pos line 802
  36. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.bounded_nonempty line 818
  37. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.nonempty line 949
  38. theorem OAI.Erdos3.FixedDensity.SourceFullCoarseTargetSchedule.certificate_nonempty_full line 962