FeynmanKac.lean

1 import Mathlib.Analysis.SpecialFunctions.Exp
2 import Mathlib.Data.Fintype.BigOperators
3 import Mathlib.LinearAlgebra.Matrix.ToLin
4 import Mathlib.Tactic
5 
6 /-! Author: Komorebi P. Enumerated finite path law and the actual potential-weighted matrix. -/
7 namespace KomorebiPaperVI.FeynmanKac
8 open scoped BigOperators
9 variable {I : Type*} [Fintype I] [DecidableEq I]
10 
11 noncomputable def pathProbability (K : Matrix I I ℝ) : (n : ℕ) → I → (Fin n → I) → ℝ
12   | 0, _, _ => 1
13   | n+1, i, x => K (x 0) i*pathProbability K n (x 0) (Fin.tail x)
14 
15 noncomputable def pathPotential (V : I → ℝ) : (n : ℕ) → I → (Fin n → I) → ℝ
16   | 0, _, _ => 0
17   | n+1, i, x => V i+pathPotential V n (x 0) (Fin.tail x)
18 
19 def terminal : (n : ℕ) → I → (Fin n → I) → I
20   | 0, i, _ => i
21   | n+1, _, x => terminal n (x 0) (Fin.tail x)
22 
23 noncomputable def pathExpectation (K : Matrix I I ℝ) (V f : I → ℝ) (n : ℕ) (i : I) : ℝ :=
24   ∑ x : Fin n → I, pathProbability K n i x*Real.exp (-pathPotential V n i x)*f (terminal n i x)
25 
26 noncomputable def transfer (K : Matrix I I ℝ) (V : I → ℝ) : Matrix I I ℝ :=
27   Matrix.diagonal (fun i => Real.exp (-V i))*K.transpose
28 
29 omit [DecidableEq I] in
30 theorem sum_paths_succ (n : ℕ) (F : (Fin (n+1) → I) → ℝ) :
31     (∑ x, F x)=∑ i, ∑ y : Fin n → I, F (Fin.cons i y) := by
32   have h := (Fin.consEquiv (fun _ : Fin (n+1) => I)).sum_comp F
33   change (∑ x : I × (Fin n → I), F (Fin.cons x.1 x.2))=∑ x : Fin (n+1) → I, F x at h
34   rw [Fintype.sum_prod_type] at h
35   exact h.symm
36 
37 theorem transfer_entry (K : Matrix I I ℝ) (V : I → ℝ) (i j : I) :
38     transfer K V i j=Real.exp (-V i)*K j i := by simp [transfer]
39 
40 omit [Fintype I] [DecidableEq I] in
41 theorem path_probability_nonnegative (K : Matrix I I ℝ) (hK : ∀ i j, 0 ≤ K i j)
42     (n : ℕ) (i : I) (x : Fin n → I) : 0 ≤ pathProbability K n i x := by
43   induction n generalizing i with
44   | zero => exact zero_le_one
45   | succ n ih => exact mul_nonneg (hK _ _) (ih _ _)
46 
47 omit [DecidableEq I] in
48 theorem path_probability_mass (K : Matrix I I ℝ) (hK : ∀ j, ∑ i, K i j=1)
49     (n : ℕ) (i : I) : (∑ x : Fin n → I, pathProbability K n i x)=1 := by
50   induction n generalizing i with
51   | zero => simp [pathProbability]
52   | succ n ih =>
53     rw [sum_paths_succ]
54     simp only [pathProbability,Fin.cons_zero,Fin.tail_cons,← Finset.mul_sum,ih,mul_one,hK]
55 
56 omit [DecidableEq I] in
57 theorem path_expectation_zero (K : Matrix I I ℝ) (V f : I → ℝ) (i : I) :
58     pathExpectation K V f 0 i=f i := by simp [pathExpectation,pathProbability,pathPotential,terminal]
59 
60 omit [DecidableEq I] in
61 theorem path_expectation_step (K : Matrix I I ℝ) (V f : I → ℝ) (n : ℕ) (i : I) :
62     pathExpectation K V f (n+1) i=
63       Real.exp (-V i)*∑ j, K j i*pathExpectation K V f n j := by
64   unfold pathExpectation
65   rw [sum_paths_succ]
66   simp only [pathProbability,pathPotential,terminal,Fin.cons_zero,Fin.tail_cons,neg_add,
67     Real.exp_add,Finset.mul_sum]
68   apply Finset.sum_congr rfl
69   intro j _
70   apply Finset.sum_congr rfl
71   intro x _
72   ring
73 
74 theorem feynman_kac_path_formula (K : Matrix I I ℝ) (V f : I → ℝ) (n : ℕ) :
75     (transfer K V ^ n).mulVec f=pathExpectation K V f n := by
76   induction n with
77   | zero => funext i; simp [path_expectation_zero]
78   | succ n ih =>
79     rw [pow_succ',← Matrix.mulVec_mulVec,ih]
80     funext i
81     rw [path_expectation_step]
82     simp only [Matrix.mulVec,dotProduct,transfer_entry,Finset.mul_sum,mul_assoc]
83 
84 omit [Fintype I] [DecidableEq I] in
85 theorem path_probability_product (K : Matrix I I ℝ) (n : ℕ) (i : I) (x : Fin n → I) :
86     pathProbability K n i x = ∏ r : Fin n,
87       K ((Fin.cons i x : Fin (n+1) → I) r.succ) ((Fin.cons i x : Fin (n+1) → I) r.castSucc) := by
88   induction n generalizing i with
89   | zero => simp [pathProbability]
90   | succ n ih =>
91     rw [pathProbability,ih,Fin.prod_univ_succ]
92     simp [Fin.castSucc_succ,Fin.cons_self_tail,Fin.tail]
93 
94 omit [Fintype I] [DecidableEq I] in
95 theorem path_potential_sum (V : I → ℝ) (n : ℕ) (i : I) (x : Fin n → I) :
96     pathPotential V n i x = ∑ r : Fin n, V ((Fin.cons i x : Fin (n+1) → I) r.castSucc) := by
97   induction n generalizing i with
98   | zero => simp [pathPotential]
99   | succ n ih =>
100     rw [pathPotential,ih,Fin.sum_univ_succ]
101     simp [Fin.castSucc_succ,Fin.cons_self_tail]
102 
103 omit [Fintype I] [DecidableEq I] in
104 theorem terminal_last (n : ℕ) (i : I) (x : Fin n → I) :
105     terminal n i x = (Fin.cons i x : Fin (n+1) → I) (Fin.last n) := by
106   induction n generalizing i with
107   | zero => simp [terminal]
108   | succ n ih =>
109     rw [terminal,ih,← Fin.succ_last]
110     simp
111 
112 end KomorebiPaperVI.FeynmanKac

Back to source controls