ExactTreeCompiler.lean

1 module
2 public import Mathlib.Algebra.Order.Field.Basic
3 public import Mathlib.Algebra.Order.BigOperators.Group.Finset
4 public import Mathlib.Algebra.BigOperators.Field
5 public import Mathlib.Tactic
6 
7 /-!
8 Author: Komorebi P.
9 Paper VIII 9.4--9.7 and 9.11: exact finite-branching tree compilation.
10 Prunings are an independent inductive type. The recurrence is proved both a
11 lower bound for every pruning and attained by the constructed pruning.
12 The ordered field parameter permits exact rational execution and real models.
13 -/
14 
15 public section
16 set_option autoImplicit false
17 set_option maxRecDepth 2048
18 namespace KomorebiPaperVIII
19 open scoped BigOperators
20 
21 inductive CandidateTree (α : Type*) where
22   | leaf (label : α)
23   | node (label : α) (arity : ℕ) (children : Fin (arity + 1) → CandidateTree α)
24 
25 namespace CandidateTree
26 variable {α : Type*}
27 
28 def root : CandidateTree α → α
29   | .leaf a => a
30   | .node a _ _ => a
31 
32 /-- A legal pruning either keeps a node or independently prunes every child. -/
33 inductive Cut : CandidateTree α → Type _ where
34   | keep (t : CandidateTree α) : Cut t
35   | split {a : α} {n : ℕ} {ts : Fin (n + 1) → CandidateTree α}
36       (cs : ∀ i, Cut (ts i)) : Cut (.node a n ts)
37 
38 variable {R : Type*} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
39 
40 /-- The independently defined additive objective of a legal pruning. -/
41 def cutValue (keep overhead : α → R) : {t : CandidateTree α} → Cut t → R
42   | t, .keep _ => keep t.root
43   | .node a _ _, .split cs => overhead a + ∑ i, cutValue keep overhead (cs i)
44 
45 def optimalValue (keep overhead : α → R) : CandidateTree α → R
46   | .leaf a => keep a
47   | .node a _ ts => min (keep a) (overhead a + ∑ i, optimalValue keep overhead (ts i))
48 
49 /-- An actual pruning is returned, with ties resolved in favor of keeping. -/
50 def compile (keep overhead : α → R) : (t : CandidateTree α) → Cut t
51   | .leaf a => .keep (.leaf a)
52   | .node a n ts =>
53     if keep a ≤ overhead a + ∑ i, optimalValue keep overhead (ts i) then
54       .keep (.node a n ts)
55     else .split (fun i => compile keep overhead (ts i))
56 
57 theorem optimalValue_le_cut (keep overhead : α → R) (t : CandidateTree α) (c : Cut t) :
58     optimalValue keep overhead t ≤ cutValue keep overhead c := by
59   induction t with
60   | leaf a => cases c; exact le_rfl
61   | node a n ts ih =>
62     cases c with
63     | keep => exact min_le_left _ _
64     | split cs =>
65       exact (min_le_right _ _).trans
66         (add_le_add le_rfl (Finset.sum_le_sum (fun i _ => ih i (cs i))))
67 
68 omit [IsStrictOrderedRing R] in
69 theorem compile_attains (keep overhead : α → R) (t : CandidateTree α) :
70     cutValue keep overhead (compile keep overhead t) = optimalValue keep overhead t := by
71   induction t with
72   | leaf a => rfl
73   | node a n ts ih =>
74     by_cases h : keep a ≤ overhead a + ∑ i, optimalValue keep overhead (ts i)
75     · simp [compile, h, cutValue, root, optimalValue]
76     · simp [compile, h, cutValue, ih, optimalValue, min_eq_right (le_of_not_ge h)]
77 
78 /-- Exactness includes both lower-bound correctness and an attaining witness. -/
79 theorem exact_tree_compiler (keep overhead : α → R) (t : CandidateTree α) :
80     (∀ c : Cut t, optimalValue keep overhead t ≤ cutValue keep overhead c) ∧
81     ∃ c : Cut t, cutValue keep overhead c = optimalValue keep overhead t := by
82   exact ⟨optimalValue_le_cut keep overhead t, compile keep overhead t,
83     compile_attains keep overhead t⟩
84 
85 theorem compile_minimizes (keep overhead : α → R) (t : CandidateTree α) (c : Cut t) :
86     cutValue keep overhead (compile keep overhead t) ≤ cutValue keep overhead c := by
87   rw [compile_attains]
88   exact optimalValue_le_cut keep overhead t c
89 
90 /- Cost plus multiplier times error equals the local-score objective. -/
91 omit [LinearOrder R] [IsStrictOrderedRing R] in
92 theorem lagrangian_decomposition (κ ε σ : α → R) (lam : R)
93     {t : CandidateTree α} (c : Cut t) :
94     cutValue (fun a => κ a + lam * ε a) σ c =
95       cutValue κ σ c + lam * cutValue ε (fun _ => 0) c := by
96   induction c with
97   | keep t => rfl
98   | @split a n ts cs ih =>
99     simp only [cutValue, ih, Finset.sum_add_distrib, zero_add, Finset.mul_sum]
100     ring
101 
102 theorem exact_lagrangian_compiler (κ ε σ : α → R) (lam : R) (t : CandidateTree α)
103     (c : Cut t) :
104     let best := compile (fun a => κ a + lam * ε a) σ t
105     cutValue κ σ best + lam * cutValue ε (fun _ => 0) best ≤
106       cutValue κ σ c + lam * cutValue ε (fun _ => 0) c := by
107   dsimp
108   simpa only [← lagrangian_decomposition] using
109     compile_minimizes (fun a => κ a + lam * ε a) σ t c
110 
111 /- Aggregation is proved at the actual pruning level, including split costs. -/
112 omit [LinearOrder R] [IsStrictOrderedRing R] in
113 theorem cutValue_weighted_family {J : Type*} [Fintype J]
114     (setup σ : α → R) (weights : J → R) (κ : J → α → R)
115     {t : CandidateTree α} (c : Cut t) :
116     cutValue (fun a => setup a + ∑ j, weights j * κ j a) σ c =
117       cutValue setup σ c + ∑ j, weights j * cutValue (κ j) (fun _ => 0) c := by
118   induction c with
119   | keep t => rfl
120   | @split a n ts cs ih =>
121     simp only [cutValue, ih, Finset.sum_add_distrib, zero_add, Finset.mul_sum]
122     rw [Finset.sum_comm (f := fun i j => weights j * cutValue (κ j) (fun _ => 0) (cs i))]
123     ring
124 
125 theorem shared_family_compiler {J : Type*} [Fintype J]
126     (setup σ : α → R) (weights : J → R) (κ ε : J → α → R)
127     (lam : R) (t : CandidateTree α) (c : Cut t) :
128     let agg := fun a => setup a + ∑ j, weights j * (κ j a + lam * ε j a)
129     let best := compile agg σ t
130     cutValue setup σ best +
131         ∑ j, weights j * (cutValue (κ j) (fun _ => 0) best +
132           lam * cutValue (ε j) (fun _ => 0) best) ≤
133       cutValue setup σ c +
134         ∑ j, weights j * (cutValue (κ j) (fun _ => 0) c +
135           lam * cutValue (ε j) (fun _ => 0) c) := by
136   dsimp
137   have h := compile_minimizes
138     (fun a => setup a + ∑ j, weights j * (κ j a + lam * ε j a)) σ t c
139   simpa only [cutValue_weighted_family, lagrangian_decomposition] using h
140 
141 /-- Two genuinely optimal prunings have a monotone error/cost frontier. -/
142 theorem monotone_lagrangian_frontier (κ ε σ : α → R)
143     (lam1 lam2 : R) (hlam1 : 0 ≤ lam1) (hlam : lam1 < lam2)
144     {t : CandidateTree α} (c₁ c₂ : Cut t)
145     (h₁ : ∀ c : Cut t, cutValue κ σ c₁ + lam1 * cutValue ε (fun _ => 0) c₁ ≤
146       cutValue κ σ c + lam1 * cutValue ε (fun _ => 0) c)
147     (h₂ : ∀ c : Cut t, cutValue κ σ c₂ + lam2 * cutValue ε (fun _ => 0) c₂ ≤
148       cutValue κ σ c + lam2 * cutValue ε (fun _ => 0) c) :
149     cutValue ε (fun _ => 0) c₂ ≤ cutValue ε (fun _ => 0) c₁ ∧
150       cutValue κ σ c₁ ≤ cutValue κ σ c₂ := by
151   have h12 := h₁ c₂
152   have h21 := h₂ c₁
153   have he : cutValue ε (fun _ => 0) c₂ ≤ cutValue ε (fun _ => 0) c₁ := by
154     nlinarith
155   exact ⟨he, by nlinarith⟩
156 
157 theorem positive_lagrangian_pareto (κ ε σ : α → R) (lam : R) (hlam : 0 < lam)
158     {t : CandidateTree α} (best : Cut t)
159     (hbest : ∀ c : Cut t, cutValue κ σ best + lam * cutValue ε (fun _ => 0) best ≤
160       cutValue κ σ c + lam * cutValue ε (fun _ => 0) c) :
161     ¬ ∃ c : Cut t, cutValue κ σ c ≤ cutValue κ σ best ∧
162       cutValue ε (fun _ => 0) c ≤ cutValue ε (fun _ => 0) best ∧
163       (cutValue κ σ c < cutValue κ σ best ∨
164        cutValue ε (fun _ => 0) c < cutValue ε (fun _ => 0) best) := by
165   rintro ⟨c, hc, he, hs⟩
166   have hb := hbest c
167   rcases hs with h | h <;> nlinarith
168 
169 /-- Strict score gaps withstand perturbations strictly smaller than half the gap. -/
170 theorem keep_decision_stable (K S K' S' : R) (_h : K < S)
171     (hK : |K' - K| < (S - K) / 2) (hS : |S' - S| < (S - K) / 2) :
172     K' < S' := by
173   have hk := (abs_lt.mp hK).2
174   have hs := (abs_lt.mp hS).1
175   linarith
176 
177 theorem split_decision_stable (K S K' S' : R) (h : S < K)
178     (hK : |K' - K| < (K - S) / 2) (hS : |S' - S| < (K - S) / 2) :
179     S' < K' := by
180   exact keep_decision_stable S K S' K' h hS hK
181 
182 end CandidateTree
183 end KomorebiPaperVIII
184 
185 -- FINAL AXIOM AUDITS
186 #print axioms KomorebiPaperVIII.CandidateTree.optimalValue_le_cut
187 #print axioms KomorebiPaperVIII.CandidateTree.compile_attains
188 #print axioms KomorebiPaperVIII.CandidateTree.exact_tree_compiler
189 #print axioms KomorebiPaperVIII.CandidateTree.compile_minimizes
190 #print axioms KomorebiPaperVIII.CandidateTree.lagrangian_decomposition
191 #print axioms KomorebiPaperVIII.CandidateTree.exact_lagrangian_compiler
192 #print axioms KomorebiPaperVIII.CandidateTree.cutValue_weighted_family
193 #print axioms KomorebiPaperVIII.CandidateTree.shared_family_compiler
194 #print axioms KomorebiPaperVIII.CandidateTree.monotone_lagrangian_frontier
195 #print axioms KomorebiPaperVIII.CandidateTree.positive_lagrangian_pareto
196 #print axioms KomorebiPaperVIII.CandidateTree.keep_decision_stable
197 #print axioms KomorebiPaperVIII.CandidateTree.split_decision_stable
198 #print axioms KomorebiPaperVIII.CandidateTree.compile
199 #print axioms KomorebiPaperVIII.CandidateTree.optimalValue

Back to source controls