WorkloadPricing.lean

1 import MachineTheory.ResourcePrices
2 import Mathlib.Tactic.Linarith
3 
4 /-! # Preparation and repeated workloads
5 
6 The ledger is a difference of actual nonnegative counters, formed only after
7 embedding them in the signed real-valued event space. Workload counts are fixed
8 natural numbers. This account does not silently include memory peaks or wall time.
9 -/
10 namespace Komorebi.MachineTheory.ResourcePrices
11 open scoped BigOperators
12 noncomputable section
13 variable {E : Type*} [Fintype E]
14 
15 /-- Per-use savings may be negative in some coordinates. -/
16 def net {J : Type*} [Fintype J] (setup : E → ℝ) (uses : J → ℕ)
17     (perUse : J → E → ℝ) : E → ℝ :=
18   fun i => (∑ j, (uses j : ℝ) * perUse j i) - setup i
19 
20 /-- Full old and new ledgers, including the incremental preparation charge. -/
21 structure Ledger (J E : Type*) where
22   setup : E → ℕ
23   uses : J → ℕ
24   old : J → E → ℕ
25   revised : J → E → ℕ
26 
27 def Ledger.oldTotal {J : Type*} [Fintype J] (L : Ledger J E) (i : E) : ℕ :=
28   ∑ j, L.uses j * L.old j i
29 
30 def Ledger.newTotal {J : Type*} [Fintype J] (L : Ledger J E) (i : E) : ℕ :=
31   L.setup i + ∑ j, L.uses j * L.revised j i
32 
33 def Ledger.delta {J : Type*} [Fintype J] (L : Ledger J E) : E → ℝ :=
34   net (fun i => L.setup i) L.uses (fun j i => (L.old j i : ℝ) - L.revised j i)
35 
36 omit [Fintype E] in
37 /-- The signed net equals old total minus revised total, not natural subtraction. -/
38 theorem Ledger.delta_eq_total_difference {J : Type*} [Fintype J] (L : Ledger J E) (i : E) :
39     L.delta i = (L.oldTotal i : ℝ) - (L.newTotal i : ℝ) := by
40   simp only [Ledger.delta,net,Ledger.oldTotal,Ledger.newTotal,Nat.cast_sum,Nat.cast_add,
41     Nat.cast_mul,mul_sub,Finset.sum_sub_distrib]
42   ring
43 
44 /-- Valuation commutes with aggregation of the entire declared workload. -/
45 theorem saving_net {J : Type*} [Fintype J] (setup : E → ℝ) (uses : J → ℕ)
46     (perUse : J → E → ℝ) (w : E → ℝ) :
47     saving (net setup uses perUse) w =
48       (∑ j, (uses j : ℝ) * saving (perUse j) w) - saving setup w := by
49   simp only [saving,net,mul_sub,Finset.sum_sub_distrib,Finset.mul_sum]
50   rw [Finset.sum_comm]
51   congr 1
52   apply Finset.sum_congr rfl
53   intro j _
54   apply Finset.sum_congr rfl
55   intro i _
56   ring
57 
58 /-- One actual old/revised ledger supports the price comparison. -/
59 theorem Ledger.saving_eq_cost_difference {J : Type*} [Fintype J] (L : Ledger J E) (w : E → ℝ) :
60     saving L.delta w = saving (fun i => (L.oldTotal i : ℝ)) w -
61       saving (fun i => (L.newTotal i : ℝ)) w := by
62   have he : L.delta = (fun i => (L.oldTotal i : ℝ)) - (fun i => (L.newTotal i : ℝ)) := by
63     funext i
64     exact L.delta_eq_total_difference i
65   rw [he,saving_event_sub]
66 
67 /-- Source formula, including setup, with the all-price quantifier unchanged. -/
68 theorem workload_robust_iff {J : Type*} [Fintype J] (setup : E → ℝ) (uses : J → ℕ)
69     (perUse : J → E → ℝ) :
70     (∀ w : E → ℝ, (∀ i, 0 ≤ w i) → 0 ≤ saving (net setup uses perUse) w) ↔
71       ∀ i, setup i ≤ ∑ j, (uses j : ℝ) * perUse j i := by
72   rw [all_nonnegative_prices_iff]
73   simp only [net,sub_nonneg]
74 
75 /-- A change in an event unit must not silently change the associated price. -/
76 theorem saving_mono (a b w : E → ℝ) (hw : ∀ i, 0 ≤ w i) (hab : ∀ i, a i ≤ b i) :
77     saving a w ≤ saving b w :=
78   Finset.sum_le_sum (fun i _ => mul_le_mul_of_nonneg_left (hab i) (hw i))
79 
80 theorem preparation_is_not_free {J : Type*} [Fintype J] (K L : E → ℝ)
81     (uses : J → ℕ) (s : J → E → ℝ) (w : E → ℝ)
82     (hw : ∀ i, 0 ≤ w i) (hKL : ∀ i, K i ≤ L i) :
83     saving (net L uses s) w ≤ saving (net K uses s) w := by
84   rw [saving_net,saving_net]
85   exact sub_le_sub_left (saving_mono K L w hw hKL) _
86 
87 /-- Scalar reuse is evaluated only after the event coordinates have been priced. -/
88 def repeated (setup perUse : E → ℝ) (N : ℕ) : E → ℝ :=
89   fun i => (N : ℝ) * perUse i - setup i
90 
91 theorem saving_repeated (setup perUse w : E → ℝ) (N : ℕ) :
92     saving (repeated setup perUse N) w = (N : ℝ) * saving perUse w - saving setup w := by
93   change saving ((N : ℝ) • perUse - setup) w = _
94   rw [saving_event_sub,saving_event_smul]
95 
96 /-- Strict break-even boundary for a fixed workload and fixed additive prices. -/
97 theorem amortization_iff (setup perUse w : E → ℝ) (N : ℕ)
98     (hd : 0 < saving perUse w) :
99     0 < saving (repeated setup perUse N) w ↔ saving setup w / saving perUse w < (N : ℝ) := by
100   rw [saving_repeated,sub_pos,div_lt_iff₀ hd]
101 
102 /-- Repetition cannot repay nonnegative setup when per-use savings are nonpositive. -/
103 theorem no_amortization_of_nonpositive (setup perUse w : E → ℝ) (N : ℕ)
104     (hK : 0 ≤ saving setup w) (hd : saving perUse w ≤ 0) :
105     saving (repeated setup perUse N) w ≤ 0 := by
106   rw [saving_repeated]
107   have hm := mul_nonpos_of_nonneg_of_nonpos (Nat.cast_nonneg N : (0 : ℝ) ≤ N) hd
108   linarith
109 
110 /-- An interval guarantee on the already priced per-use and setup accounts composes. -/
111 theorem robust_repeated_lower (setup perUse w : E → ℝ) (N : ℕ) (d K : ℝ)
112     (hd : d ≤ saving perUse w) (hK : saving setup w ≤ K) :
113     (N : ℝ) * d - K ≤ saving (repeated setup perUse N) w := by
114   rw [saving_repeated]
115   exact sub_le_sub (mul_le_mul_of_nonneg_left hd (Nat.cast_nonneg N)) hK
116 
117 /-- Applying the finite-price theorem to the net ledger includes preparation automatically. -/
118 theorem workload_minimum {J : Type*} [Fintype J]
119     (setup : E → ℝ) (uses : J → ℕ) (perUse : J → E → ℝ)
120     (W : Finset (E → ℝ)) (hne : W.Nonempty) :
121     ∃ w ∈ W, IsLeast ((saving (net setup uses perUse)) '' convexHull ℝ (W : Set (E → ℝ)))
122       (saving (net setup uses perUse) w) := by
123   obtain ⟨w,hw,he,hmin⟩ := finite_price_minimum (net setup uses perUse) W hne
124   exact ⟨w,hw,he.symm ▸ hmin⟩
125 
126 end
127 end Komorebi.MachineTheory.ResourcePrices

Back to source controls