Algebra.lean

1 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
2 import Mathlib.Tactic
3 
4 /-! Author: Komorebi P. Exact packet and rectangular refinement identities. -/
5 namespace KomorebiPaperVI.Algebra
6 open scoped BigOperators
7 
8 variable {R I : Type*} [Ring R] [Fintype I]
9 
10 def block (P : I → R) (A : R) (b a : I) : R := P b * A * P a
11 
12 theorem block_reconstruction (P : I → R) (hP : ∑ i, P i = 1) (A : R) :
13     ∑ b, ∑ a, block P A b a = A := by
14   simp only [block, ← Finset.mul_sum, hP, mul_one, ← Finset.sum_mul, one_mul]
15 
16 theorem block_multiplication (P : I → R) (hP : ∑ i, P i = 1)
17     (hid : ∀ i, P i * P i = P i) (A B : R) (b a : I) :
18     block P (A*B) b a = ∑ c, block P A b c * block P B c a := by
19   have term (c : I) : block P A b c * block P B c a =
20       P b * A * P c * B * P a := by
21     dsimp [block]
22     calc
23       _ = P b * A * (P c * P c) * B * P a := by noncomm_ring
24       _ = _ := by rw [hid]
25   simp_rw [term]
26   simp only [← Finset.sum_mul, ← Finset.mul_sum, hP, block, mul_assoc, one_mul]
27 
28 theorem packet_semigroup_convolution (P : I → R) (hP : ∑ i, P i = 1)
29     (hid : ∀ i, P i * P i = P i) (T : ℝ → R)
30     (hT : ∀ s t, T (s+t) = T s*T t) (s t : ℝ) (b a : I) :
31     block P (T (s+t)) b a = ∑ c, block P (T s) b c * block P (T t) c a := by
32   rw [hT]
33   exact block_multiplication P hP hid _ _ _ _
34 
35 theorem difference_idempotent (P Q : R) (hP : P*P=P) (hQ : Q*Q=Q)
36     (hPQ : P*Q=P) (hQP : Q*P=P) : (Q-P)*(Q-P)=Q-P := by
37   noncomm_ring [hP,hQ,hPQ,hQP]
38 
39 theorem difference_annihilates_coarse (P Q : R) (hP : P*P=P)
40     (hPQ : P*Q=P) (hQP : Q*P=P) :
41     P*(Q-P)=0 ∧ (Q-P)*P=0 := by
42   constructor <;> noncomm_ring [hP,hPQ,hQP]
43 
44 theorem tower_telescope (P : ℕ → R) (n : ℕ) :
45     P 0 + ∑ j ∈ Finset.range n, (P (j+1)-P j) = P n := by
46   induction n with
47   | zero => simp
48   | succ n ih => rw [Finset.sum_range_succ]; rw [← add_assoc, ih]; abel
49 
50 section Rectangular
51 variable {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
52 
53 theorem intertwining_powers (C : Matrix m n R) (A : Matrix n n R) (B : Matrix m m R)
54     (h : C*A=B*C) (k : ℕ) : C*A^k=B^k*C := by
55   induction k with
56   | zero => simp
57   | succ k ih =>
58     calc
59       C*A^(k+1) = (C*A^k)*A := by rw [pow_succ, Matrix.mul_assoc]
60       _ = (B^k*C)*A := by rw [ih]
61       _ = (B^k*B)*C := by rw [Matrix.mul_assoc, h, ← Matrix.mul_assoc]
62       _ = B^(k+1)*C := by rw [pow_succ]
63 
64 theorem finite_horizon_defect (C : Matrix m n R) (A : Matrix n n R) (B : Matrix m m R)
65     (k : ℕ) :
66     C*A^k-B^k*C = ∑ j ∈ Finset.range k, B^(k-1-j)*(C*A-B*C)*A^j := by
67   induction k with
68   | zero => simp
69   | succ k ih =>
70     rw [Finset.sum_range_succ]
71     have hs : (∑ j ∈ Finset.range k, B^(k+1-1-j)*(C*A-B*C)*A^j) =
72         B*(∑ j ∈ Finset.range k, B^(k-1-j)*(C*A-B*C)*A^j) := by
73       rw [Matrix.mul_sum]
74       apply Finset.sum_congr rfl
75       intro j hj
76       have hjk := Finset.mem_range.mp hj
77       have he : k+1-1-j = (k-1-j)+1 := by omega
78       rw [he, pow_succ']
79       simp only [Matrix.mul_assoc]
80     rw [hs, ← ih]
81     simp only [Nat.add_sub_cancel, Nat.sub_self, pow_zero, Matrix.one_mul]
82     simp only [pow_succ', Matrix.mul_sub, Matrix.sub_mul, Matrix.mul_assoc]
83     abel
84 
85 theorem rectangular_resolvent_identity (C : Matrix m n R)
86     (A : Matrix n n R) (B : Matrix m m R)
87     (Rf : Matrix n n R) (Rc : Matrix m m R) (z : R)
88     (hz : ∀ i j, z*C i j = C i j*z)
89     (hf : (Matrix.scalar n z-A)*Rf=1)
90     (hc : Rc*(Matrix.scalar m z-B)=1) :
91     C*Rf-Rc*C=Rc*(C*A-B*C)*Rf := by
92   have hzC : Matrix.scalar m z*C=C*Matrix.scalar n z := by
93     ext i j
94     simpa using hz i j
95   have hd : C*A-B*C=(Matrix.scalar m z-B)*C-C*(Matrix.scalar n z-A) := by
96     rw [Matrix.sub_mul, Matrix.mul_sub, hzC]
97     abel
98   rw [hd, Matrix.mul_sub, Matrix.sub_mul]
99   simp only [← Matrix.mul_assoc, hc, Matrix.one_mul]
100   rw [Matrix.mul_assoc (Rc*C), hf, Matrix.mul_one]
101 
102 end Rectangular
103 end KomorebiPaperVI.Algebra

Back to source controls