ConditionalExpectation.lean

1 import KomorebiPaperVI.Coarsening
2 import Mathlib.Analysis.Complex.Basic
3 
4 /-! Author: Komorebi P. Literal finite complex weighted conditional expectations. -/
5 namespace KomorebiPaperVI.ConditionalExpectation
6 open KomorebiPaperVI.Coarsening
7 open scoped BigOperators ComplexConjugate
8 variable {I A B : Type*} [Fintype I]
9     [DecidableEq A] [DecidableEq B]
10 
11 def fiber (f : I → A) (v : I → ℂ) (a : A) : ℂ := ∑ i, if f i=a then v i else 0
12 noncomputable def average (f : I → A) (p : I → ℝ) (v : I → ℂ) (a : A) : ℂ :=
13   fiber f (fun i => (p i:ℂ)*v i) a / (coarsen f p a:ℂ)
14 noncomputable def expect (f : I → A) (p : I → ℝ) (v : I → ℂ) (i : I) : ℂ :=
15   average f p v (f i)
16 
17 theorem fiber_mass_cast (f : I → A) (p : I → ℝ) (a : A) :
18     fiber f (fun i => (p i:ℂ)) a=(coarsen f p a:ℂ) := by
19   simp only [fiber,coarsen,Complex.ofReal_sum]
20   apply Finset.sum_congr rfl
21   intro i _; split_ifs <;> simp
22 
23 theorem fiber_pull (f : I → A) (w : I → ℂ) (v : A → ℂ) (a : A) :
24     fiber f (fun i => w i*v (f i)) a=fiber f w a*v a := by
25   simp only [fiber,Finset.sum_mul]
26   apply Finset.sum_congr rfl
27   intro i _
28   by_cases hi : f i=a
29   · simp [hi]
30   · simp [hi]
31 
32 theorem fiber_mass_ne (f : I → A) (p : I → ℝ) (hp : ∀ i, 0 < p i) (i : I) :
33     (coarsen f p (f i):ℂ)≠0 := by
34   intro h
35   have hr : coarsen f p (f i)=0 := by exact_mod_cast h
36   have hz := zero_packet_component f p (fun j => (hp j).le) (f i) hr i rfl
37   exact (hp i).ne' hz
38 
39 theorem expect_constant (f : I → A) (p : I → ℝ) (hp : ∀ i, 0 < p i) (v : A → ℂ) :
40     expect f p (v ∘ f)=v ∘ f := by
41   funext i
42   dsimp [expect,average,Function.comp_def]
43   rw [fiber_pull,fiber_mass_cast]
44   exact mul_div_cancel_left₀ _ (fiber_mass_ne f p hp i)
45 
46 theorem expect_block_constant (f : I → A) (p : I → ℝ) (v : I → ℂ) (i j : I)
47     (h : f i=f j) : expect f p v i=expect f p v j := by simp only [expect,h]
48 
49 theorem expect_idempotent (f : I → A) (p : I → ℝ) (hp : ∀ i, 0 < p i) (v : I → ℂ) :
50     expect f p (expect f p v)=expect f p v :=
51   expect_constant f p hp (average f p v)
52 
53 theorem expect_fixes_iff (f : I → A) (p : I → ℝ) (hp : ∀ i, 0 < p i) (v : I → ℂ) :
54     expect f p v=v ↔ ∀ i j, f i=f j → v i=v j := by
55   constructor
56   · intro h i j hij
57     rw [← h]
58     exact expect_block_constant f p v i j hij
59   · intro h
60     funext i
61     have he : fiber f (fun j => (p j:ℂ)*v j) (f i)=
62         (coarsen f p (f i):ℂ)*v i := by
63       rw [← fiber_mass_cast]
64       simp only [fiber,Finset.sum_mul]
65       apply Finset.sum_congr rfl
66       intro j _
67       by_cases hj : f j=f i
68       · simp [hj,h j i hj]
69       · simp [hj]
70     dsimp [expect,average]
71     rw [he]
72     exact mul_div_cancel_left₀ _ (fiber_mass_ne f p hp i)
73 
74 theorem expect_range (f : I → A) (p : I → ℝ) (hp : ∀ i, 0 < p i) :
75     Set.range (expect f p) = {v | ∀ i j, f i=f j → v i=v j} := by
76   ext v
77   constructor
78   · rintro ⟨w,rfl⟩; exact expect_block_constant f p w
79   · intro h; exact ⟨v,(expect_fixes_iff f p hp v).mpr h⟩
80 
81 noncomputable def kernel (f : I → A) (p : I → ℝ) : Matrix I I ℂ :=
82   fun i j => if f j=f i then (p j:ℂ)/(coarsen f p (f i):ℂ) else 0
83 
84 theorem expect_matrix (f : I → A) (p : I → ℝ) (v : I → ℂ) :
85     expect f p v=(kernel f p).mulVec v := by
86   funext i
87   simp only [expect,average,fiber,Matrix.mulVec,dotProduct,Finset.sum_div,kernel]
88   apply Finset.sum_congr rfl
89   intro j _
90   by_cases hj : f j=f i
91   · simp only [hj,ite_true]; ring
92   · simp [hj]
93 
94 theorem kernel_weighted_symmetry (f : I → A) (p : I → ℝ) (i j : I) :
95     (p i:ℂ)*kernel f p i j=(p j:ℂ)*conj (kernel f p j i) := by
96   by_cases hij : f j=f i
97   · simp only [kernel,hij,ite_true,div_eq_mul_inv]
98     simp only [map_mul,map_inv₀,Complex.conj_ofReal]
99     ring
100   · simp [kernel,hij,Ne.symm hij]
101 
102 noncomputable def weightedInner (p : I → ℝ) (v w : I → ℂ) : ℂ :=
103   ∑ i, (p i:ℂ)*v i*conj (w i)
104 
105 theorem expect_self_adjoint (f : I → A) (p : I → ℝ) (v w : I → ℂ) :
106     weightedInner p (expect f p v) w=weightedInner p v (expect f p w) := by
107   rw [expect_matrix,expect_matrix]
108   simp only [weightedInner,Matrix.mulVec,dotProduct,Finset.mul_sum,Finset.sum_mul,
109     map_sum,map_mul]
110   rw [Finset.sum_comm]
111   apply Finset.sum_congr rfl
112   intro i _
113   apply Finset.sum_congr rfl
114   intro j _
115   have h := kernel_weighted_symmetry f p j i
116   calc
117     _ = ((p j:ℂ)*kernel f p j i)*v i*conj (w j) := by ring
118     _ = _ := by rw [h]; ring
119 
120 end KomorebiPaperVI.ConditionalExpectation

Back to source controls