OAI/Combinatorics/Progressions/Dynamics/ReplacementCellPotential.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.rpow_sub_rpow_ge_tangent line 12
  2. theorem OAI.Erdos3.peeling_rpow line 30
  3. theorem OAI.Erdos3.peeling_quarter line 69
  4. theorem OAI.Erdos3.sq_deviation_le_sqrt_gap line 77
  5. theorem OAI.Erdos3.sqrt_average_le_of_second_moment line 93
  6. theorem OAI.Erdos3.sqrt_average_sq_le line 143
  7. theorem OAI.Erdos3.fourth_root_product_average_le line 152
  8. theorem OAI.Erdos3.concave_power_drop line 198
  9. theorem OAI.Erdos3.density_invariant_preserved line 210
  10. theorem OAI.Erdos3.no_invariant_of_descent line 221
  11. theorem OAI.Erdos3.Peeling.step_mass_bounds line 253
  12. theorem OAI.Erdos3.Peeling.step_potential_le line 263
  13. theorem OAI.Erdos3.Peeling.step_coefficient_le_mass_drop line 274
  14. theorem OAI.Erdos3.fourth_root_product_average_le_means line 295
  15. theorem OAI.Erdos3.expect_quarter_product_le line 330
  16. theorem OAI.Erdos3.expect_quarter_product_contraction line 344
  17. theorem OAI.Erdos3.normalized_quarter_potential_contraction line 368
  18. theorem OAI.Erdos3.normalized_quarter_potential_contraction_either line 400
  19. theorem OAI.Erdos3.quarter_contraction_factor_bounds line 414
  20. theorem OAI.Erdos3.parent_cell_potential_le line 434
  21. theorem OAI.Erdos3.normalized_cell_cap line 450
  22. theorem OAI.Erdos3.small_ratio_quarter_potential_le line 458
  23. theorem OAI.Erdos3.combine_matched_potential_contractions line 474
  24. def OAI.Erdos3.CellRefinement.replacementPotential line 492
  25. theorem OAI.Erdos3.CellRefinement.replacementPotential_nonneg line 495
  26. theorem OAI.Erdos3.CellRefinement.replacementPotential_le line 505
  27. theorem OAI.Erdos3.CellRefinement.replacementPotential_eq_cell_means line 518