OAI/Combinatorics/Progressions/Estimates/RefinementMatchingGeometry.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.LocalConvolution.exists_unbalanced_matched_contraction line 15
  2. theorem OAI.Erdos3.LocalConvolution.exists_small_scale_unbalanced_shape line 97
  3. theorem OAI.Erdos3.LocalConvolution.exists_small_scale_unbalanced_contraction line 173
  4. theorem OAI.Erdos3.LocalConvolution.unbalanced_shape_to_uniform line 256
  5. theorem OAI.Erdos3.LocalConvolution.exists_uniform_unbalanced_matched_contraction line 267
  6. def OAI.Erdos3.LocalConvolution.unbalancedReturnWidthLoss line 318
  7. theorem OAI.Erdos3.LocalConvolution.unbalanced_return_width_lower line 321
  8. theorem OAI.Erdos3.LocalConvolution.exists_unbalanced_independent_refinement line 339
  9. theorem OAI.Erdos3.Peeling.admissibleBohrShape_transfer line 410
  10. theorem OAI.Erdos3.Peeling.uniform_unbalanced_shape_in_parent line 419
  11. theorem OAI.Erdos3.Peeling.normalized_local_caps_from_parent line 430
  12. theorem OAI.Erdos3.LocalConvolution.exists_parent_unbalanced_contraction line 458
  13. theorem OAI.Erdos3.LocalConvolution.exists_parent_unbalanced_independent_refinement line 523
  14. def OAI.Erdos3.CellRefinement.refinementMatchingWidthLoss line 610
  15. theorem OAI.Erdos3.CellRefinement.exists_refinement_matching_geometry line 616