Conditioning.lean

1 import KomorebiLSM.FiniteTV
2 
3 /-! P44: conditioning costs an inverse event-probability factor.
4 The proof accounts for the discarded complementary event. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.FiniteTV
7 open scoped BigOperators
8 open FiniteBayes FiniteInstruments
9 variable {I : Type*} [Fintype I]
10 
11 /-- Normalization comparison for actual nonnegative subprobability vectors. -/
12 theorem normalized_l1_bound (u v : I → ℝ) (hv : ∀ i, 0 ≤ v i)
13     (ha : 0<mass u) (hb : 0<mass v) :
14     l1 (normalize mass u-normalize mass v) ≤
15       (l1 (u-v)+|mass u-mass v|)/mass u := by
16   rw [normalized_difference mass u v (ne_of_gt ha) (ne_of_gt hb),l1_smul]
17   rw [abs_inv,abs_of_pos ha]
18   have h := l1_sub_le (u-v) (mass (u-v) • normalize mass v)
19   rw [l1_smul,l1_prior _ (normalized_prior v hv hb),mul_one,map_sub] at h
20   have he := mul_le_mul_of_nonneg_left h (inv_nonneg.mpr ha.le)
21   change (mass u)⁻¹ * l1 ((u-v)-mass (u-v) • normalize mass v) ≤ _
22   rw [map_sub]
23   simpa only [div_eq_mul_inv,mul_comm] using he
24 
25 section Events
26 variable [DecidableEq I]
27 
28 /-- Adequate true event mass forces positive comparison mass. -/
29 theorem comparison_event_positive (p q : I → ℝ) (hp : IsPrior p) (hq : IsPrior q)
30     (H : Finset I) (δ : ℝ) (hδ : distance p q ≤ δ) (hH : δ<eventMass p H) :
31     0<eventMass q H := by
32   have he := (event_difference_le_distance p q hp hq H).trans hδ
33   have hb := (abs_le.mp he).2
34   linarith
35 
36 /-- P44: conditional laws on the same event, with both evidences positive. -/
37 theorem conditioning_tv_bound (p q : I → ℝ) (hp : IsPrior p) (hq : IsPrior q)
38     (H : Finset I) (δ : ℝ) (hδ : distance p q ≤ δ)
39     (hP : 0<eventMass p H) (hQ : 0<eventMass q H) :
40     distance (conditional p H) (conditional q H) ≤ min 1 (δ/eventMass p H) := by
41   apply le_min
42   · exact distance_le_one _ _ (conditional_prior p hp H hP) (conditional_prior q hq H hQ)
43   · have hn := normalized_l1_bound (restrict p H) (restrict q H)
44       (restrict_nonneg q hq.1 H) (by rwa [restrict_mass]) (by rwa [restrict_mass])
45     rw [restrict_mass,restrict_mass] at hn
46     change l1 (conditional p H-conditional q H) ≤
47       (l1 (restrict p H-restrict q H)+|eventMass p H-eventMass q H|)/eventMass p H at hn
48     have hb := restriction_budget p q hp hq H
49     have hm := (le_div_iff₀ hP).mp hn
50     unfold distance at hδ ⊢
51     apply (le_div_iff₀ hP).mpr
52     nlinarith
53 
54 /-- The explicit positivity premise for the comparison event can be discharged by a margin. -/
55 theorem conditioning_tv_bound_of_margin (p q : I → ℝ) (hp : IsPrior p) (hq : IsPrior q)
56     (H : Finset I) (δ : ℝ) (hδ : distance p q ≤ δ) (hP : δ<eventMass p H) :
57     0<eventMass q H ∧
58     distance (conditional p H) (conditional q H) ≤ min 1 (δ/eventMass p H) := by
59   have hQ := comparison_event_positive p q hp hq H δ hδ hP
60   have hd : 0 ≤ δ := (distance_nonneg p q).trans hδ
61   exact ⟨hQ,conditioning_tv_bound p q hp hq H δ hδ (lt_of_le_of_lt hd hP) hQ⟩
62 
63 /-- A deterministic continuation readout cannot increase the conditional bound. -/
64 theorem conditional_readout_bound {J : Type*} [Fintype J] [DecidableEq J]
65     (c : I → J) (p q : I → ℝ) (hp : IsPrior p) (hq : IsPrior q)
66     (H : Finset I) (δ : ℝ) (hδ : distance p q ≤ δ)
67     (hP : 0<eventMass p H) (hQ : 0<eventMass q H) :
68     distance (aggregate c (conditional p H)) (aggregate c (conditional q H)) ≤
69       min 1 (δ/eventMass p H) :=
70   (distance_aggregate_le c _ _).trans (conditioning_tv_bound p q hp hq H δ hδ hP hQ)
71 
72 end Events
73 end Komorebi.LSM.FiniteTV

Back to source controls