OAI/Combinatorics/Progressions/FixedDensity/AdaptiveCoarseTargetRegularity.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule line 9
  2. def OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.IsAdmissible line 20
  3. inductive OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing line 31
  4. def OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing.tolerance line 45
  5. def OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing.budget line 54
  6. def OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing.length line 63
  7. def OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing.index line 72
  8. theorem OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing.tolerance_node_last line 82
  9. theorem OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing.tolerance_node_castSucc line 97
  10. theorem OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing.budget_node_last line 113
  11. theorem OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing.budget_node_castSucc line 128
  12. theorem OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing.length_node_last line 144
  13. theorem OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing.length_node_castSucc line 159
  14. theorem OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing.index_node_last line 175
  15. theorem OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing.index_node_castSucc line 190
  16. theorem OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing.index_lt_length line 205
  17. theorem OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing.tolerance_nonneg line 221
  18. theorem OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing.budget_spec line 238
  19. theorem OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Landing.length_pos line 275
  20. structure OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Realization line 294
  21. theorem OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.Realization.nonempty line 306
  22. theorem OAI.Erdos3.FixedDensity.AdaptiveCoarseTargetSchedule.exists_landing_certificate line 707