OAI/Combinatorics/Progressions/Estimates/SmallWeightedPhysicalReplacement.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.weightedReplacementTolerance line 11
  2. theorem OAI.Erdos3.weightedReplacementTolerance_pos line 14
  3. theorem OAI.Erdos3.weightedReplacementTolerance_bound line 19
  4. theorem OAI.Erdos3.cutoff_weighted_replacement_bound line 40
  5. theorem OAI.Erdos3.weightedReplacementTolerance_inverse_le_exp line 65
  6. theorem OAI.Erdos3.replacementWindowFactor_le_exp line 88
  7. theorem OAI.Erdos3.replacementSampledEnergy_le_exp line 98
  8. def OAI.Erdos3.physicalReplacementInputLog line 108
  9. theorem OAI.Erdos3.physicalReplacementInputLog_nonneg line 111
  10. theorem OAI.Erdos3.physicalReplacementTolerance_inverse_le_exp line 116
  11. theorem OAI.Erdos3.normalized_physical_residual_sum_energy line 147
  12. def OAI.Erdos3.physicalMeanAccuracyLog line 186
  13. theorem OAI.Erdos3.physicalMeanAccuracyLog_spec line 190
  14. def OAI.Erdos3.physicalReplacementScaleThreshold line 203
  15. theorem OAI.Erdos3.physicalReplacementScaleThreshold_conditions line 210
  16. theorem OAI.Erdos3.smoothPairCoefficientScale_large line 227
  17. theorem OAI.Erdos3.weighted_physical_replacement line 246
  18. theorem OAI.Erdos3.physicalMeanAccuracyLog_le line 322
  19. def OAI.Erdos3.physicalReplacementThresholdLog line 334
  20. theorem OAI.Erdos3.physicalReplacementThresholdLog_bounds line 338
  21. theorem OAI.Erdos3.physicalReplacementScaleThreshold_le_exp line 355
  22. theorem OAI.Erdos3.allocated_weighted_physical_replacement line 403
  23. theorem OAI.Erdos3.small_weighted_physical_replacement line 507