OAI/Combinatorics/Progressions/Estimates/ResidualErrorAllocation.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.inv_min_le_of_inv_le line 10
  2. theorem OAI.Erdos3.one_add_le_exp_succ line 16
  3. theorem OAI.Erdos3.NativeModelingNumerics.mul_exp_le_exp line 33
  4. theorem OAI.Erdos3.NativeModelingNumerics.exp_ratio_le line 40
  5. theorem OAI.Erdos3.NativeModelingNumerics.exp_threshold_le line 50
  6. theorem OAI.Erdos3.NativeModelingNumerics.sequential_thresholds line 60
  7. theorem OAI.Erdos3.NativeModelingNumerics.coefficient_bound line 80
  8. theorem OAI.Erdos3.NativeModelingNumerics.one_add_mul_exp_bound line 84
  9. theorem OAI.Erdos3.NativeModelingNumerics.first_length_bound line 93
  10. theorem OAI.Erdos3.NativeModelingNumerics.second_length_bound line 109
  11. theorem OAI.Erdos3.NativeModelingNumerics.length_product_bound line 125
  12. def OAI.Erdos3.regularizationRadius line 148
  13. theorem OAI.Erdos3.regularizationRadius_spec line 150
  14. theorem OAI.Erdos3.regularizationRadius_inverse_le_exp line 159
  15. theorem OAI.Erdos3.regularizationRadius_log_inverse_le line 173
  16. def OAI.Erdos3.twoTermErrorResolution line 188
  17. def OAI.Erdos3.twoTermErrorWidth line 190
  18. theorem OAI.Erdos3.twoTermErrorChoices_spec line 192
  19. theorem OAI.Erdos3.twoTermErrorChoices_log_bounds line 221
  20. theorem OAI.Erdos3.translated_shift_error_bound line 256
  21. def OAI.Erdos3.replacementAccuracy line 301
  22. theorem OAI.Erdos3.replacementAccuracy_spec line 303
  23. theorem OAI.Erdos3.replacementAccuracy_cost line 315
  24. theorem OAI.Erdos3.replacementAccuracy_inverse_le_exp line 319
  25. def OAI.Erdos3.replacementScaleThreshold line 344
  26. theorem OAI.Erdos3.replacementScaleThreshold_conditions line 347
  27. theorem OAI.Erdos3.replacementScaleThreshold_le_exp line 398
  28. def OAI.Erdos3.residualPointAccuracy line 435
  29. def OAI.Erdos3.residualGridAccuracy line 438
  30. def OAI.Erdos3.residualMeanAccuracy line 441
  31. theorem OAI.Erdos3.residualPointAccuracy_spec line 444
  32. theorem OAI.Erdos3.residualGridAccuracy_spec line 455
  33. theorem OAI.Erdos3.residualMeanAccuracy_spec line 461
  34. theorem OAI.Erdos3.residual_three_term_budget line 476