BudgetConvolution.lean

1 module
2 public import Mathlib.Algebra.Order.Field.Basic
3 public import Mathlib.Algebra.Order.BigOperators.Group.Finset
4 public import Mathlib.Data.Fin.Tuple.Basic
5 public import Mathlib.Data.List.OfFn
6 public import Mathlib.Tactic
7 
8 /-!
9 Author: Komorebi P.
10 Exact min-plus dynamic programming with explicit infeasible states.
11 `none` denotes infeasible, never zero cost and never a finite sentinel.
12 All optima are proved attained, not only lower bounds on attainable costs.
13 -/
14 public section
15 set_option autoImplicit false
16 namespace KomorebiPaperVIII
17 namespace BudgetDP
18 open scoped BigOperators
19 variable {R : Type*} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
20 
21 /-- Semantics of a table entry, relative to an independently defined feasible set. -/
22 def IsMinimum (o : Option R) (S : R → Prop) : Prop :=
23   match o with
24   | none => ∀ z, ¬ S z
25   | some v => S v ∧ ∀ z, S z → v ≤ z
26 
27 /-- Infeasible options are ignored. Ties choose the left entry. -/
28 def choose (x y : Option R) : Option R :=
29   match x, y with
30   | none, y => y
31   | x, none => x
32   | some a, some b => if a ≤ b then some a else some b
33 
34 /-- Independent feasible components add; infeasibility is absorbing. -/
35 def add (x y : Option R) : Option R :=
36   match x, y with
37   | some a, some b => some (a + b)
38   | _, _ => none
39 
40 /-- A finite minimum is computed, not postulated. -/
41 def bestOver {ι : Type*} (f : ι → Option R) : List ι → Option R
42   | [] => none
43   | x :: xs => choose (f x) (bestOver f xs)
44 
45 /-- Min-plus convolution splits the exact error weight in every possible way. -/
46 def convolution (F G : ℕ → Option R) (b : ℕ) : Option R :=
47   bestOver (fun k => add (F k) (G (b - k))) (List.range (b + 1))
48 
49 omit [Field R] [IsStrictOrderedRing R] in
50 theorem minimum_congr {o : Option R} {S T : R → Prop}
51     (h : IsMinimum o S) (he : ∀ z, S z ↔ T z) : IsMinimum o T := by
52   cases o with
53   | none => exact fun z hz => h z ((he z).mpr hz)
54   | some v => exact ⟨(he v).mp h.1, fun z hz => h.2 z ((he z).mpr hz)⟩
55 
56 omit [Field R] [IsStrictOrderedRing R] in
57 theorem choose_correct (x y : Option R) (S T : R → Prop)
58     (hx : IsMinimum x S) (hy : IsMinimum y T) :
59     IsMinimum (choose x y) (fun z => S z ∨ T z) := by
60   cases x with
61   | none =>
62     cases y with
63     | none => exact fun z hz => hz.elim (hx z) (hy z)
64     | some b =>
65       exact ⟨Or.inr hy.1, fun z hz => hz.elim (fun h => False.elim (hx z h)) (hy.2 z)⟩
66   | some a =>
67     cases y with
68     | none =>
69       exact ⟨Or.inl hx.1, fun z hz => hz.elim (hx.2 z) (fun h => False.elim (hy z h))⟩
70     | some b =>
71       by_cases hab : a ≤ b
72       · simp only [choose, hab, ↓reduceIte]
73         exact ⟨Or.inl hx.1, fun z hz => hz.elim (hx.2 z) (fun h => hab.trans (hy.2 z h))⟩
74       · simp only [choose, hab, ↓reduceIte]
75         exact ⟨Or.inr hy.1, fun z hz => hz.elim
76           (fun h => (le_of_not_ge hab).trans (hx.2 z h)) (hy.2 z)⟩
77 
78 theorem add_correct (x y : Option R) (S T : R → Prop)
79     (hx : IsMinimum x S) (hy : IsMinimum y T) :
80     IsMinimum (add x y) (fun z => ∃ u v, S u ∧ T v ∧ z = u + v) := by
81   cases x with
82   | none =>
83     cases y <;> intro z hz
84     all_goals obtain ⟨u, v, hu, hv, he⟩ := hz; exact hx u hu
85   | some a =>
86     cases y with
87     | none =>
88       intro z hz
89       obtain ⟨u, v, hu, hv, he⟩ := hz
90       exact hy v hv
91     | some b =>
92       refine ⟨⟨a, b, hx.1, hy.1, rfl⟩, ?_⟩
93       intro z hz
94       obtain ⟨u, v, hu, hv, rfl⟩ := hz
95       exact add_le_add (hx.2 u hu) (hy.2 v hv)
96 
97 omit [Field R] [IsStrictOrderedRing R] in
98 theorem bestOver_correct {ι : Type*} (xs : List ι) (f : ι → Option R)
99     (S : ι → R → Prop) (h : ∀ i ∈ xs, IsMinimum (f i) (S i)) :
100     IsMinimum (bestOver f xs) (fun z => ∃ i ∈ xs, S i z) := by
101   induction xs with
102   | nil => simp [bestOver, IsMinimum]
103   | cons i xs ih =>
104     have hc := choose_correct (f i) (bestOver f xs) (S i)
105       (fun z => ∃ j ∈ xs, S j z) (h i (by simp))
106       (ih (fun j hj => h j (by simp [hj])))
107     apply minimum_congr hc
108     intro z
109     simp
110 
111 /-- Every feasible split is represented, and the returned finite value is attained. -/
112 theorem convolution_correct (F G : ℕ → Option R) (S T : ℕ → R → Prop)
113     (hF : ∀ b, IsMinimum (F b) (S b)) (hG : ∀ b, IsMinimum (G b) (T b)) (b : ℕ) :
114     IsMinimum (convolution F G b)
115       (fun z => ∃ k l u v, k + l = b ∧ S k u ∧ T l v ∧ z = u + v) := by
116   have h := bestOver_correct (List.range (b + 1))
117     (fun k => add (F k) (G (b - k)))
118     (fun k z => ∃ u v, S k u ∧ T (b - k) v ∧ z = u + v)
119     (fun k _ => add_correct (F k) (G (b - k)) (S k) (T (b - k)) (hF k) (hG (b - k)))
120   apply minimum_congr h
121   intro z
122   constructor
123   · rintro ⟨k, hk, u, v, hu, hv, hz⟩
124     have hk' : k < b + 1 := List.mem_range.mp hk
125     exact ⟨k, b - k, u, v, by omega, hu, hv, hz⟩
126   · rintro ⟨k, l, u, v, hkl, hu, hv, hz⟩
127     have hk : k < b + 1 := by omega
128     have hl : b - k = l := by omega
129     exact ⟨k, List.mem_range.mpr hk, u, v, hu, hl ▸ hv, hz⟩
130 
131 /-- A singleton feasible cost, at exactly its declared weight. -/
132 def singletonTable (w : ℕ) (c : R) (b : ℕ) : Option R :=
133   if b = w then some c else none
134 
135 omit [Field R] [IsStrictOrderedRing R] in
136 theorem singletonTable_correct (w : ℕ) (c : R) (b : ℕ) :
137     IsMinimum (singletonTable w c b) (fun z => b = w ∧ z = c) := by
138   by_cases h : b = w
139   · simp [singletonTable, h, IsMinimum]
140   · simp [singletonTable, h, IsMinimum]
141 
142 /-- Min-plus combination for arbitrary finite branching, including no children. -/
143 def combine : {n : ℕ} → (Fin n → ℕ → Option R) → ℕ → Option R
144   | 0, _ => singletonTable 0 0
145   | n + 1, F => convolution (F 0) (combine (fun i : Fin n => F i.succ))
146 
147 /-- The result is the minimum over all independently chosen component weights and costs. -/
148 theorem combine_correct {n : ℕ} (F : Fin n → ℕ → Option R)
149     (S : Fin n → ℕ → R → Prop) (hF : ∀ i b, IsMinimum (F i b) (S i b)) (b : ℕ) :
150     IsMinimum (combine F b)
151       (fun z => ∃ w : Fin n → ℕ, ∃ c : Fin n → R,
152         (∀ i, S i (w i) (c i)) ∧ (∑ i, w i) = b ∧ (∑ i, c i) = z) := by
153   induction n generalizing b with
154   | zero =>
155     apply minimum_congr (singletonTable_correct 0 (0 : R) b)
156     intro z
157     simp [eq_comm]
158   | succ n ih =>
159     have h := convolution_correct (F 0) (combine (fun i : Fin n => F i.succ))
160       (S 0)
161       (fun l v => ∃ w : Fin n → ℕ, ∃ c : Fin n → R,
162         (∀ i, S i.succ (w i) (c i)) ∧ (∑ i, w i) = l ∧ (∑ i, c i) = v)
163       (hF 0) (fun l => ih (fun i => F i.succ) (fun i => S i.succ) (fun i => hF i.succ) l) b
164     apply minimum_congr h
165     intro z
166     constructor
167     · rintro ⟨k, l, u, v, hkl, hu, ⟨w, c, hc, hw, hv⟩, hz⟩
168       refine ⟨Fin.cons k w, Fin.cons u c, ?_, ?_, ?_⟩
169       · intro i
170         refine Fin.cases ?_ (fun j => ?_) i
171         · exact hu
172         · exact hc j
173       · simp only [Fin.sum_univ_succ, Fin.cons_zero, Fin.cons_succ, hw]
174         exact hkl
175       · simp only [Fin.sum_univ_succ, Fin.cons_zero, Fin.cons_succ, hv]
176         exact hz.symm
177     · rintro ⟨w, c, hc, hw, hz⟩
178       refine ⟨w 0, ∑ i : Fin n, w i.succ, c 0, ∑ i : Fin n, c i.succ,
179         ?_, hc 0, ⟨fun i => w i.succ, fun i => c i.succ, fun i => hc i.succ, rfl, rfl⟩, ?_⟩
180       · simpa only [Fin.sum_univ_succ] using hw
181       · simpa only [Fin.sum_univ_succ] using hz.symm
182 
183 /-- Return the best feasible exact-weight entry up to a budget. -/
184 def withinBudget (F : ℕ → Option R) (B : ℕ) : Option R :=
185   bestOver F (List.range (B + 1))
186 
187 omit [Field R] [IsStrictOrderedRing R] in
188 theorem withinBudget_correct (F : ℕ → Option R) (S : ℕ → R → Prop)
189     (hF : ∀ b, IsMinimum (F b) (S b)) (B : ℕ) :
190     IsMinimum (withinBudget F B) (fun z => ∃ b, b ≤ B ∧ S b z) := by
191   apply minimum_congr (bestOver_correct (List.range (B + 1)) F S (fun b _ => hF b))
192   intro z
193   simp only [List.mem_range, Nat.lt_succ_iff]
194 
195 /- A finite answer contains an attaining feasible cost. -/
196 omit [Field R] [IsStrictOrderedRing R] in
197 theorem minimum_some_iff (F : Option R) (S : R → Prop) (h : IsMinimum F S) (c : R) :
198     F = some c ↔ S c ∧ ∀ z, S z → c ≤ z := by
199   constructor
200   · intro hf; subst F; exact h
201   · intro hc
202     cases F with
203     | none => exact False.elim (h c hc.1)
204     | some v => have he : v = c := le_antisymm (h.2 c hc.1) (hc.2 v h.1); simp [he]
205 
206 /- The sentinel is returned exactly when the feasible set is empty. -/
207 omit [Field R] [IsStrictOrderedRing R] in
208 theorem minimum_none_iff (F : Option R) (S : R → Prop) (h : IsMinimum F S) :
209     F = none ↔ ¬ ∃ z, S z := by
210   cases F with
211   | none => exact ⟨fun _ ⟨z, hz⟩ => h z hz, fun _ => rfl⟩
212   | some v => simp only [Option.some_ne_none, false_iff, not_not]; exact ⟨v, h.1⟩
213 end BudgetDP
214 end KomorebiPaperVIII
215 
216 #print axioms KomorebiPaperVIII.BudgetDP.minimum_congr
217 #print axioms KomorebiPaperVIII.BudgetDP.choose_correct
218 #print axioms KomorebiPaperVIII.BudgetDP.add_correct
219 #print axioms KomorebiPaperVIII.BudgetDP.bestOver_correct
220 #print axioms KomorebiPaperVIII.BudgetDP.convolution_correct
221 #print axioms KomorebiPaperVIII.BudgetDP.singletonTable_correct
222 #print axioms KomorebiPaperVIII.BudgetDP.combine_correct
223 #print axioms KomorebiPaperVIII.BudgetDP.withinBudget_correct
224 #print axioms KomorebiPaperVIII.BudgetDP.minimum_some_iff
225 #print axioms KomorebiPaperVIII.BudgetDP.minimum_none_iff

Back to source controls