OAI/Combinatorics/Progressions/Estimates/RawSourceTolerance.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.coefficient_array_joint_comparison line 15
  2. theorem OAI.Erdos3.coefficient_array_fiber_comparison line 101
  3. theorem OAI.Erdos3.random_coefficient_array_joint_comparison line 179
  4. def OAI.Erdos3.booleanRegularizationRadius line 256
  5. def OAI.Erdos3.booleanToleranceMinor line 263
  6. def OAI.Erdos3.booleanToleranceBoundary line 268
  7. def OAI.Erdos3.booleanToleranceC2 line 273
  8. def OAI.Erdos3.booleanToleranceDivergence line 280
  9. def OAI.Erdos3.booleanPerturbationScale line 290
  10. theorem OAI.Erdos3.booleanToleranceMinor_pos line 310
  11. theorem OAI.Erdos3.booleanToleranceBoundary_pos line 317
  12. theorem OAI.Erdos3.booleanToleranceC2_nonneg line 323
  13. theorem OAI.Erdos3.booleanToleranceDivergence_nonneg line 330
  14. theorem OAI.Erdos3.booleanRegularizationRadius_inverse_le_exp line 343
  15. theorem OAI.Erdos3.booleanPerturbationScale_inverse_le_exp line 354
  16. theorem OAI.Erdos3.exists_random_coefficient_array_tolerance_with_scale line 384
  17. theorem OAI.Erdos3.exists_random_coefficient_array_tolerance line 458
  18. theorem OAI.Erdos3.exists_uniform_boolean_regularization_with_radius line 507
  19. theorem OAI.Erdos3.exists_uniform_boolean_regularization line 559
  20. theorem OAI.Erdos3.exists_canonical_raw_sampler_tolerance_with_scale line 594
  21. theorem OAI.Erdos3.exists_canonical_raw_sampler_tolerance line 645
  22. theorem OAI.Erdos3.exists_random_coefficient_smaller_tolerance_with_scale line 698
  23. theorem OAI.Erdos3.exists_raw_source_tolerance_with_scale line 767
  24. theorem OAI.Erdos3.exists_raw_source_tolerance line 820