OAI/Combinatorics/UniformKServer/ParentScale.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Parent H is an actual persistent relative reference of the clipped sum of persistent size trackers, not an oracle for the true size.

  1. def OAI.UniformKServer.ParentScale.trueX line 17
  2. def OAI.UniformKServer.ParentScale.estimateX line 20
  3. def OAI.UniformKServer.ParentScale.reference line 23
  4. def OAI.UniformKServer.ParentScale.lowerX line 26
  5. theorem OAI.UniformKServer.ParentScale.estimate_comparison line 29
  6. theorem OAI.UniformKServer.ParentScale.reference_comparison line 45
  7. theorem OAI.UniformKServer.ParentScale.lower_bounds line 60
  8. theorem OAI.UniformKServer.ParentScale.true_positive line 75
  9. theorem OAI.UniformKServer.ParentScale.lower_positive line 78
  10. theorem OAI.UniformKServer.ParentScale.estimate_change line 81
  11. theorem OAI.UniformKServer.ParentScale.reference_charge line 100