FiniteAdaptive.lean

1 import Mathlib.MeasureTheory.Measure.Basic
2 import KomorebiPaperV.FiniteSelection
3 
4 /-!
5 Author: Komorebi P.
6 Checked source; see the bundled build and axiom audit.
7 Finite trees with arbitrary positive finite branching, including unary branches.
8 Cuts are typed recursive prunings. CompletePrunings proves the set-valued
9 covering-antichain equivalence.
10 -/
11 
12 open scoped BigOperators
13 namespace KomorebiPaperV.FiniteAdaptive
14 
15 inductive Tree (A : Type*) where
16   | leaf : A → Tree A
17   | branch : (a : A) → (n : ℕ) → (Fin (n + 1) → Tree A) → Tree A
18 
19 variable {A E : Type*}
20 
21 def label : Tree A → A
22   | .leaf a => a
23   | .branch a _ _ => a
24 
25 inductive Cut : Tree A → Type _ where
26   | stop (t : Tree A) : Cut t
27   | split {a : A} {n : ℕ} {children : Fin (n + 1) → Tree A} :
28       (∀ i, Cut (children i)) → Cut (.branch a n children)
29 
30 def cutSum [AddCommMonoid E] (p : A → E) : {t : Tree A} → Cut t → E
31   | t, .stop _ => p (label t)
32   | _, .split q => ∑ i, cutSum p (q i)
33 
34 def conserves [AddCommMonoid E] (p : A → E) : Tree A → Prop
35   | .leaf _ => True
36   | .branch a _ children =>
37       p a = ∑ i, p (label (children i)) ∧ ∀ i, conserves p (children i)
38 
39 theorem cutSum_eq_root [AddCommMonoid E] (p : A → E) {t : Tree A} (q : Cut t) :
40     conserves p t → cutSum p q = p (label t) := by
41   induction q with
42   | stop t => intro _; rfl
43   | @split a n children q ih =>
44     intro h
45     rcases h with ⟨hroot, hchild⟩
46     change (∑ i, cutSum p (q i)) = p a
47     calc
48       _ = ∑ i, p (label (children i)) :=
49         Finset.sum_congr rfl (fun i _ => ih i (hchild i))
50       _ = p a := hroot.symm
51 
52 /-- This includes operator-valued packets: take E to be an additive space of maps. -/
53 theorem cutSum_eq_identity [AddCommMonoid E] (p : A → E) {t : Tree A}
54     (q : Cut t) (h : conserves p t) (identity : E) (hroot : p (label t) = identity) :
55     cutSum p q = identity := (cutSum_eq_root p q h).trans hroot
56 
57 inductive Terminal : Tree A → Type _ where
58   | here {a : A} : Terminal (.leaf a)
59   | down {a : A} {n : ℕ} {children : Fin (n + 1) → Tree A}
60       (i : Fin (n + 1)) : Terminal (children i) → Terminal (.branch a n children)
61 
62 /-- Number of selected packets met by a typed root-to-terminal path. -/
63 def pathHits : {t : Tree A} → Cut t → Terminal t → ℕ
64   | _, .stop _, _ => 1
65   | _, .split q, .down i path => pathHits (q i) path
66 
67 theorem pathHits_one {t : Tree A} (q : Cut t) :
68     ∀ path : Terminal t, pathHits q path = 1 := by
69   induction q with
70   | stop t => intro _; rfl
71   | split q ih =>
72     intro path
73     cases path with
74     | down i path => exact ih i path
75 
76 def leafCutEquiv (a : A) : Cut (.leaf a) ≃ Unit where
77   toFun _ := ()
78   invFun _ := .stop (.leaf a)
79   left_inv q := by cases q; rfl
80   right_inv u := by cases u; rfl
81 
82 def branchCutEquiv (a : A) (n : ℕ) (children : Fin (n + 1) → Tree A) :
83     Cut (.branch a n children) ≃ (Unit ⊕ (∀ i, Cut (children i))) where
84   toFun q := match q with
85     | .stop _ => .inl ()
86     | .split childrenCuts => .inr childrenCuts
87   invFun q := match q with
88     | .inl _ => .stop (.branch a n children)
89     | .inr childrenCuts => .split childrenCuts
90   left_inv q := by cases q <;> rfl
91   right_inv q := by cases q with
92     | inl u => cases u; rfl
93     | inr qs => rfl
94 
95 /-- Finiteness of all admissible recursive cuts, not merely a sampled cut list. -/
96 @[instance_reducible]
97 noncomputable def cutFintype : (t : Tree A) → Fintype (Cut t)
98   | .leaf a => Fintype.ofEquiv Unit (leafCutEquiv a).symm
99   | .branch a n children =>
100       letI : ∀ i, Fintype (Cut (children i)) := fun i => cutFintype (children i)
101       Fintype.ofEquiv (Unit ⊕ (∀ i, Cut (children i)))
102         (branchCutEquiv a n children).symm
103 
104 noncomputable instance (t : Tree A) : Fintype (Cut t) := cutFintype t
105 
106 /-- Arbitrary criteria need not be additive for finite attainment. -/
107 theorem arbitrary_objective_minimum (t : Tree A) (J : Cut t → ℝ) :
108     ∃ q : Cut t, ∀ r : Cut t, J q ≤ J r := by
109   classical
110   obtain ⟨q, _, hq⟩ := KomorebiPaperV.finite_minimum J Finset.univ
111     ⟨Cut.stop t, Finset.mem_univ _⟩
112   exact ⟨q, fun r => hq r (Finset.mem_univ _)⟩
113 
114 theorem strict_minimum_positive_gap (t : Tree A) (J : Cut t → ℝ) (q : Cut t)
115     (hother : ∃ r : Cut t, r ≠ q) (hstrict : ∀ r : Cut t, r ≠ q → J q < J r) :
116     ∃ γ : ℝ, 0 < γ ∧ ∀ r : Cut t, r ≠ q → γ ≤ J r - J q := by
117   classical
118   obtain ⟨r, hr⟩ := hother
119   obtain ⟨γ, hγ, hgap⟩ := KomorebiPaperV.positive_gap Finset.univ J q
120     ⟨r, Finset.mem_erase.mpr ⟨hr, Finset.mem_univ _⟩⟩
121     (fun s _ hs => hstrict s hs)
122   exact ⟨γ, hγ, fun s hs => hgap s (Finset.mem_univ _) hs⟩
123 
124 noncomputable def value (c : A → ℝ) : Tree A → ℝ
125   | .leaf a => c a
126   | .branch a _ children => min (c a) (∑ i, value c (children i))
127 
128 /-- Specification-level selector. The exact Python implementation caches children.
129 This definition alone is NOT a formal bound on Lean evaluation time. -/
130 noncomputable def best (c : A → ℝ) : (t : Tree A) → Cut t
131   | .leaf a => .stop (.leaf a)
132   | .branch a n children =>
133       if c a ≤ ∑ i, value c (children i) then .stop (.branch a n children)
134       else .split (fun i => best c (children i))
135 
136 theorem value_le_cost (c : A → ℝ) {t : Tree A} (q : Cut t) :
137     value c t ≤ cutSum c q := by
138   induction q with
139   | stop t =>
140     cases t with
141     | leaf a => exact le_rfl
142     | branch a n children => exact min_le_left _ _
143   | split q ih =>
144     exact le_trans (min_le_right _ _) (Finset.sum_le_sum (fun i _ => ih i))
145 
146 theorem best_cost (c : A → ℝ) (t : Tree A) : cutSum c (best c t) = value c t := by
147   induction t with
148   | leaf a => rfl
149   | branch a n children ih =>
150     by_cases h : c a ≤ ∑ i, value c (children i)
151     · simp [best, h, cutSum, label, value]
152     · have h' : (∑ i, value c (children i)) ≤ c a := le_of_lt (lt_of_not_ge h)
153       simp only [best, ite_eq_right h, cutSum, value, min_eq_right h']
154       exact Finset.sum_congr rfl (fun i _ => ih i)
155 
156 theorem best_is_global_minimum (c : A → ℝ) {t : Tree A} (q : Cut t) :
157     cutSum c (best c t) ≤ cutSum c q := by
158   rw [best_cost]
159   exact value_le_cost c q
160 
161 theorem best_preserves_synthesis [AddCommMonoid E] (p : A → E) (c : A → ℝ)
162     (t : Tree A) (h : conserves p t) : cutSum p (best c t) = p (label t) :=
163   cutSum_eq_root p (best c t) h
164 
165 theorem stop_on_tie (c : A → ℝ) (a : A) (n : ℕ) (children : Fin (n + 1) → Tree A)
166     (h : c a = ∑ i, value c (children i)) :
167     best c (.branch a n children) = Cut.stop (.branch a n children) := by
168   simp [best, le_of_eq h]
169 
170 noncomputable def envelope (e : A → ℝ) : Tree A → ℝ
171   | .leaf a => e a
172   | .branch a _ children => max (e a) (∑ i, envelope e (children i))
173 
174 theorem root_le_envelope (e : A → ℝ) (t : Tree A) : e (label t) ≤ envelope e t := by
175   cases t with
176   | leaf a => exact le_rfl
177   | branch a n children => exact le_max_left _ _
178 
179 theorem cost_le_envelope (e : A → ℝ) {t : Tree A} (q : Cut t) :
180     cutSum e q ≤ envelope e t := by
181   induction q with
182   | stop t => exact root_le_envelope e t
183   | split q ih =>
184     exact le_trans (Finset.sum_le_sum (fun i _ => ih i)) (le_max_right _ _)
185 
186 /-- The envelope is attained by a pruning, so it is the exact worst cut weight. -/
187 theorem envelope_attained (e : A → ℝ) (t : Tree A) :
188     ∃ q : Cut t, cutSum e q = envelope e t := by
189   classical
190   induction t with
191   | leaf a => exact ⟨.stop (.leaf a), rfl⟩
192   | branch a n children ih =>
193     by_cases h : (∑ i, envelope e (children i)) ≤ e a
194     · exact ⟨.stop (.branch a n children), (max_eq_left h).symm⟩
195     · choose q hq using ih
196       refine ⟨.split q, ?_⟩
197       change (∑ i, cutSum e (q i)) = max (e a) (∑ i, envelope e (children i))
198       rw [max_eq_right (le_of_lt (lt_of_not_ge h))]
199       exact Finset.sum_congr rfl (fun i _ => hq i)
200 
201 theorem cut_perturbation (c d e : A → ℝ) (h : ∀ a, |d a - c a| ≤ e a)
202     {t : Tree A} (q : Cut t) : |cutSum d q - cutSum c q| ≤ envelope e t := by
203   induction q with
204   | stop t => exact le_trans (h (label t)) (root_le_envelope e t)
205   | @split a n children q ih =>
206     change |(∑ i, cutSum d (q i)) - ∑ i, cutSum c (q i)| ≤ _
207     calc
208       _ = |∑ i, (cutSum d (q i) - cutSum c (q i))| := by rw [Finset.sum_sub_distrib]
209       _ ≤ ∑ i, |cutSum d (q i) - cutSum c (q i)| := Finset.abs_sum_le_sum_abs _ _
210       _ ≤ ∑ i, envelope e (children i) := Finset.sum_le_sum (fun i _ => ih i)
211       _ ≤ envelope e (.branch a n children) := le_max_right _ _
212 
213 theorem value_perturbation (c d e : A → ℝ) (h : ∀ a, |d a - c a| ≤ e a)
214     (t : Tree A) : |value d t - value c t| ≤ envelope e t := by
215   have hc := abs_le.mp (cut_perturbation c d e h (best c t))
216   have hd := abs_le.mp (cut_perturbation c d e h (best d t))
217   have hminc := value_le_cost c (best d t)
218   have hmind := value_le_cost d (best c t)
219   rw [best_cost c t] at hc
220   rw [best_cost d t] at hd
221   exact abs_le.mpr ⟨by linarith, by linarith⟩
222 
223 theorem best_unchanged_of_gap (c d e : A → ℝ) (h : ∀ a, |d a - c a| ≤ e a)
224     (t : Tree A) (γ : ℝ)
225     (hgap : ∀ q : Cut t, q ≠ best c t → γ ≤ cutSum c q - cutSum c (best c t))
226     (hmargin : 2 * envelope e t < γ) : best d t = best c t := by
227   by_contra hne
228   have hfirst := abs_le.mp (cut_perturbation c d e h (best c t))
229   have hsecond := abs_le.mp (cut_perturbation c d e h (best d t))
230   have hsep := hgap (best d t) hne
231   have hmin := best_is_global_minimum d (best c t)
232   linarith
233 
234 /-- Logical bottom-up comparison recurrence, excluding arithmetic and cut copying. -/
235 def comparisonCount : Tree A → ℕ
236   | .leaf _ => 0
237   | .branch _ _ children => 1 + ∑ i, comparisonCount (children i)
238 
239 def internalNodes : Tree A → ℕ
240   | .leaf _ => 0
241   | .branch _ _ children => (∑ i, internalNodes (children i)) + 1
242 
243 theorem one_comparison_per_internal_node (t : Tree A) : comparisonCount t = internalNodes t := by
244   induction t with
245   | leaf a => rfl
246   | branch a n children ih =>
247     dsimp [comparisonCount, internalNodes]
248     rw [Finset.sum_congr rfl (fun i _ => ih i)]
249     omega
250 
251 /-- Probability is transferred from a joint local-error event by set inclusion. -/
252 theorem selector_probability {Ω : Type*} [MeasurableSpace Ω]
253     (μ : MeasureTheory.Measure Ω) (good : Set Ω) (δ : ENNReal)
254     (c e : A → ℝ) (d : Ω → A → ℝ) (t : Tree A) (γ : ℝ)
255     (hgood : ∀ ω ∈ good, ∀ a, |d ω a - c a| ≤ e a)
256     (hgap : ∀ q : Cut t, q ≠ best c t → γ ≤ cutSum c q - cutSum c (best c t))
257     (hmargin : 2 * envelope e t < γ) (hprob : 1 - δ ≤ μ good) :
258     1 - δ ≤ μ {ω | best (d ω) t = best c t} := by
259   apply hprob.trans
260   apply MeasureTheory.measure_mono
261   intro ω hω
262   exact best_unchanged_of_gap c (d ω) e (hgood ω hω) t γ hgap hmargin
263 
264 end KomorebiPaperV.FiniteAdaptive

Back to source controls