ReducingPackets.lean

1 import KomorebiPaperVI.Semigroups
2 
3 /-! Author: Komorebi P. From vanishing generator blocks to independent exponential evolution. -/
4 namespace KomorebiPaperVI.ReducingPackets
5 open KomorebiPaperVI.Semigroups
6 open scoped BigOperators
7 variable {R I : Type*} [Fintype I]
8 
9 section Ring
10 variable [Ring R]
11 
12 theorem generator_commutes (P : I → R) (hP : ∑ a, P a=1) (A : R)
13     (h : ∀ b a, b≠a → P b*A*P a=0) (a : I) : P a*A=A*P a := by
14   classical
15   have hl : A*P a=P a*A*P a := by
16     calc
17       _ = (∑ b, P b)*A*P a := by rw [hP,one_mul]
18       _ = ∑ b, P b*A*P a := by rw [Finset.sum_mul,Finset.sum_mul]
19       _ = _ := Finset.sum_eq_single a (fun b _ hb => h b a hb) (by simp)
20   have hr : P a*A=P a*A*P a := by
21     calc
22       _ = P a*A*(∑ b, P b) := by rw [hP,mul_one]
23       _ = ∑ b, P a*A*P b := by rw [Finset.mul_sum]
24       _ = _ := Finset.sum_eq_single a (fun b _ hb => h a b hb.symm) (by simp)
25   exact hr.trans hl.symm
26 
27 end Ring
28 
29 section Exponential
30 variable [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R]
31 
32 theorem reducing_exponential (P : I → R) (hP : ∑ a, P a=1)
33     (ho : ∀ b a, b≠a → P b*P a=0) (A : R)
34     (h : ∀ b a, b≠a → P b*A*P a=0) (t : ℝ) (b a : I) (hba : b≠a) :
35     P b*transfer A t*P a=0 := by
36   rw [transfer_intertwining (P b) A A (generator_commutes P hP A h b) t,
37     mul_assoc,ho b a hba,mul_zero]
38 
39 theorem compressed_evolution (P : I → R) (hP : ∑ a, P a=1)
40     (hi : ∀ a, P a*P a=P a) (A : R)
41     (h : ∀ b a, b≠a → P b*A*P a=0) (t : ℝ) (a : I) :
42     P a*transfer A t*P a=transfer (P a*A*P a) t*P a := by
43   have hc := generator_commutes P hP A h a
44   have he : P a*A=(P a*A*P a)*P a := by
45     calc
46       _ = A*(P a*P a) := by rw [hi, hc]
47       _ = P a*A*P a := by rw [← mul_assoc,← hc]
48       _ = _ := by rw [mul_assoc (P a*A),hi]
49   rw [transfer_intertwining (P a) A (P a*A*P a) he t,mul_assoc,hi]
50 
51 end Exponential
52 end KomorebiPaperVI.ReducingPackets

Back to source controls