MarkovSemigroup.lean

1 import Mathlib.Analysis.Normed.Algebra.MatrixExponential
2 import Mathlib.Analysis.SpecialFunctions.Exponential
3 import Mathlib.Tactic
4 
5 /-! Author: Komorebi P. Entrywise positivity and column conservation for actual matrix exponentials. -/
6 namespace KomorebiPaperVI.MarkovSemigroup
7 open scoped BigOperators Matrix.Norms.Operator
8 open NormedSpace
9 set_option backward.isDefEq.respectTransparency false
10 variable {I : Type*} [Fintype I] [DecidableEq I]
11 
12 theorem matrix_powers_nonnegative (M : Matrix I I ℝ) (hM : ∀ i j, 0 ≤ M i j)
13     (n : ℕ) (i j : I) : 0 ≤ (M^n) i j := by
14   induction n generalizing i j with
15   | zero => simp only [pow_zero,Matrix.one_apply]; split_ifs <;> norm_num
16   | succ n ih =>
17     rw [pow_succ,Matrix.mul_apply]
18     exact Finset.sum_nonneg (fun k _ => mul_nonneg (ih i k) (hM k j))
19 
20 theorem exponential_nonnegative (M : Matrix I I ℝ) (hM : ∀ i j, 0 ≤ M i j) (i j : I) :
21     0 ≤ exp M i j := by
22   have hm := expSeries_summable' (𝕂 := ℝ) M
23   rw [exp_eq_tsum ℝ]
24   change 0 ≤ (∑' n : ℕ, ((n.factorial:ℝ)⁻¹) • M^n) i j
25   rw [Pi.tsum_apply hm,Pi.tsum_apply (Pi.summable.mp hm i)]
26   simp only [Matrix.smul_apply,smul_eq_mul]
27   exact tsum_nonneg (fun n => mul_nonneg (by positivity) (matrix_powers_nonnegative M hM n i j))
28 
29 theorem shifted_generator_nonnegative (Q : Matrix I I ℝ)
30     (hQ : ∀ i j, i≠j → 0 ≤ Q i j) :
31     ∀ i j, 0 ≤ (Q+(∑ k, |Q k k|) • (1 : Matrix I I ℝ)) i j := by
32   intro i j
33   by_cases hij : i=j
34   · subst j
35     have h := Finset.single_le_sum (fun k _ => abs_nonneg (Q k k)) (Finset.mem_univ i)
36     simp only [Matrix.add_apply,Matrix.smul_apply,Matrix.one_apply_eq,smul_eq_mul,mul_one]
37     linarith [neg_le_abs (Q i i)]
38   · simpa [hij] using hQ i j hij
39 
40 theorem scalar_exponential (s : ℝ) : exp (s • (1 : Matrix I I ℝ))=Real.exp s • 1 := by
41   have he : s • (1 : Matrix I I ℝ)=Matrix.diagonal (fun _ => s) := by
42     ext i j; by_cases hij : i=j <;> simp [hij,Matrix.diagonal]
43   rw [he,Matrix.exp_diagonal]
44   ext i j
45   simp only [Pi.coe_exp,← Real.exp_eq_exp_ℝ,Matrix.diagonal_apply,Matrix.smul_apply,Matrix.one_apply,smul_eq_mul]
46   split_ifs <;> simp
47 
48 theorem markov_nonnegative (Q : Matrix I I ℝ) (hQ : ∀ i j, i≠j → 0 ≤ Q i j)
49     (t : ℝ) (ht : 0 ≤ t) (i j : I) : 0 ≤ exp (t • Q) i j := by
50   let a := ∑ k, |Q k k|
51   let B := Q+a • (1 : Matrix I I ℝ)
52   have hb : ∀ i j, 0 ≤ (t • B) i j :=
53     fun i j => mul_nonneg ht (shifted_generator_nonnegative Q hQ i j)
54   have he : t • Q=(-t*a) • (1 : Matrix I I ℝ)+t • B := by
55     dsimp [B]
56     module
57   have hc : Commute ((-t*a) • (1 : Matrix I I ℝ)) (t • B) :=
58     (Commute.one_left _).smul_left _
59   rw [he,Matrix.exp_add_of_commute _ _ hc,scalar_exponential]
60   simp only [Algebra.smul_mul_assoc,one_mul,Matrix.smul_apply,smul_eq_mul]
61   exact mul_nonneg (Real.exp_pos _).le (exponential_nonnegative (t • B) hb i j)
62 
63 theorem generator_power_columns (Q : Matrix I I ℝ) (hQ : ∀ j, ∑ i, Q i j=0)
64     (n : ℕ) (j : I) : (∑ i, (Q^n) i j)=if n=0 then 1 else 0 := by
65   cases n with
66   | zero => simp [Matrix.one_apply]
67   | succ n =>
68     simp only [pow_succ',Matrix.mul_apply,Finset.sum_comm,← Finset.sum_mul,hQ,zero_mul,
69       Finset.sum_const_zero,Nat.add_eq_zero_iff,Nat.one_ne_zero,and_false,ite_false]
70 
71 theorem markov_column_sum (Q : Matrix I I ℝ) (hQ : ∀ j, ∑ i, Q i j=0)
72     (t : ℝ) (j : I) : (∑ i, exp (t • Q) i j)=1 := by
73   have hc : ∀ j, ∑ i, (t • Q) i j=0 := by
74     intro j; simp [Matrix.smul_apply,smul_eq_mul,← Finset.mul_sum,hQ]
75   have hm := expSeries_summable' (𝕂 := ℝ) (t • Q)
76   rw [exp_eq_tsum ℝ]
77   simp only [Pi.tsum_apply hm,Pi.tsum_apply (Pi.summable.mp hm _),Matrix.smul_apply,smul_eq_mul]
78   have hs (i : I) : Summable (fun n : ℕ => ((n.factorial:ℝ)⁻¹)*((t • Q)^n) i j) := by
79     exact Pi.summable.mp (Pi.summable.mp hm i) j
80   rw [← Summable.tsum_finsetSum (s := Finset.univ) (fun i _ => hs i)]
81   simp only [← Finset.mul_sum,generator_power_columns _ hc]
82   simp
83 
84 theorem markov_probability (Q : Matrix I I ℝ) (hpos : ∀ i j, i≠j → 0 ≤ Q i j)
85     (hcol : ∀ j, ∑ i, Q i j=0) (p : I → ℝ) (hp : ∀ i, 0 ≤ p i)
86     (hpsum : ∑ i, p i=1) (t : ℝ) (ht : 0 ≤ t) :
87     (∀ i, 0 ≤ (exp (t • Q)).mulVec p i) ∧ ∑ i, (exp (t • Q)).mulVec p i=1 := by
88   constructor
89   · intro i
90     exact Finset.sum_nonneg (fun j _ => mul_nonneg (markov_nonnegative Q hpos t ht i j) (hp j))
91   · simp only [Matrix.mulVec,dotProduct,Finset.sum_comm,← Finset.sum_mul,markov_column_sum Q hcol,
92       one_mul,hpsum]
93 
94 end KomorebiPaperVI.MarkovSemigroup

Back to source controls