OAI/Combinatorics/Progressions/Estimates/SmoothSublevelCutoff.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_smooth_scalar_cutoff line 13
  2. theorem OAI.Erdos3.exists_smooth_sublevel_cutoff line 40
  3. def OAI.Erdos3.sublevelCutoff line 65
  4. theorem OAI.Erdos3.sublevelCutoff_range line 68
  5. theorem OAI.Erdos3.sublevelCutoff_eq_zero line 72
  6. theorem OAI.Erdos3.sublevelCutoff_eq_one line 79
  7. theorem OAI.Erdos3.sublevelCutoff_tsupport_subset line 86
  8. theorem OAI.Erdos3.contDiff_sublevelCutoff line 96
  9. theorem OAI.Erdos3.sublevelCutoff_fderiv_norm_le line 101