PruningAlgorithm.lean

1 import KomorebiPaperV.PruningSums
2 
3 /-!
4 Author: Komorebi P. A bottom-up evaluator with cached child results.
5 The cost model charges one node visit, one comparison per internal node, and
6 one addition per child when summing cached values. Scalar node costs are inputs.
7 The theorem concerns this unit-cost model, not Lean runtime or output printing.
8 -/
9 namespace KomorebiPaperV.PruningAlgorithm
10 open KomorebiPaperV.FiniteAdaptive KomorebiPaperV.CompletePrunings KomorebiPaperV.PruningSums
11 variable {A : Type*}
12 
13 structure Result (t : FiniteAdaptive.Tree A) where
14   cut : Cut t
15   cost : ℝ
16   comparisons : ℕ
17   additions : ℕ
18   visits : ℕ
19 
20 noncomputable def solve (c : A → ℝ) : (t : FiniteAdaptive.Tree A) → Result t
21   | .leaf a => ⟨.stop _, c a, 0, 0, 1⟩
22   | .branch a n ch =>
23       let child := fun i => solve c (ch i)
24       let total := ∑ i, (child i).cost
25       let stop := c a ≤ total
26       ⟨if stop then .stop _ else .split (fun i => (child i).cut),
27        min (c a) total,
28        1 + ∑ i, (child i).comparisons,
29        (n+1) + ∑ i, (child i).additions,
30        1 + ∑ i, (child i).visits⟩
31 
32 def nodes : FiniteAdaptive.Tree A → ℕ
33   | .leaf _ => 1
34   | .branch _ _ ch => 1 + ∑ i, nodes (ch i)
35 
36 theorem solve_correct (c : A → ℝ) (t : FiniteAdaptive.Tree A) :
37     (solve c t).cost = value c t ∧ (solve c t).cut = best c t := by
38   induction t with
39   | leaf a => exact ⟨rfl,rfl⟩
40   | branch a n ch ih =>
41     have hc : (∑ i, (solve c (ch i)).cost) = ∑ i, value c (ch i) :=
42       Finset.sum_congr rfl (fun i _ => (ih i).1)
43     constructor
44     · simp only [solve, value, hc]
45     · simp only [solve, best, hc]
46       split_ifs
47       · rfl
48       · congr 1
49         funext i
50         exact (ih i).2
51 
52 theorem solve_comparisons (c : A → ℝ) (t : FiniteAdaptive.Tree A) :
53     (solve c t).comparisons = internalNodes t := by
54   induction t with
55   | leaf a => rfl
56   | branch a n ch ih =>
57     simp only [solve, internalNodes]
58     rw [Finset.sum_congr rfl (fun i _ => ih i)]
59     omega
60 
61 theorem solve_visits (c : A → ℝ) (t : FiniteAdaptive.Tree A) :
62     (solve c t).visits = nodes t := by
63   induction t with
64   | leaf a => rfl
65   | branch a n ch ih =>
66     simp only [solve, nodes]
67     rw [Finset.sum_congr rfl (fun i _ => ih i)]
68 
69 theorem solve_additions (c : A → ℝ) (t : FiniteAdaptive.Tree A) :
70     (solve c t).additions + 1 = nodes t := by
71   induction t with
72   | leaf a => rfl
73   | branch a n ch ih =>
74     have hs : ∑ i, ((solve c (ch i)).additions+1) = ∑ i, nodes (ch i) :=
75       Finset.sum_congr rfl (fun i _ => ih i)
76     simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_univ,
77       Fintype.card_fin, smul_eq_mul, mul_one] at hs
78     dsimp [solve, nodes]
79     omega
80 
81 theorem internal_le_nodes (t : FiniteAdaptive.Tree A) : internalNodes t ≤ nodes t := by
82   induction t with
83   | leaf a => simp [internalNodes, nodes]
84   | branch a n ch ih =>
85     have h := Finset.sum_le_sum (fun i (_ : i ∈ Finset.univ) => ih i)
86     dsimp [internalNodes, nodes]
87     omega
88 
89 theorem solve_linear_work (c : A → ℝ) (t : FiniteAdaptive.Tree A) :
90     (solve c t).visits + (solve c t).comparisons + (solve c t).additions ≤ 3 * nodes t := by
91   have hv := solve_visits c t
92   have hc := solve_comparisons c t
93   have ha := solve_additions c t
94   have hi := internal_le_nodes t
95   omega
96 
97 theorem computed_antichain_optimal (c : A → ℝ) (t : FiniteAdaptive.Tree A) (S : Pruning t) :
98     nodeSum c (pruningEquiv t (solve c t).cut) ≤ nodeSum c S := by
99   rw [(solve_correct c t).2]
100   exact selected_global_minimum c t S
101 
102 theorem antichain_probability {Ω : Type*} [MeasurableSpace Ω]
103     (μ : MeasureTheory.Measure Ω) (good : Set Ω) (δ : ENNReal)
104     (c e : A → ℝ) (d : Ω → A → ℝ) (t : FiniteAdaptive.Tree A) (γ : ℝ)
105     (hgood : ∀ ω ∈ good, ∀ a, |d ω a-c a| ≤ e a)
106     (hg : ∀ S : Pruning t, S ≠ selected c t → γ ≤ nodeSum c S-nodeSum c (selected c t))
107     (hm : 2*envelope e t < γ) (hprob : 1-δ ≤ μ good) :
108     1-δ ≤ μ {ω | selected (d ω) t = selected c t} := by
109   apply hprob.trans
110   apply MeasureTheory.measure_mono
111   intro ω hω
112   exact antichain_selector_stable c (d ω) e (hgood ω hω) t γ hg hm
113 
114 end KomorebiPaperV.PruningAlgorithm

Back to source controls