OAI/Combinatorics/UniformKServer/TreeCoverage.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The allocation serves every request and is dominated by true posterior counts. Positive parks therefore have validity witnesses; no impossible history is used in either conclusion.

  1. def OAI.UniformKServer.TreeCoverage.mean line 18
  2. theorem OAI.UniformKServer.TreeCoverage.mean_nonneg line 21
  3. theorem OAI.UniformKServer.TreeCoverage.child_size_bound line 24
  4. theorem OAI.UniformKServer.TreeCoverage.nonroot_domination line 32
  5. theorem OAI.UniformKServer.TreeCoverage.root_mean line 44
  6. theorem OAI.UniformKServer.TreeCoverage.domination line 52
  7. theorem OAI.UniformKServer.TreeCoverage.required line 60
  8. theorem OAI.UniformKServer.TreeCoverage.positive_witness line 67
  9. theorem OAI.UniformKServer.TreeCoverage.allocation_witness line 81