OAI/Combinatorics/Progressions/Lattices/AffinePrecisionBudget.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.normalized_adaptive_affine_comparison line 12
  2. theorem OAI.Erdos3.normalized_affine_error_le line 151
  3. theorem OAI.Erdos3.affine_error_envelope_at_precision line 196
  4. def OAI.Erdos3.affineStabilityInputBudget line 215
  5. theorem OAI.Erdos3.affineStabilityInputBudget_bounds line 220
  6. theorem OAI.Erdos3.affineStabilityInputBudget_mask line 235
  7. def OAI.Erdos3.affineReferenceTargetTime line 251
  8. def OAI.Erdos3.affineReferenceTargetShell line 254
  9. theorem OAI.Erdos3.affineReferenceTargetTime_nonneg line 257
  10. theorem OAI.Erdos3.affineReferenceTargetShell_pos line 263
  11. theorem OAI.Erdos3.affine_error_envelope_le_precision line 268
  12. theorem OAI.Erdos3.affine_error_envelope_lt_target line 278