ConditionalTowers.lean

1 import KomorebiPaperVI.ConditionalExpectation
2 import KomorebiPaperVI.Algebra
3 import KomorebiPaperVI.MartingalePackets
4 
5 /-! Author: Komorebi P. Concrete conditional-expectation towers and martingale packets. -/
6 namespace KomorebiPaperVI.ConditionalTowers
7 open KomorebiPaperVI.ConditionalExpectation
8 open scoped BigOperators ComplexConjugate
9 variable {I A B : Type*} [Fintype I] [DecidableEq A] [DecidableEq B]
10 
11 theorem weighted_inner_separates (p : I → ℝ) (hp : ∀ i, 0 < p i) (v w : I → ℂ)
12     (h : ∀ z, weightedInner p v z=weightedInner p w z) : v=w := by
13   classical
14   funext i
15   have he := h (fun j => if j=i then 1 else 0)
16   simp [weightedInner] at he
17   exact he.resolve_right (hp i).ne'
18 
19 theorem fine_after_coarse (f : I → A) (g : A → B) (p : I → ℝ) (hp : ∀ i, 0 < p i)
20     (v : I → ℂ) : expect f p (expect (g ∘ f) p v)=expect (g ∘ f) p v := by
21   apply (expect_fixes_iff f p hp _).mpr
22   intro i j hij
23   apply expect_block_constant
24   simp only [Function.comp_apply,hij]
25 
26 theorem coarse_after_fine (f : I → A) (g : A → B) (p : I → ℝ) (hp : ∀ i, 0 < p i)
27     (v : I → ℂ) : expect (g ∘ f) p (expect f p v)=expect (g ∘ f) p v := by
28   apply weighted_inner_separates p hp
29   intro w
30   rw [expect_self_adjoint,expect_self_adjoint,fine_after_coarse f g p hp,
31     ← expect_self_adjoint]
32 
33 section Matrix
34 variable [DecidableEq I]
35 
36 omit [DecidableEq I] in
37 theorem conditional_kernel_product (f : I → A) (g : A → B) (p : I → ℝ)
38     (hp : ∀ i, 0 < p i) :
39     kernel (g ∘ f) p*kernel f p=kernel (g ∘ f) p ∧
40       kernel f p*kernel (g ∘ f) p=kernel (g ∘ f) p := by
41   constructor
42   · apply Matrix.mulVec_injective
43     funext v
44     rw [← Matrix.mulVec_mulVec,← expect_matrix,← expect_matrix,coarse_after_fine f g p hp,expect_matrix]
45   · apply Matrix.mulVec_injective
46     funext v
47     rw [← Matrix.mulVec_mulVec,← expect_matrix,← expect_matrix,fine_after_coarse f g p hp,expect_matrix]
48 
49 
50 variable {J : ℕ → Type*} [∀ n, DecidableEq (J n)]
51 
52 omit [DecidableEq I] in
53 theorem nested_kernel_min (f : ∀ n, I → J n) (p : I → ℝ) (hp : ∀ i, 0 < p i)
54     (hf : ∀ m n, m ≤ n → ∃ g : J n → J m, f m=g ∘ f n) (m n : ℕ) :
55     kernel (f m) p*kernel (f n) p=kernel (f (min m n)) p := by
56   by_cases hmn : m ≤ n
57   · obtain ⟨g,hg⟩ := hf m n hmn
58     rw [Nat.min_eq_left hmn,hg]
59     exact (conditional_kernel_product (f n) g p hp).1
60   · have hnm : n ≤ m := by omega
61     obtain ⟨g,hg⟩ := hf n m hnm
62     rw [Nat.min_eq_right hnm,hg]
63     exact (conditional_kernel_product (f m) g p hp).2
64 
65 theorem martingale_packet_product (f : ∀ n, I → J n) (p : I → ℝ) (hp : ∀ i, 0 < p i)
66     (hf : ∀ m n, m ≤ n → ∃ g : J n → J m, f m=g ∘ f n) (m n : ℕ) :
67     MartingalePackets.packet (fun k => kernel (f k) p) m *
68       MartingalePackets.packet (fun k => kernel (f k) p) n =
69         if m=n then MartingalePackets.packet (fun k => kernel (f k) p) n else 0 :=
70   MartingalePackets.packet_product _ (nested_kernel_min f p hp hf) m n
71 
72 theorem martingale_packet_reconstruction (f : ∀ n, I → J n) (p : I → ℝ) (n : ℕ) :
73     ∑ j ∈ Finset.range (n+1), MartingalePackets.packet (fun k => kernel (f k) p) j=kernel (f n) p :=
74   MartingalePackets.packet_sum _ n
75 
76 end Matrix
77 end KomorebiPaperVI.ConditionalTowers

Back to source controls