BayesianFlow.lean

1 import KomorebiPaperVI.FiniteBayes
2 import Mathlib.Analysis.Calculus.Deriv.Inv
3 
4 /-! Author: Komorebi P. The normalized exponential flow and its actual derivative. -/
5 namespace KomorebiPaperVI.BayesianFlow
6 open KomorebiPaperVI.FiniteBayes
7 open scoped BigOperators
8 variable {I : Type*} [Fintype I]
9 
10 noncomputable def likelihood (g : I → ℝ) (t : ℝ) (i : I) : ℝ := Real.exp (t*g i)
11 noncomputable def flow (p g : I → ℝ) (t : ℝ) : I → ℝ := update p (likelihood g t)
12 
13 theorem positive_evidence (p g : I → ℝ) (hp : IsProbability p) (t : ℝ) :
14     0 < evidence p (likelihood g t) := by
15   have hex : ∃ i, 0 < p i := by
16     by_contra h
17     push Not at h
18     have he : mass p=0 := Finset.sum_eq_zero (fun i _ => le_antisymm (h i) (hp.1 i))
19     linarith [hp.2]
20   obtain ⟨i, hi⟩ := hex
21   apply Finset.sum_pos'
22   · intro j _; exact mul_nonneg (Real.exp_pos _).le (hp.1 j)
23   · exact ⟨i, Finset.mem_univ i, mul_pos (Real.exp_pos _) hi⟩
24 
25 theorem flow_probability (p g : I → ℝ) (hp : IsProbability p) (t : ℝ) :
26     IsProbability (flow p g t) :=
27   posterior_probability p _ hp (fun _ => (Real.exp_pos _).le) (positive_evidence p g hp t)
28 
29 omit [Fintype I] in
30 theorem likelihood_add (g : I → ℝ) (s t : ℝ) :
31     likelihood g (s+t) = fun i => likelihood g t i*likelihood g s i := by
32   funext i
33   dsimp [likelihood]
34   rw [add_mul, Real.exp_add, mul_comm]
35 
36 theorem flow_add (p g : I → ℝ) (hp : IsProbability p) (s t : ℝ) :
37     flow p g (s+t) = flow (flow p g t) g s := by
38   have hz := (positive_evidence p g hp (s+t)).ne'
39   rw [likelihood_add] at hz
40   dsimp only [flow]
41   rw [likelihood_add]
42   exact (posterior_composition p (likelihood g t) (likelihood g s)
43     (positive_evidence p g hp t).ne' hz).symm
44 
45 theorem flow_zero (p g : I → ℝ) (hp : IsProbability p) : flow p g 0=p := by
46   funext i
47   simp only [flow, update, likelihood, zero_mul, Real.exp_zero, one_mul, evidence]
48   change p i/mass p=p i
49   rw [hp.2, div_one]
50 
51 omit [Fintype I] in
52 theorem likelihood_derivative (g : I → ℝ) (t : ℝ) (i : I) :
53     HasDerivAt (fun u => likelihood g u i) (g i*likelihood g t i) t := by
54   simpa [likelihood, mul_comm] using ((hasDerivAt_id t).mul_const (g i)).exp
55 
56 theorem evidence_derivative (p g : I → ℝ) (t : ℝ) :
57     HasDerivAt (fun u => evidence p (likelihood g u))
58       (∑ i, g i*likelihood g t i*p i) t := by
59   convert! HasDerivAt.sum (u := Finset.univ)
60     (fun i _ => (likelihood_derivative g t i).mul_const (p i)) using 1
61   ext u
62   simp [evidence]
63 
64 theorem flow_derivative (p g : I → ℝ) (hp : IsProbability p) (t : ℝ) (i : I) :
65     HasDerivAt (fun u => flow p g u i)
66       ((g i-(∑ j, g j*flow p g t j))*flow p g t i) t := by
67   have hz := (positive_evidence p g hp t).ne'
68   have hd := ((likelihood_derivative g t i).mul_const (p i)).div
69     (evidence_derivative p g t) hz
70   convert! hd using 1
71   simp only [flow, update]
72   simp only [← mul_div_assoc, ← Finset.sum_div]
73   field_simp
74 
75 end KomorebiPaperVI.BayesianFlow

Back to source controls