MartingalePackets.lean

1 import KomorebiPaperVI.Algebra
2 
3 /-! Author: Komorebi P. All pairwise difference identities for a nested projector tower. -/
4 namespace KomorebiPaperVI.MartingalePackets
5 open scoped BigOperators
6 variable {R : Type*} [Ring R]
7 
8 def packet (P : ℕ → R) : ℕ → R
9   | 0 => P 0
10   | n+1 => P (n+1)-P n
11 
12 theorem packet_product (P : ℕ → R) (h : ∀ i j, P i*P j=P (min i j)) (i j : ℕ) :
13     packet P i*packet P j=if i=j then packet P j else 0 := by
14   cases i with
15   | zero =>
16     cases j with
17     | zero => simp [packet,h]
18     | succ j => simp [packet,mul_sub,h]
19   | succ i =>
20     cases j with
21     | zero => simp [packet,sub_mul,h]
22     | succ j =>
23       by_cases hij : i=j
24       · subst j
25         simp only [packet,sub_mul,mul_sub,h,Nat.min_self,ite_true,
26           Nat.min_eq_left (Nat.le_succ i),Nat.min_eq_right (Nat.le_succ i)]
27         abel
28       · rcases lt_or_gt_of_ne hij with hij' | hji'
29         · have h1 : i+1 ≤ j := hij'
30           have h2 : i+1 ≤ j+1 := by omega
31           have h3 : i ≤ j+1 := by omega
32           simp [packet,sub_mul,mul_sub,h,Nat.min_eq_left h1,Nat.min_eq_left h2,
33             Nat.min_eq_left h3,Nat.min_eq_left hij'.le,hij]
34         · have h1 : j+1 ≤ i := hji'
35           have h2 : j+1 ≤ i+1 := by omega
36           have h3 : j ≤ i+1 := by omega
37           simp [packet,sub_mul,mul_sub,h,Nat.min_eq_right h1,Nat.min_eq_right h2,
38             Nat.min_eq_right h3,Nat.min_eq_right hji'.le,hij]
39 
40 theorem packet_sum (P : ℕ → R) (n : ℕ) : ∑ j ∈ Finset.range (n+1), packet P j=P n := by
41   induction n with
42   | zero => simp [packet]
43   | succ n ih => rw [Finset.sum_range_succ,ih,packet]; abel
44 
45 end KomorebiPaperVI.MartingalePackets

Back to source controls