SharpConditioning.lean

1 import KomorebiLSM.Conditioning
2 import Mathlib.Tactic.FinCases
3 
4 /-! A parameterized family attains the inverse-event-mass bound exactly. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.FiniteTV
7 open scoped BigOperators
8 open FiniteBayes FiniteInstruments
9 
10 noncomputable def sharpP (r : ℝ) : Fin 3 → ℝ := ![r,0,1-r]
11 noncomputable def sharpQ (r d : ℝ) : Fin 3 → ℝ := ![r-d,d,1-r]
12 def sharpEvent : Finset (Fin 3) := {0,1}
13 
14 theorem sharpP_prior (r : ℝ) (hr : 0 ≤ r) (h1 : r ≤ 1) : IsPrior (sharpP r) := by
15   constructor
16   · intro i; fin_cases i <;> simp [sharpP] <;> linarith
17   · simp [sharpP,Fin.sum_univ_three]
18 
19 theorem sharpQ_prior (r d : ℝ) (h1 : r ≤ 1) (hd : 0 ≤ d) (hdr : d ≤ r) :
20     IsPrior (sharpQ r d) := by
21   constructor
22   · intro i; fin_cases i <;> simp [sharpQ] <;> linarith
23   · simp [sharpQ,Fin.sum_univ_three]
24 
25 theorem sharpP_eventMass (r : ℝ) : eventMass (sharpP r) sharpEvent=r := by
26   simp [eventMass,sharpEvent,sharpP]
27 
28 theorem sharpQ_eventMass (r d : ℝ) : eventMass (sharpQ r d) sharpEvent=r := by
29   simp [eventMass,sharpEvent,sharpQ]
30 
31 theorem sharp_distance (r d : ℝ) (hd : 0 ≤ d) : distance (sharpP r) (sharpQ r d)=d := by
32   have he : sharpP r-sharpQ r d=(![d,-d,0] : Fin 3 → ℝ) := by
33     funext i; fin_cases i <;> simp [sharpP,sharpQ]
34   rw [distance,he]
35   simp [l1,Fin.sum_univ_three,abs_of_nonneg hd]
36 
37 theorem sharpP_conditional (r : ℝ) (hr : 0<r) :
38     conditional (sharpP r) sharpEvent=(![1,0,0] : Fin 3 → ℝ) := by
39   unfold conditional normalize
40   rw [restrict_mass,sharpP_eventMass]
41   funext i
42   fin_cases i <;> simp [restrict,sharpP,sharpEvent,ne_of_gt hr]
43 
44 theorem sharpQ_conditional (r d : ℝ) (hr : 0<r) :
45     conditional (sharpQ r d) sharpEvent=(![1-d/r,d/r,0] : Fin 3 → ℝ) := by
46   unfold conditional normalize
47   rw [restrict_mass,sharpQ_eventMass]
48   funext i
49   fin_cases i <;> simp [restrict,sharpQ,sharpEvent,div_eq_mul_inv] <;> field_simp
50 
51 theorem sharp_conditional_distance (r d : ℝ) (hr : 0<r) (hd : 0 ≤ d) :
52     distance (conditional (sharpP r) sharpEvent) (conditional (sharpQ r d) sharpEvent)=d/r := by
53   rw [sharpP_conditional r hr,sharpQ_conditional r d hr]
54   have he : (![1,0,0] : Fin 3 → ℝ)-![1-d/r,d/r,0]=![d/r,-(d/r),0] := by
55     funext i; fin_cases i <;> simp
56   rw [distance,he]
57   simp [l1,Fin.sum_univ_three,abs_of_nonneg (div_nonneg hd hr.le)]
58 
59 /-- P44's sharpness, for every event mass and every admissible moved mass. -/
60 theorem sharp_conditioning (r d : ℝ) (hr : 0<r) (h1 : r ≤ 1)
61     (hd : 0 ≤ d) (hdr : d ≤ r) :
62     ∃ (p q : Fin 3 → ℝ) (H : Finset (Fin 3)),
63       IsPrior p ∧ IsPrior q ∧ eventMass p H=r ∧ eventMass q H=r ∧
64       distance p q=d ∧ distance (conditional p H) (conditional q H)=d/r :=
65   ⟨sharpP r,sharpQ r d,sharpEvent,sharpP_prior r hr.le h1,sharpQ_prior r d h1 hd hdr,
66     sharpP_eventMass r,sharpQ_eventMass r d,sharp_distance r d hd,
67     sharp_conditional_distance r d hr hd⟩
68 
69 end Komorebi.LSM.FiniteTV

Back to source controls