OAI/Combinatorics/Progressions/Dynamics/PeelingReplacementPotential.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.Peeling.potentialCost_zero line 14
  2. theorem OAI.Erdos3.Peeling.Chain.potential_budget_nonneg line 22
  3. theorem OAI.Erdos3.Peeling.pair_potential_budget line 33
  4. theorem OAI.Erdos3.Peeling.pair_coefficient_budget line 51
  5. theorem OAI.Erdos3.Peeling.coefficientCost_nonneg line 74
  6. theorem OAI.Erdos3.Peeling.pair_coefficientCost_le line 82
  7. theorem OAI.Erdos3.Peeling.weighted_pair_error_le line 95
  8. theorem OAI.Erdos3.Peeling.contraction_after_peeling line 105
  9. def OAI.Erdos3.CellRefinement.replacementPotentialSum line 129
  10. theorem OAI.Erdos3.CellRefinement.replacementPotentialSum_nonneg line 135
  11. theorem OAI.Erdos3.CellRefinement.replacementPotentialSum_le_cost line 146
  12. theorem OAI.Erdos3.CellRefinement.pair_replacement_potential_budget line 162
  13. theorem OAI.Erdos3.CellRefinement.pair_replacement_contraction line 183