OAI/Combinatorics/Progressions/Dynamics/FixedRefinementBudget.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.CellRefinement.refinementScaleLoss line 12
  2. def OAI.Erdos3.CellRefinement.refinementMatchingLoss line 15
  3. def OAI.Erdos3.CellRefinement.refinementRoundLoss line 19
  4. def OAI.Erdos3.CellRefinement.refinementComparisonBudget line 23
  5. theorem OAI.Erdos3.CellRefinement.refinementMatchingLoss_eq line 29
  6. theorem OAI.Erdos3.CellRefinement.refinementRoundLoss_eq line 37
  7. theorem OAI.Erdos3.CellRefinement.refinementMatchingLoss_nonneg line 44
  8. theorem OAI.Erdos3.CellRefinement.two_le_refinementRoundLoss line 54
  9. theorem OAI.Erdos3.CellRefinement.refinementMatchingLoss_mono_rank line 65
  10. theorem OAI.Erdos3.CellRefinement.refinementRoundLoss_mono_rank line 71
  11. theorem OAI.Erdos3.CellRefinement.fixed_refinement_scale_spec line 85