NormalizedDefect.lean

1 import KomorebiLSM.PositivePriors
2 
3 /-! P36: likelihood error and normalized state error are distinct.
4 The all-interior-prior converse is derived using explicit spanning priors. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.FiniteInstruments
7 open scoped BigOperators
8 open FiniteBayes
9 universe u v
10 
11 section Algebra
12 variable {E : Type*} [AddCommGroup E] [Module ℝ E]
13 
14 /-- The rank-one mass component is removed after normalization. -/
15 def oblique (l : E →ₗ[ℝ] ℝ) (q : E) : E →ₗ[ℝ] E :=
16   LinearMap.id - l.smulRight q
17 
18 @[simp] theorem oblique_apply (l : E →ₗ[ℝ] ℝ) (q x : E) :
19     oblique l q x = x - l x • q := rfl
20 
21 theorem oblique_null (l : E →ₗ[ℝ] ℝ) (q : E) (hq : l q = 1) :
22     oblique l q q = 0 := by
23   simp [hq]
24 
25 theorem oblique_mass_zero (l : E →ₗ[ℝ] ℝ) (q : E) (hq : l q = 1) (x : E) :
26     l (oblique l q x) = 0 := by
27   simp [map_sub, hq]
28 
29 theorem oblique_idempotent (l : E →ₗ[ℝ] ℝ) (q : E) (hq : l q = 1) :
30     (oblique l q).comp (oblique l q) = oblique l q := by
31   ext x
32   change oblique l q (oblique l q x) = oblique l q x
33   rw [oblique_apply, oblique_mass_zero l q hq, zero_smul, sub_zero]
34 
35 variable {X : Type*} [AddCommGroup X] [Module ℝ X]
36 
37 def closureDefect (R : X →ₗ[ℝ] E) (M : X →ₗ[ℝ] X) (B : E →ₗ[ℝ] E) :
38     X →ₗ[ℝ] E := R.comp M - B.comp R
39 
40 @[simp] theorem closureDefect_apply (R : X →ₗ[ℝ] E) (M : X →ₗ[ℝ] X)
41     (B : E →ₗ[ℝ] E) (p : X) : closureDefect R M B p = R (M p) - B (R p) := rfl
42 
43 theorem closureDefect_zero_iff (R : X →ₗ[ℝ] E) (M : X →ₗ[ℝ] X)
44     (B : E →ₗ[ℝ] E) : closureDefect R M B = 0 ↔ R.comp M = B.comp R := sub_eq_zero
45 
46 theorem normalize_transport (R : X →ₗ[ℝ] E) (mu : X →ₗ[ℝ] ℝ)
47     (l : E →ₗ[ℝ] ℝ) (h : l.comp R = mu) (x : X) :
48     R (normalize mu x) = normalize l (R x) := by
49   have hx : l (R x) = mu x := congrArg (fun f : X →ₗ[ℝ] ℝ => f x) h
50   simp only [normalize, map_smul, hx]
51 
52 theorem likelihood_defect (R : X →ₗ[ℝ] E) (M : X →ₗ[ℝ] X) (B : E →ₗ[ℝ] E)
53     (mu : X →ₗ[ℝ] ℝ) (l : E →ₗ[ℝ] ℝ) (h : l.comp R = mu) (p : X) :
54     mu (M p) - l (B (R p)) = l (closureDefect R M B p) := by
55   have hx : l (R (M p)) = mu (M p) := congrArg (fun f : X →ₗ[ℝ] ℝ => f (M p)) h
56   simp [hx]
57 
58 end Algebra
59 
60 section CoordinateIdentity
61 variable {J : Type v}
62 
63 /-- A vector identity with both denominators declared nonzero. -/
64 theorem normalized_difference (l : (J → ℝ) →ₗ[ℝ] ℝ) (u v : J → ℝ)
65     (hu : l u ≠ 0) (hv : l v ≠ 0) :
66     normalize l u - normalize l v =
67       (l u)⁻¹ • oblique l (normalize l v) (u-v) := by
68   funext j
69   simp only [normalize, oblique_apply, map_sub, Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
70   field_simp
71   ring
72 
73 /-- P36's vector defect, including transport from the fine normalized state. -/
74 theorem normalized_closure_defect {I : Type u} [Fintype I]
75     (R : (I → ℝ) →ₗ[ℝ] (J → ℝ)) (M : (I → ℝ) →ₗ[ℝ] (I → ℝ))
76     (B : (J → ℝ) →ₗ[ℝ] (J → ℝ)) (l : (J → ℝ) →ₗ[ℝ] ℝ)
77     (hmass : l.comp R = mass) (p : I → ℝ)
78     (ha : 0 < mass (M p)) (hb : 0 < l (B (R p))) :
79     R (normalize mass (M p)) - normalize l (B (R p)) =
80       (mass (M p))⁻¹ • oblique l (normalize l (B (R p))) (closureDefect R M B p) := by
81   have hx : l (R (M p)) = mass (M p) :=
82     congrArg (fun f : (I → ℝ) →ₗ[ℝ] ℝ => f (M p)) hmass
83   rw [normalize_transport R mass l hmass]
84   have hd := normalized_difference l (R (M p)) (B (R p))
85     (by rw [hx]; exact ne_of_gt ha) (ne_of_gt hb)
86   simpa only [hx, closureDefect_apply] using hd
87 
88 end CoordinateIdentity
89 
90 section Converse
91 variable {I : Type u} [Fintype I] [Nonempty I]
92 variable {E : Type*} [AddCommGroup E] [Module ℝ E]
93 
94 /-- Matching likelihood and posterior on every interior belief forces actual closure. -/
95 theorem closure_of_likelihood_and_posterior
96     (M : Matrix I I ℝ) (hM : ∀ j i, 0 ≤ M j i) (h0 : M ≠ 0)
97     (R : (I → ℝ) →ₗ[ℝ] E) (B : E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
98     (hlik : ∀ p, IsStrictPrior p → mass (M.mulVecLin p) = l (B (R p)))
99     (hpost : ∀ p, IsStrictPrior p →
100       R (normalize mass (M.mulVecLin p)) = normalize l (B (R p))) :
101     R.comp M.mulVecLin = B.comp R := by
102   apply linearMap_eq_of_strict_priors
103   intro p hp
104   have ha := nonnegative_branch_mass_pos M hM h0 p hp.2
105   have hb : l (B (R p)) ≠ 0 := by rw [← hlik p hp]; exact ne_of_gt ha
106   change R (M.mulVecLin p) = B (R p)
107   calc
108     R (M.mulVecLin p) = R (mass (M.mulVecLin p) • normalize mass (M.mulVecLin p)) :=
109       congrArg R (recover_from_normalize mass _ (ne_of_gt ha)).symm
110     _ = mass (M.mulVecLin p) • R (normalize mass (M.mulVecLin p)) := map_smul R _ _
111     _ = l (B (R p)) • normalize l (B (R p)) := by rw [hlik p hp, hpost p hp]
112     _ = B (R p) := recover_from_normalize l _ hb
113 
114 end Converse
115 
116 section Packet
117 variable {X : Type*} [AddCommGroup X] [Module ℝ X]
118 
119 /-- The probability defect reduces to the omitted-to-retained transfer block. -/
120 theorem closureDefect_projected (P M : X →ₗ[ℝ] X) (hP : P.comp P = P) :
121     closureDefect P M (P.comp (M.comp P)) = P.comp (M.comp (LinearMap.id-P)) := by
122   ext x
123   have hx : P (P x) = P x := congrArg (fun F : X →ₗ[ℝ] X => F x) hP
124   simp [closureDefect, LinearMap.comp_apply, hx, map_sub]
125 
126 end Packet
127 end Komorebi.LSM.FiniteInstruments

Back to source controls