ResourcePrices.lean

1 import MachineTheory.Planning
2 import Mathlib.Analysis.Convex.Hull
3 
4 /-! # Resource prices and their declared uncertainty set
5 
6 Core 7.3. Event coordinates use old-minus-new signs. A price is a linear conversion
7 of named additive events, not a hardware timing law. The convex hull below is
8 Mathlib's actual `convexHull`, not an assumed collection of convenient test prices.
9 -/
10 namespace Komorebi.MachineTheory.ResourcePrices
11 open scoped BigOperators
12 noncomputable section
13 variable {E : Type*} [Fintype E]
14 
15 /-- Positive saving means that the old route consumes more priced events. -/
16 def saving (delta w : E → ℝ) : ℝ := ∑ i, w i * delta i
17 
18 @[simp] theorem saving_zero_price (delta : E → ℝ) : saving delta 0 = 0 := by
19   simp [saving]
20 
21 @[simp] theorem saving_zero_events (w : E → ℝ) : saving 0 w = 0 := by
22   simp [saving]
23 
24 theorem saving_price_add (delta w z : E → ℝ) :
25     saving delta (w+z) = saving delta w + saving delta z := by
26   simp only [saving,Pi.add_apply,add_mul,Finset.sum_add_distrib]
27 
28 theorem saving_price_smul (delta w : E → ℝ) (a : ℝ) :
29     saving delta (a • w) = a * saving delta w := by
30   simp only [saving,Pi.smul_apply,smul_eq_mul,mul_assoc,Finset.mul_sum]
31 
32 theorem saving_event_add (a b w : E → ℝ) :
33     saving (a+b) w = saving a w + saving b w := by
34   simp only [saving,Pi.add_apply,mul_add,Finset.sum_add_distrib]
35 
36 theorem saving_event_sub (a b w : E → ℝ) :
37     saving (a-b) w = saving a w - saving b w := by
38   simp only [saving,Pi.sub_apply,mul_sub,Finset.sum_sub_distrib]
39 
40 theorem saving_event_smul (delta w : E → ℝ) (a : ℝ) :
41     saving (a • delta) w = a * saving delta w := by
42   unfold saving
43   simp only [Pi.smul_apply,smul_eq_mul,Finset.mul_sum]
44   apply Finset.sum_congr rfl
45   intro i _
46   ring
47 
48 /-- Core 7.3, first equivalence. Coordinate prices can expose any negative saving. -/
49 theorem all_nonnegative_prices_iff (delta : E → ℝ) :
50     (∀ w : E → ℝ, (∀ i, 0 ≤ w i) → 0 ≤ saving delta w) ↔ ∀ i, 0 ≤ delta i := by
51   classical
52   constructor
53   · intro h i
54     have hh := h (fun j => if j=i then 1 else 0) (by intro j; split <;> norm_num)
55     simpa [saving] using hh
56   · intro h w hw
57     exact Finset.sum_nonneg (fun i _ => mul_nonneg (hw i) (h i))
58 
59 /-- A negative coordinate gives an explicit nonnegative counter-price. -/
60 theorem adverse_price_of_negative (delta : E → ℝ) (i : E) (hi : delta i < 0) :
61     ∃ w : E → ℝ, (∀ j, 0 ≤ w j) ∧ saving delta w < 0 := by
62   classical
63   refine ⟨fun j => if j=i then 1 else 0, ?_, ?_⟩
64   · intro j; dsimp; split <;> norm_num
65   · simpa [saving] using hi
66 
67 /-- The zero price excludes strict improvement at every nonnegative price. -/
68 theorem not_strict_at_all_nonnegative_prices (delta : E → ℝ) :
69     ¬ ∀ w : E → ℝ, (∀ i, 0 ≤ w i) → 0 < saving delta w := by
70   intro h
71   have hz := h 0 (by intro i; exact le_rfl)
72   simp at hz
73 
74 /-- Linear lower-value sets are convex; no continuity or compactness is needed. -/
75 theorem lower_halfspace_convex (delta : E → ℝ) (b : ℝ) :
76     Convex ℝ {w : E → ℝ | b ≤ saving delta w} := by
77   intro x hx y hy a c ha hc hac
78   change b ≤ saving delta (a • x + c • y)
79   rw [saving_price_add,saving_price_smul,saving_price_smul]
80   calc
81     b = a*b+c*b := by rw [← add_mul,hac,one_mul]
82     _ ≤ a*saving delta x+c*saving delta y :=
83       add_le_add (mul_le_mul_of_nonneg_left hx ha) (mul_le_mul_of_nonneg_left hy hc)
84 
85 /-- Testing every generator is equivalent to the same bound on its entire convex hull. -/
86 theorem hull_lower_bound_iff (delta : E → ℝ) (W : Set (E → ℝ)) (b : ℝ) :
87     (∀ w ∈ convexHull ℝ W, b ≤ saving delta w) ↔ ∀ w ∈ W, b ≤ saving delta w := by
88   constructor
89   · intro h w hw
90     exact h w (subset_convexHull ℝ W hw)
91   · intro h
92     exact convexHull_min h (lower_halfspace_convex delta b)
93 
94 /-- Core 7.3, second conclusion: the finite minimum is the actual minimum on the hull. -/
95 theorem finite_price_minimum (delta : E → ℝ) (W : Finset (E → ℝ)) (hne : W.Nonempty) :
96     ∃ w ∈ W, saving delta w = Planning.finiteMin W hne (saving delta) ∧
97       IsLeast ((saving delta) '' convexHull ℝ (W : Set (E → ℝ)))
98         (Planning.finiteMin W hne (saving delta)) := by
99   obtain ⟨w,hw,hmin⟩ := Planning.finiteMin_attained W hne (saving delta)
100   refine ⟨w,hw,hmin,?_,?_⟩
101   · exact ⟨w,subset_convexHull ℝ (W : Set (E → ℝ)) hw,hmin⟩
102   · rintro r ⟨z,hz,rfl⟩
103     apply (hull_lower_bound_iff delta (W : Set (E → ℝ)) _).mpr ?_ z hz
104     intro v hv
105     exact Planning.finiteMin_le W hne (saving delta) v hv
106 
107 /-- The listed minimum is attained, rather than a mere infimum outside the price set. -/
108 theorem listed_hull_minimizer (delta : E → ℝ) (W : Finset (E → ℝ)) (hne : W.Nonempty) :
109     ∃ w ∈ W, w ∈ convexHull ℝ (W : Set (E → ℝ)) ∧
110       ∀ z ∈ convexHull ℝ (W : Set (E → ℝ)), saving delta w ≤ saving delta z := by
111   obtain ⟨w,hw,he,hmin⟩ := finite_price_minimum delta W hne
112   refine ⟨w,hw,subset_convexHull ℝ (W : Set (E → ℝ)) hw,?_⟩
113   intro z hz
114   rw [he]
115   exact hmin.2 ⟨z,hz,rfl⟩
116 
117 /-- Changing the units requires compensating prices, not keeping their numbers fixed. -/
118 theorem consistent_unit_change (delta w units : E → ℝ) (hu : ∀ i, units i ≠ 0) :
119     saving (fun i => units i * delta i) (fun i => w i / units i) = saving delta w := by
120   unfold saving
121   apply Finset.sum_congr rfl
122   intro i _
123   field_simp [hu i]
124 
125 omit [Fintype E] in
126 theorem rescaled_price_nonnegative (w units : E → ℝ)
127     (hw : ∀ i, 0 ≤ w i) (hu : ∀ i, 0 < units i) :
128     ∀ i, 0 ≤ w i / units i := fun i => div_nonneg (hw i) (le_of_lt (hu i))
129 
130 end
131 end Komorebi.MachineTheory.ResourcePrices

Back to source controls