OAI/Combinatorics/UniformKServer/AllocationEpoch.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Source companion §03, cumulative-variation epochs. Variation credit is carried in one potential; a forced parent refresh discards unused credit, and never creates a fresh initialization allowance.

  1. structure OAI.UniformKServer.AllocationEpoch.State line 16
  2. def OAI.UniformKServer.AllocationEpoch.initial line 20
  3. def OAI.UniformKServer.AllocationEpoch.fires line 22
  4. def OAI.UniformKServer.AllocationEpoch.update line 25
  5. def OAI.UniformKServer.AllocationEpoch.valid line 29
  6. def OAI.UniformKServer.AllocationEpoch.charge line 32
  7. theorem OAI.UniformKServer.AllocationEpoch.initial_valid line 36
  8. theorem OAI.UniformKServer.AllocationEpoch.update_valid line 40
  9. theorem OAI.UniformKServer.AllocationEpoch.wholesale_bound line 56
  10. theorem OAI.UniformKServer.AllocationEpoch.credit_step line 67
  11. def OAI.UniformKServer.AllocationEpoch.schedule line 92
  12. theorem OAI.UniformKServer.AllocationEpoch.schedule_valid line 96
  13. theorem OAI.UniformKServer.AllocationEpoch.schedule_budget line 104
  14. theorem OAI.UniformKServer.AllocationEpoch.total_variation line 127

    Source documentation

    Actual held vectors supply the total-variation hypothesis without degree loss.

    theorem total_variation {ι : Type*} [Fintype ι] (a b : ι → ℝ) :
    |(∑ i, b i)-(∑ i, a i)| ≤ ∑ i, |b i-a i| := by
…