OAI/Combinatorics/Progressions/Estimates/MatchedFlatDecay.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.flatComparisonDelta line 10
  2. theorem OAI.Erdos3.flatComparisonDelta_spec line 12
  3. theorem OAI.Erdos3.exp_mul_half_pow_le line 25
  4. theorem OAI.Erdos3.flat_exception_error_le line 35
  5. theorem OAI.Erdos3.exists_flat_moment_slope line 59
  6. theorem OAI.Erdos3.exp_extra_decay_le_half line 95
  7. theorem OAI.Erdos3.flat_total_error_le_exp line 105
  8. theorem OAI.Erdos3.LocalConvolution.unbalanced_error_control line 126
  9. theorem OAI.Erdos3.LocalConvolution.exists_unbalanced_moment_threshold line 137
  10. theorem OAI.Erdos3.exists_joint_moment_orders line 155
  11. theorem OAI.Erdos3.CellRefinement.matched_flat_integral_decay line 206