OAI/Combinatorics/Progressions/Estimates/RefinementEnlargement.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.mixed_center_contraction line 14
  2. theorem OAI.Erdos3.parent_center_potential_contraction line 41
  3. theorem OAI.Erdos3.center_refinement_integral_bound line 86
  4. theorem OAI.Erdos3.parent_and_centers_integral_bound line 110
  5. theorem OAI.Erdos3.exists_center_refinement line 134
  6. theorem OAI.Erdos3.CellRefinement.exists_admissible_independent_return_shape line 216
  7. theorem OAI.Erdos3.CellRefinement.exists_refinement_moment_orders line 271
  8. theorem OAI.Erdos3.CellRefinement.matched_refinement_alternatives line 281
  9. theorem OAI.Erdos3.CellRefinement.matched_independent_refinement_alternatives line 367
  10. theorem OAI.Erdos3.CellRefinement.unbalanced_factor_bounds line 459
  11. theorem OAI.Erdos3.CellRefinement.capped_center_alternatives line 475
  12. theorem OAI.Erdos3.CellRefinement.exists_capped_parent_refinement line 581
  13. theorem OAI.Erdos3.CellRefinement.capped_parent_bound_of_children line 729
  14. theorem OAI.Erdos3.CellRefinement.bilinear_refinement_step line 811
  15. theorem OAI.Erdos3.CellRefinement.admissible_child_bound_of_bounded_shapes line 918
  16. theorem OAI.Erdos3.CellRefinement.normalized_bilinear_refinement_step line 935
  17. theorem OAI.Erdos3.CellRefinement.fixed_refinement_thresholds line 1015
  18. def OAI.Erdos3.CellRefinement.refinementContraction line 1022
  19. theorem OAI.Erdos3.CellRefinement.refinementContraction_eq line 1025
  20. theorem OAI.Erdos3.CellRefinement.refinementContraction_bounds line 1032
  21. theorem OAI.Erdos3.CellRefinement.refinement_cap_cutoff line 1039
  22. theorem OAI.Erdos3.CellRefinement.refinement_tiny_cutoff line 1049
  23. theorem OAI.Erdos3.CellRefinement.refinement_return_error line 1059
  24. theorem OAI.Erdos3.CellRefinement.refinement_peeling_error line 1073
  25. theorem OAI.Erdos3.CellRefinement.refinement_total_error line 1091
  26. theorem OAI.Erdos3.CellRefinement.refinement_enlargement_bounds line 1109
  27. theorem OAI.Erdos3.CellRefinement.refinement_enlargement_amplitude line 1119
  28. theorem OAI.Erdos3.CellRefinement.refinement_enlargement_error line 1129
  29. theorem OAI.Erdos3.CellRefinement.signed_comparison_amplitude line 1139