OAI/Combinatorics/Progressions/Fourier/UnbalancedBohrShape.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.Peeling.admissibleBohrShape line 17
  2. def OAI.Erdos3.Peeling.admissibleBohrCarriers line 22
  3. theorem OAI.Erdos3.Peeling.removed_cell_has_admissible_shape line 26
  4. theorem OAI.Erdos3.Peeling.exists_budgeted_bohr_peeling line 36
  5. theorem OAI.Erdos3.LocalConvolution.exists_bohr_average_square_mean line 85
  6. theorem OAI.Erdos3.LocalConvolution.exists_bohr_average_local_second_moment line 152
  7. theorem OAI.Erdos3.Peeling.exists_admissible_shape_selection line 188
  8. theorem OAI.Erdos3.Peeling.admissible_shape_translation_control line 207
  9. theorem OAI.Erdos3.CellRefinement.exists_bohr_replacement_family line 232
  10. theorem OAI.Erdos3.LocalConvolution.exists_unbalanced_bohr_second_moment_at_scale line 287
  11. theorem OAI.Erdos3.LocalConvolution.exists_unbalanced_bohr_second_moment line 359
  12. theorem OAI.Erdos3.CellRefinement.bohr_peeling_parent_bound line 407
  13. theorem OAI.Erdos3.CellRefinement.bohr_parent_bound_from_capped line 439
  14. def OAI.Erdos3.LocalConvolution.unbalancedRankExtra line 510
  15. def OAI.Erdos3.LocalConvolution.unbalancedMinimumWidth line 513
  16. theorem OAI.Erdos3.LocalConvolution.unbalancedMinimumWidth_pos line 519
  17. theorem OAI.Erdos3.LocalConvolution.exists_unbalanced_admissible_shape line 536