BinaryAdaptive.lean

1 import Mathlib.Basic.Real.Basic
2 import Mathlib.Tactic
3 
4 /-!
5 Author: Komorebi P.
6 Checked source. Finite, possibly unbalanced BINARY trees.
7 Cuts are defined recursively. The bridge to set-valued antichains of arbitrary
8 finite arity is not included. Parent conservation is an explicit hypothesis.
9 -/
10 
11 namespace KomorebiPaperV.Binary
12 
13 inductive Tree (A : Type*) where
14   | leaf : A → Tree A
15   | branch : A → Tree A → Tree A → Tree A
16 
17 variable {A E : Type*}
18 
19 def label : Tree A → A
20   | .leaf a => a
21   | .branch a _ _ => a
22 
23 inductive Cut : Tree A → Type _ where
24   | stop (t : Tree A) : Cut t
25   | split {a : A} {l r : Tree A} : Cut l → Cut r → Cut (.branch a l r)
26 
27 def cutSum [Add E] (p : A → E) : {t : Tree A} → Cut t → E
28   | t, .stop _ => p (label t)
29   | _, .split l r => cutSum p l + cutSum p r
30 
31 def conserves [Add E] (p : A → E) : Tree A → Prop
32   | .leaf _ => True
33   | .branch a l r =>
34       p a = p (label l) + p (label r) ∧ conserves p l ∧ conserves p r
35 
36 theorem cutSum_eq_root [Add E] (p : A → E) {t : Tree A} (q : Cut t) :
37     conserves p t → cutSum p q = p (label t) := by
38   induction q with
39   | stop t =>
40     intro _
41     rfl
42   | split ql qr ihl ihr =>
43     intro h
44     rcases h with ⟨hp, hl, hr⟩
45     change cutSum p ql + cutSum p qr = _
46     rw [ihl hl, ihr hr]
47     exact hp.symm
48 
49 noncomputable def value (c : A → ℝ) : Tree A → ℝ
50   | .leaf a => c a
51   | .branch a l r => min (c a) (value c l + value c r)
52 
53 noncomputable def best (c : A → ℝ) : (t : Tree A) → Cut t
54   | .leaf a => .stop (.leaf a)
55   | .branch a l r =>
56       if c a ≤ value c l + value c r then .stop (.branch a l r)
57       else .split (best c l) (best c r)
58 
59 theorem value_le_cost (c : A → ℝ) {t : Tree A} (q : Cut t) :
60     value c t ≤ cutSum c q := by
61   induction q with
62   | stop t =>
63     cases t with
64     | leaf a => exact le_rfl
65     | branch a l r => exact min_le_left _ _
66   | split ql qr ihl ihr =>
67     exact le_trans (min_le_right _ _) (add_le_add ihl ihr)
68 
69 theorem best_cost (c : A → ℝ) (t : Tree A) :
70     cutSum c (best c t) = value c t := by
71   induction t with
72   | leaf a => rfl
73   | branch a l r ihl ihr =>
74     by_cases h : c a ≤ value c l + value c r
75     · simp [best, h, cutSum, label, value]
76     · have h' : value c l + value c r ≤ c a := by linarith
77       simp [best, h, cutSum, ihl, ihr, value, min_eq_right h']
78 
79 theorem best_is_global_minimum (c : A → ℝ) {t : Tree A} (q : Cut t) :
80     cutSum c (best c t) ≤ cutSum c q := by
81   rw [best_cost]
82   exact value_le_cost c q
83 
84 noncomputable def envelope (e : A → ℝ) : Tree A → ℝ
85   | .leaf a => e a
86   | .branch a l r => max (e a) (envelope e l + envelope e r)
87 
88 theorem root_le_envelope (e : A → ℝ) (t : Tree A) :
89     e (label t) ≤ envelope e t := by
90   cases t with
91   | leaf a => exact le_rfl
92   | branch a l r => exact le_max_left _ _
93 
94 theorem cut_perturbation (c d e : A → ℝ)
95     (h : ∀ a, |d a - c a| ≤ e a) {t : Tree A} (q : Cut t) :
96     |cutSum d q - cutSum c q| ≤ envelope e t := by
97   induction q with
98   | stop t =>
99     exact le_trans (h (label t)) (root_le_envelope e t)
100   | @split a l r ql qr ihl ihr =>
101     change |(cutSum d ql + cutSum d qr) - (cutSum c ql + cutSum c qr)| ≤ _
102     calc
103       |(cutSum d ql + cutSum d qr) - (cutSum c ql + cutSum c qr)| =
104           |(cutSum d ql - cutSum c ql) + (cutSum d qr - cutSum c qr)| := by
105             congr 1
106             ring
107       _ ≤ |cutSum d ql - cutSum c ql| + |cutSum d qr - cutSum c qr| := abs_add_le _ _
108       _ ≤ envelope e l + envelope e r := add_le_add ihl ihr
109       _ ≤ envelope e (.branch a l r) := le_max_right _ _
110 
111 end KomorebiPaperV.Binary

Back to source controls