OAI/Combinatorics/Progressions/Estimates/IndependentReturnScale.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.localizedAverageScale_mono_error line 11
  2. theorem OAI.Erdos3.localizedAverageScale_exp_lower_of_error line 18
  3. def OAI.Erdos3.CellRefinement.outerMatchingScale line 35
  4. theorem OAI.Erdos3.CellRefinement.outerMatchingScale_spec line 38
  5. def OAI.Erdos3.CellRefinement.outerMatchingScaleLoss line 46
  6. theorem OAI.Erdos3.CellRefinement.outerMatchingScaleLoss_nonneg line 49
  7. theorem OAI.Erdos3.CellRefinement.outerMatchingScale_exp_lower line 55
  8. def OAI.Erdos3.LocalConvolution.controlledLocalMomentScale line 93
  9. def OAI.Erdos3.LocalConvolution.localMomentErrorBudget line 96
  10. theorem OAI.Erdos3.LocalConvolution.controlledLocalMomentScale_spec line 99
  11. theorem OAI.Erdos3.LocalConvolution.localMomentErrorBudget_spec line 120
  12. theorem OAI.Erdos3.LocalConvolution.controlledLocalMomentScale_exp_lower line 133
  13. theorem OAI.Erdos3.LocalConvolution.normalized_local_alternatives_at_scale line 166
  14. def OAI.Erdos3.CellRefinement.independentReturnScale line 211
  15. theorem OAI.Erdos3.CellRefinement.independentReturnScale_spec line 214
  16. theorem OAI.Erdos3.CellRefinement.independentReturnScale_exp_lower line 242
  17. theorem OAI.Erdos3.CellRefinement.bohr_matched_independent_at_return_scale line 263