FiniteTV.lean

1 import KomorebiLSM.NormalizedDefect
2 
3 /-! Finite total variation uses the actual half-sum of absolute probability differences. -/
4 set_option autoImplicit false
5 namespace Komorebi.LSM.FiniteTV
6 open scoped BigOperators
7 open FiniteBayes FiniteInstruments
8 variable {I : Type*} [Fintype I]
9 
10 noncomputable def l1 (x : I → ℝ) : ℝ := ∑ i, |x i|
11 noncomputable def distance (p q : I → ℝ) : ℝ := l1 (p-q)/2
12 
13 theorem l1_nonneg (x : I → ℝ) : 0 ≤ l1 x := Finset.sum_nonneg (fun i _ => abs_nonneg (x i))
14 @[simp] theorem l1_zero : l1 (0 : I → ℝ)=0 := by simp [l1]
15 @[simp] theorem l1_neg (x : I → ℝ) : l1 (-x)=l1 x := by simp [l1]
16 
17 theorem l1_add_le (x y : I → ℝ) : l1 (x+y) ≤ l1 x+l1 y := by
18   simp only [l1,Pi.add_apply,← Finset.sum_add_distrib]
19   exact Finset.sum_le_sum (fun i _ => abs_add_le (x i) (y i))
20 
21 theorem l1_sub_le (x y : I → ℝ) : l1 (x-y) ≤ l1 x+l1 y := by
22   simpa only [sub_eq_add_neg,l1_neg] using l1_add_le x (-y)
23 
24 theorem l1_smul (a : ℝ) (x : I → ℝ) : l1 (a • x)=|a| * l1 x := by
25   simp only [l1,Pi.smul_apply,smul_eq_mul,abs_mul,Finset.mul_sum]
26 
27 theorem abs_mass_le_l1 (x : I → ℝ) : |mass x| ≤ l1 x := by
28   simpa only [mass_apply,l1] using Finset.abs_sum_le_sum_abs x Finset.univ
29 
30 theorem l1_of_nonneg (x : I → ℝ) (hx : ∀ i, 0 ≤ x i) : l1 x=mass x := by
31   simp only [l1,mass_apply,abs_of_nonneg (hx _)]
32 
33 theorem l1_prior (p : I → ℝ) (hp : IsPrior p) : l1 p=1 :=
34   (l1_of_nonneg p hp.1).trans (mass_prior p hp)
35 
36 theorem distance_nonneg (p q : I → ℝ) : 0 ≤ distance p q :=
37   div_nonneg (l1_nonneg _) (by norm_num)
38 
39 @[simp] theorem distance_self (p : I → ℝ) : distance p p=0 := by simp [distance]
40 
41 theorem distance_comm (p q : I → ℝ) : distance p q=distance q p := by
42   simp only [distance,l1,Pi.sub_apply,abs_sub_comm]
43 
44 theorem distance_triangle (p q r : I → ℝ) : distance p r ≤ distance p q+distance q r := by
45   have he : p-r=(p-q)+(q-r) := by abel
46   have h := l1_add_le (p-q) (q-r)
47   rw [← he] at h
48   unfold distance
49   linarith
50 
51 theorem distance_le_one (p q : I → ℝ) (hp : IsPrior p) (hq : IsPrior q) :
52     distance p q ≤ 1 := by
53   have h := l1_sub_le p q
54   rw [l1_prior p hp,l1_prior q hq] at h
55   unfold distance
56   linarith
57 
58 section Events
59 variable [DecidableEq I]
60 
61 noncomputable def restrict (p : I → ℝ) (H : Finset I) (i : I) : ℝ := if i∈H then p i else 0
62 noncomputable def eventMass (p : I → ℝ) (H : Finset I) : ℝ := ∑ i ∈ H, p i
63 noncomputable def conditional (p : I → ℝ) (H : Finset I) : I → ℝ := normalize mass (restrict p H)
64 
65 omit [Fintype I] in
66 theorem restrict_nonneg (p : I → ℝ) (hp : ∀ i, 0 ≤ p i) (H : Finset I) :
67     ∀ i, 0 ≤ restrict p H i := by
68   intro i
69   unfold restrict
70   split_ifs
71   · exact hp i
72   · exact le_rfl
73 
74 theorem restrict_mass (p : I → ℝ) (H : Finset I) : mass (restrict p H)=eventMass p H := by
75   simp [mass_apply,restrict,eventMass]
76 
77 omit [Fintype I] [DecidableEq I] in
78 theorem eventMass_nonneg (p : I → ℝ) (hp : ∀ i, 0 ≤ p i) (H : Finset I) :
79     0 ≤ eventMass p H := Finset.sum_nonneg (fun i _ => hp i)
80 
81 theorem conditional_prior (p : I → ℝ) (hp : IsPrior p) (H : Finset I)
82     (hH : 0<eventMass p H) : IsPrior (conditional p H) :=
83   normalized_prior _ (restrict_nonneg p hp.1 H) (by rwa [restrict_mass])
84 
85 omit [Fintype I] in
86 theorem restrict_sub (p q : I → ℝ) (H : Finset I) :
87     restrict p H-restrict q H=restrict (p-q) H := by
88   funext i
89   simp only [restrict,Pi.sub_apply]
90   split_ifs <;> simp
91 
92 theorem l1_restrict (x : I → ℝ) (H : Finset I) : l1 (restrict x H)=∑ i ∈ H, |x i| := by
93   simp [l1,restrict,apply_ite abs]
94 
95 theorem restriction_complement (x : I → ℝ) (H : Finset I) :
96     l1 (restrict x H)+l1 (restrict x Hᶜ)=l1 x := by
97   rw [l1_restrict,l1_restrict]
98   exact Finset.sum_add_sum_compl H (fun i => |x i|)
99 
100 theorem event_complement (x : I → ℝ) (H : Finset I) :
101     eventMass x H+eventMass x Hᶜ=mass x := by
102   simpa only [eventMass,mass_apply] using Finset.sum_add_sum_compl H x
103 
104 omit [Fintype I] [DecidableEq I] in
105 theorem eventMass_sub (p q : I → ℝ) (H : Finset I) :
106     eventMass (p-q) H=eventMass p H-eventMass q H := by
107   simp only [eventMass,Pi.sub_apply,Finset.sum_sub_distrib]
108 
109 /-- The omitted complement contributes at least the difference of event masses. -/
110 theorem restriction_budget (p q : I → ℝ) (hp : IsPrior p) (hq : IsPrior q) (H : Finset I) :
111     l1 (restrict p H-restrict q H)+|eventMass p H-eventMass q H| ≤ l1 (p-q) := by
112   have hm : mass (p-q)=0 := by rw [map_sub,mass_prior p hp,mass_prior q hq]; ring
113   have hc := event_complement (p-q) H
114   rw [hm,eventMass_sub,eventMass_sub] at hc
115   have ha := abs_mass_le_l1 (restrict (p-q) Hᶜ)
116   rw [restrict_mass,eventMass_sub] at ha
117   have he : eventMass p Hᶜ-eventMass q Hᶜ= -(eventMass p H-eventMass q H) := by linarith
118   rw [he,abs_neg] at ha
119   rw [restrict_sub]
120   linarith [restriction_complement (p-q) H]
121 
122 theorem event_difference_le_distance (p q : I → ℝ) (hp : IsPrior p) (hq : IsPrior q)
123     (H : Finset I) : |eventMass p H-eventMass q H| ≤ distance p q := by
124   have hb := restriction_budget p q hp hq H
125   have ha := abs_mass_le_l1 (restrict (p-q) H)
126   rw [restrict_mass,eventMass_sub] at ha
127   rw [restrict_sub] at hb
128   unfold distance
129   linarith
130 
131 end Events
132 
133 section Marginals
134 variable {J : Type*} [Fintype J] [DecidableEq J]
135 
136 theorem aggregate_l1_le (c : I → J) (x : I → ℝ) : l1 (aggregate c x) ≤ l1 x := by
137   calc
138     l1 (aggregate c x) ≤ ∑ j, ∑ i, |if c i=j then x i else 0| := by
139       apply Finset.sum_le_sum
140       intro j _
141       exact Finset.abs_sum_le_sum_abs _ _
142     _ = l1 x := by
143       rw [Finset.sum_comm]
144       simp [l1,apply_ite abs]
145 
146 omit [Fintype J] in
147 theorem aggregate_sub (c : I → J) (p q : I → ℝ) :
148     aggregate c p-aggregate c q=aggregate c (p-q) := by
149   funext j
150   simp only [aggregate,Pi.sub_apply,← Finset.sum_sub_distrib]
151   apply Finset.sum_congr rfl
152   intro i _
153   split_ifs <;> simp
154 
155 /-- Forgetting part of a finite record cannot increase total variation. -/
156 theorem distance_aggregate_le (c : I → J) (p q : I → ℝ) :
157     distance (aggregate c p) (aggregate c q) ≤ distance p q := by
158   unfold distance
159   rw [aggregate_sub]
160   exact div_le_div_of_nonneg_right (aggregate_l1_le c (p-q)) (by norm_num)
161 
162 end Marginals
163 end Komorebi.LSM.FiniteTV

Back to source controls