PruningSums.lean

1 import KomorebiPaperV.CompletePrunings
2 import KomorebiPaperV.HilbertPackets
3 
4 /-! Author: Komorebi P. Literal finite node sums, synthesis and stable antichain selection. -/
5 namespace KomorebiPaperV.PruningSums
6 open KomorebiPaperV.FiniteAdaptive KomorebiPaperV.CompletePrunings
7 variable {A E : Type*}
8 
9 def leafNodeEquiv (a : A) : Node (.leaf a) ≃ Unit where
10   toFun _ := ()
11   invFun _ := .root _
12   left_inv v := by cases v; rfl
13   right_inv u := by cases u; rfl
14 
15 def branchNodeEquiv (a : A) (n : ℕ) (ch : Fin (n+1) → FiniteAdaptive.Tree A) :
16     Node (.branch a n ch) ≃ Unit ⊕ (Σ i, Node (ch i)) where
17   toFun v := match v with
18     | .root _ => .inl ()
19     | .down i w => .inr ⟨i,w⟩
20   invFun v := match v with
21     | .inl _ => .root _
22     | .inr ⟨i,w⟩ => .down i w
23   left_inv v := by cases v <;> rfl
24   right_inv v := by cases v with
25     | inl u => cases u; rfl
26     | inr v => cases v; rfl
27 
28 @[instance_reducible]
29 noncomputable def nodeFintype : (t : FiniteAdaptive.Tree A) → Fintype (Node t)
30   | .leaf a => Fintype.ofEquiv Unit (leafNodeEquiv a).symm
31   | .branch a n ch =>
32       letI : ∀ i, Fintype (Node (ch i)) := fun i => nodeFintype (ch i)
33       Fintype.ofEquiv (Unit ⊕ (Σ i, Node (ch i))) (branchNodeEquiv a n ch).symm
34 
35 noncomputable instance (t : FiniteAdaptive.Tree A) : Fintype (Node t) := nodeFintype t
36 
37 def nodeLabel : {t : FiniteAdaptive.Tree A} → Node t → A
38   | t, .root _ => label t
39   | _, .down _ v => nodeLabel v
40 
41 theorem node_sum_branch [AddCommMonoid E] (a : A) (n : ℕ)
42     (ch : Fin (n+1) → FiniteAdaptive.Tree A) (f : Node (.branch a n ch) → E) :
43     ∑ v, f v = f (.root _) + ∑ i, ∑ v, f (.down i v) := by
44   rw [← Equiv.sum_comp (branchNodeEquiv a n ch).symm]
45   rw [Fintype.sum_sum_type, Fintype.sum_sigma]
46   simp [branchNodeEquiv]
47 
48 noncomputable def selectedNodes {t : FiniteAdaptive.Tree A} (q : Cut t) : Finset (Node t) :=
49   {v | Selected q v}.toFinite.toFinset
50 
51 theorem mem_selectedNodes {t : FiniteAdaptive.Tree A} (q : Cut t) (v : Node t) :
52     v ∈ selectedNodes q ↔ Selected q v := Set.Finite.mem_toFinset _
53 
54 theorem cutSum_eq_nodeSum [AddCommMonoid E] (p : A → E) {t : FiniteAdaptive.Tree A} (q : Cut t) :
55     cutSum p q = ∑ v ∈ selectedNodes q, p (nodeLabel v) := by
56   classical
57   have hsum : ∑ v ∈ selectedNodes q, p (nodeLabel v) =
58       ∑ v, if Selected q v then p (nodeLabel v) else 0 := by
59     rw [← Finset.sum_filter]
60     congr 1
61     ext v
62     simp [mem_selectedNodes]
63   rw [hsum]
64   clear hsum
65   induction q with
66   | stop t => simp [selected_stop_iff, cutSum, nodeLabel]
67   | @split a n ch q ih =>
68     rw [node_sum_branch]
69     simp only [selected_split_root_false, ↓reduceIte, zero_add,
70       selected_split_down_iff, nodeLabel, cutSum]
71     exact Finset.sum_congr rfl (fun i _ => ih i)
72 
73 abbrev Pruning (t : FiniteAdaptive.Tree A) := {S : Set (Node t) // Complete S}
74 
75 noncomputable def nodeSum [AddCommMonoid E] (p : A → E) {t : FiniteAdaptive.Tree A}
76     (S : Pruning t) : E := ∑ v ∈ S.val.toFinite.toFinset, p (nodeLabel v)
77 
78 theorem pruning_nodeSum [AddCommMonoid E] (p : A → E) {t : FiniteAdaptive.Tree A} (q : Cut t) :
79     nodeSum p (pruningEquiv t q) = cutSum p q := (cutSum_eq_nodeSum p q).symm
80 
81 theorem antichain_synthesis [AddCommMonoid E] (p : A → E) (t : FiniteAdaptive.Tree A)
82     (h : conserves p t) (S : Pruning t) : nodeSum p S = p (label t) := by
83   obtain ⟨q,rfl⟩ := (pruningEquiv t).surjective S
84   rw [pruning_nodeSum]
85   exact cutSum_eq_root p q h
86 
87 /-- Applied operator identity for every complete covering antichain. -/
88 theorem packet_projector_synthesis {H : Type*} [NormedAddCommGroup H] [NormedSpace ℂ H]
89     (p : A → H →L[ℂ] H) (t : FiniteAdaptive.Tree A)
90     (h : conserves p t) (hr : p (label t) = ContinuousLinearMap.id ℂ H)
91     (S : Pruning t) (x : H) :
92     nodeSum p S = ContinuousLinearMap.id ℂ H ∧
93       (∑ v ∈ S.val.toFinite.toFinset, p (nodeLabel v) x) = x := by
94   have hs := (antichain_synthesis p t h S).trans hr
95   refine ⟨hs, ?_⟩
96   have hx := congrArg (fun T : H →L[ℂ] H => T x) hs
97   simpa [nodeSum] using hx
98 
99 noncomputable def selected (c : A → ℝ) (t : FiniteAdaptive.Tree A) : Pruning t :=
100   pruningEquiv t (best c t)
101 
102 theorem selected_global_minimum (c : A → ℝ) (t : FiniteAdaptive.Tree A) (S : Pruning t) :
103     nodeSum c (selected c t) ≤ nodeSum c S := by
104   obtain ⟨q,rfl⟩ := (pruningEquiv t).surjective S
105   simp only [selected, pruning_nodeSum]
106   exact best_is_global_minimum c q
107 
108 theorem antichain_perturbation (c d e : A → ℝ) (h : ∀ a, |d a-c a| ≤ e a)
109     (t : FiniteAdaptive.Tree A) (S : Pruning t) :
110     |nodeSum d S-nodeSum c S| ≤ envelope e t := by
111   obtain ⟨q,rfl⟩ := (pruningEquiv t).surjective S
112   simp only [pruning_nodeSum]
113   exact cut_perturbation c d e h q
114 
115 theorem antichain_envelope_attained (e : A → ℝ) (t : FiniteAdaptive.Tree A) :
116     ∃ S : Pruning t, nodeSum e S = envelope e t := by
117   obtain ⟨q,hq⟩ := envelope_attained e t
118   exact ⟨pruningEquiv t q, (pruning_nodeSum e q).trans hq⟩
119 
120 theorem antichain_selector_stable (c d e : A → ℝ) (h : ∀ a, |d a-c a| ≤ e a)
121     (t : FiniteAdaptive.Tree A) (γ : ℝ)
122     (hg : ∀ S : Pruning t, S ≠ selected c t → γ ≤ nodeSum c S-nodeSum c (selected c t))
123     (hm : 2*envelope e t < γ) : selected d t = selected c t := by
124   apply congrArg (pruningEquiv t)
125   apply best_unchanged_of_gap c d e h t γ _ hm
126   intro q hq
127   have hne : pruningEquiv t q ≠ selected c t := fun he => hq ((pruningEquiv t).injective he)
128   simpa only [selected, pruning_nodeSum] using hg (pruningEquiv t q) hne
129 
130 /-- The manuscript's possibly nonadditive representation/leakage/complexity criterion. -/
131 def objective {t : FiniteAdaptive.Tree A} (R L K : Pruning t → ℝ) (η τ : ℝ) (S : Pruning t) : ℝ :=
132   R S + η * L S + τ * K S
133 
134 theorem objective_minimum (t : FiniteAdaptive.Tree A) (R L K : Pruning t → ℝ) (η τ : ℝ) :
135     ∃ S : Pruning t, ∀ T, objective R L K η τ S ≤ objective R L K η τ T :=
136   complete_pruning_minimum t _
137 
138 theorem objective_positive_gap (t : FiniteAdaptive.Tree A) (J : Pruning t → ℝ) (S : Pruning t)
139     (ho : ∃ T, T ≠ S) (hu : ∀ T, T ≠ S → J S < J T) :
140     ∃ γ : ℝ, 0 < γ ∧ ∀ T, T ≠ S → γ ≤ J T-J S := by
141   let : Fintype (Pruning t) := Fintype.ofEquiv (Cut t) (pruningEquiv t)
142   classical
143   obtain ⟨T,hT⟩ := ho
144   obtain ⟨γ,hγ,hg⟩ := KomorebiPaperV.positive_gap Finset.univ J S
145     ⟨T, Finset.mem_erase.mpr ⟨hT, Finset.mem_univ _⟩⟩ (fun U _ hU => hu U hU)
146   exact ⟨γ,hγ,fun U hU => hg U (Finset.mem_univ _) hU⟩
147 
148 theorem objective_stability (t : FiniteAdaptive.Tree A) (J J' : Pruning t → ℝ)
149     (S : Pruning t) (γ ε : ℝ)
150     (hg : ∀ T, T ≠ S → γ ≤ J T-J S) (he : ∀ T, |J' T-J T| ≤ ε)
151     (hm : 2*ε < γ) : ∀ T, T ≠ S → J' S < J' T := by
152   intro T hT
153   have hs := abs_le.mp (he S)
154   have ht := abs_le.mp (he T)
155   have hgap := hg T hT
156   linarith
157 
158 theorem singleton_selector (t : FiniteAdaptive.Tree A) (S : Pruning t)
159     (hs : ∀ T : Pruning t, T = S) (J : Pruning t → ℝ) :
160     ∀ T, J S ≤ J T := by
161   intro T
162   rw [hs T]
163 
164 /-- The positive gap is attained by a genuine competitor, not just an arbitrary lower bound. -/
165 theorem objective_gap_attained (t : FiniteAdaptive.Tree A) (J : Pruning t → ℝ) (S : Pruning t)
166     (ho : ∃ T, T ≠ S) (hu : ∀ T, T ≠ S → J S < J T) :
167     ∃ T : Pruning t, T ≠ S ∧ 0 < J T-J S ∧ ∀ U, U ≠ S → J T-J S ≤ J U-J S := by
168   let : Fintype (Pruning t) := Fintype.ofEquiv (Cut t) (pruningEquiv t)
169   classical
170   obtain ⟨U,hU⟩ := ho
171   obtain ⟨T,hT,hmin⟩ := KomorebiPaperV.finite_minimum (fun T => J T-J S)
172     (Finset.univ.erase S) ⟨U, Finset.mem_erase.mpr ⟨hU, Finset.mem_univ _⟩⟩
173   have hTS := (Finset.mem_erase.mp hT).1
174   exact ⟨T,hTS,sub_pos.mpr (hu T hTS),fun V hV => hmin V
175     (Finset.mem_erase.mpr ⟨hV, Finset.mem_univ _⟩)⟩
176 
177 end KomorebiPaperV.PruningSums

Back to source controls