Survival.lean

1 import KomorebiPaperVI.MarkovSemigroup
2 import KomorebiPaperVI.Semigroups
3 import Mathlib.Analysis.SpecialFunctions.Log.Deriv
4 import Mathlib.MeasureTheory.Integral.IntegralEqImproper
5 import Mathlib.Topology.Order.MonotoneConvergence
6 
7 /-! Author: Komorebi P. Literal finite subgenerator survival, including defective exit mass. -/
8 namespace KomorebiPaperVI.Survival
9 open scoped BigOperators Matrix.Norms.Operator Topology
10 open Set Filter MeasureTheory
11 set_option backward.isDefEq.respectTransparency false
12 variable {I : Type*} [Fintype I] [DecidableEq I]
13 
14 noncomputable def state (A : Matrix I I ℝ) (p : I → ℝ) (t : ℝ) : I → ℝ :=
15   (NormedSpace.exp (t • A)).mulVec p
16 noncomputable def survival (A : Matrix I I ℝ) (p : I → ℝ) (t : ℝ) : ℝ := ∑ i, state A p t i
17 noncomputable def exitRate (A : Matrix I I ℝ) (j : I) : ℝ := -∑ i, A i j
18 noncomputable def density (A : Matrix I I ℝ) (p : I → ℝ) (t : ℝ) : ℝ :=
19   ∑ j, exitRate A j*state A p t j
20 noncomputable def hazard (A : Matrix I I ℝ) (p : I → ℝ) (t : ℝ) : ℝ :=
21   density A p t/survival A p t
22 
23 theorem survival_zero (A : Matrix I I ℝ) (p : I → ℝ) : survival A p 0=∑ i,p i := by
24   simp [survival,state]
25 
26 theorem state_nonnegative (A : Matrix I I ℝ) (hA : ∀ i j, i≠j → 0 ≤ A i j)
27     (p : I → ℝ) (hp : ∀ i,0 ≤ p i) (t : ℝ) (ht : 0 ≤ t) (i : I) : 0 ≤ state A p t i :=
28   Finset.sum_nonneg (fun j _ => mul_nonneg (MarkovSemigroup.markov_nonnegative A hA t ht i j) (hp j))
29 
30 theorem survival_positive (A : Matrix I I ℝ) (hA : ∀ i j, i≠j → 0 ≤ A i j)
31     (p : I → ℝ) (hp : ∀ i,0 ≤ p i) (hs : ∑ i,p i=1) (t : ℝ) (ht : 0 ≤ t) :
32     0 < survival A p t := by
33   have hn := state_nonnegative A hA p hp t ht
34   have hnon : 0 ≤ survival A p t := Finset.sum_nonneg (fun i _ => hn i)
35   apply lt_of_le_of_ne hnon
36   intro he
37   have hz : state A p t=0 := by
38     funext i
39     have hle := Finset.single_le_sum (fun j _ => hn j) (Finset.mem_univ i)
40     change state A p t i=0
41     change state A p t i ≤ survival A p t at hle
42     linarith [hn i]
43   have hpz : p=0 := (Matrix.mulVec_injective_of_isUnit (Matrix.isUnit_exp (t • A)))
44     (by simpa [state] using hz)
45   rw [hpz] at hs
46   simp at hs
47 
48 theorem density_nonnegative (A : Matrix I I ℝ) (hA : ∀ i j, i≠j → 0 ≤ A i j)
49     (hc : ∀ j,∑ i,A i j ≤ 0) (p : I → ℝ) (hp : ∀ i,0 ≤ p i)
50     (t : ℝ) (ht : 0 ≤ t) : 0 ≤ density A p t :=
51   Finset.sum_nonneg (fun j _ => mul_nonneg (neg_nonneg.mpr (hc j))
52     (state_nonnegative A hA p hp t ht j))
53 
54 theorem survival_derivative (A : Matrix I I ℝ) (p : I → ℝ) (t : ℝ) :
55     HasDerivAt (survival A p) (-density A p t) t := by
56   have he := Semigroups.transfer_derivative_left A t
57   have hij (i j : I) : HasDerivAt (fun u => NormedSpace.exp (u • A) i j)
58       ((A*NormedSpace.exp (t • A)) i j) t := by
59     exact hasDerivAt_pi.mp (hasDerivAt_pi.mp he i) j
60   have h := HasDerivAt.fun_sum (fun i (_ : i∈Finset.univ) =>
61     HasDerivAt.fun_sum (fun j (_ : j∈Finset.univ) => (hij i j).mul_const (p j)))
62   change HasDerivAt (survival A p) (∑ i,(A*NormedSpace.exp (t • A)).mulVec p i) t at h
63   rw [← Matrix.mulVec_mulVec] at h
64   have hd : (∑ i,A.mulVec (state A p t) i)=-density A p t := by
65     simp [density,exitRate,Matrix.mulVec,dotProduct,Finset.sum_comm,← Finset.sum_mul]
66   change HasDerivAt (survival A p) (∑ i,A.mulVec (state A p t) i) t at h
67   rwa [hd] at h
68 
69 theorem survival_antitone (A : Matrix I I ℝ) (hA : ∀ i j, i≠j → 0 ≤ A i j)
70     (hc : ∀ j,∑ i,A i j ≤ 0) (p : I → ℝ) (hp : ∀ i,0 ≤ p i) :
71     AntitoneOn (survival A p) (Ici 0) := by
72   have hd : Differentiable ℝ (survival A p) := fun t => (survival_derivative A p t).differentiableAt
73   apply antitoneOn_of_deriv_nonpos (convex_Ici 0) hd.continuous.continuousOn hd.differentiableOn
74   intro t ht
75   rw [(survival_derivative A p t).deriv]
76   exact neg_nonpos.mpr (density_nonnegative A hA hc p hp t (interior_subset ht))
77 
78 theorem density_continuous (A : Matrix I I ℝ) (p : I → ℝ) : Continuous (density A p) := by
79   unfold density state
80   fun_prop
81 
82 theorem survival_hazard (A : Matrix I I ℝ) (hA : ∀ i j, i≠j → 0 ≤ A i j)
83     (p : I → ℝ) (hp : ∀ i,0 ≤ p i) (hs : ∑ i,p i=1) (t : ℝ) (ht : 0 ≤ t) :
84     survival A p t=Real.exp (-∫ r in 0..t,hazard A p r) := by
85   have hd : ∀ r∈Icc 0 t, HasDerivAt (fun u => Real.log (survival A p u)) (-hazard A p r) r := by
86     intro r hr
87     simpa [hazard,neg_div] using (survival_derivative A p r).log
88       (survival_positive A hA p hp hs r hr.1).ne'
89   have hscont : Continuous (survival A p) :=
90     (show Differentiable ℝ (survival A p) from fun r => (survival_derivative A p r).differentiableAt).continuous
91   have hhcont : ContinuousOn (hazard A p) (Icc 0 t) :=
92     (density_continuous A p).continuousOn.div hscont.continuousOn
93       (fun r hr => (survival_positive A hA p hp hs r hr.1).ne')
94   have hi := intervalIntegral.integral_eq_sub_of_hasDerivAt
95     (by simpa [uIcc_of_le ht] using hd)
96     (hhcont.neg.intervalIntegrable_of_Icc ht)
97   simp only [Pi.neg_apply,intervalIntegral.integral_neg,survival_zero,hs,Real.log_one,sub_zero] at hi
98   rw [hi,Real.exp_log (survival_positive A hA p hp hs t ht)]
99 
100 theorem survival_has_limit (A : Matrix I I ℝ) (hA : ∀ i j, i≠j → 0 ≤ A i j)
101     (hc : ∀ j,∑ i,A i j ≤ 0) (p : I → ℝ) (hp : ∀ i,0 ≤ p i) :
102     ∃ l,0 ≤ l ∧ Tendsto (survival A p) atTop (𝓝 l) := by
103   let f : ℝ → ℝ := fun t => survival A p (max t 0)
104   have hn (t : ℝ) : 0 ≤ f t := Finset.sum_nonneg
105     (fun i _ => state_nonnegative A hA p hp _ (le_max_right _ _) i)
106   have ha : Antitone f := fun s t hst => survival_antitone A hA hc p hp
107     (show max s 0∈Ici (0:ℝ) from le_max_right s 0)
108     (show max t 0∈Ici (0:ℝ) from le_max_right t 0) (max_le_max_right 0 hst)
109   have hb : BddBelow (range f) := ⟨0,by rintro _ ⟨t,rfl⟩; exact hn t⟩
110   refine ⟨⨅ t,f t,le_ciInf hn,?_⟩
111   apply (tendsto_atTop_ciInf ha hb).congr'
112   filter_upwards [eventually_ge_atTop (0:ℝ)] with t ht
113   simp [f,max_eq_left ht]
114 
115 theorem defective_density_mass (A : Matrix I I ℝ) (hA : ∀ i j, i≠j → 0 ≤ A i j)
116     (hc : ∀ j,∑ i,A i j ≤ 0) (p : I → ℝ) (hp : ∀ i,0 ≤ p i) (hs : ∑ i,p i=1) :
117     ∃ l,0 ≤ l ∧ Tendsto (survival A p) atTop (𝓝 l) ∧
118       IntegrableOn (density A p) (Ioi 0) ∧ (∫ t in Ioi 0,density A p t)=1-l := by
119   obtain ⟨l,hl,ht⟩ := survival_has_limit A hA hc p hp
120   have hd := fun t (_ : t∈Ici (0:ℝ)) => survival_derivative A p t
121   have hn := fun t (ht : t∈Ioi (0:ℝ)) =>
122     neg_nonpos.mpr (density_nonnegative A hA hc p hp t ht.le)
123   have hi := integrableOn_Ioi_deriv_of_nonpos' hd hn ht
124   have he := integral_Ioi_of_hasDerivAt_of_nonpos' hd hn ht
125   refine ⟨l,hl,ht,integrable_neg_iff.mp hi,?_⟩
126   simp only [integral_neg,survival_zero,hs] at he
127   linarith
128 
129 theorem eventual_absorption_density (A : Matrix I I ℝ) (hA : ∀ i j, i≠j → 0 ≤ A i j)
130     (hc : ∀ j,∑ i,A i j ≤ 0) (p : I → ℝ) (hp : ∀ i,0 ≤ p i) (hs : ∑ i,p i=1)
131     (habs : Tendsto (survival A p) atTop (𝓝 0)) :
132     IntegrableOn (density A p) (Ioi 0) ∧ (∫ t in Ioi 0,density A p t)=1 := by
133   obtain ⟨l,_,hl,hi,hm⟩ := defective_density_mass A hA hc p hp hs
134   have he : l=0 := tendsto_nhds_unique hl habs
135   exact ⟨hi,by simpa [he] using hm⟩
136 
137 end KomorebiPaperVI.Survival

Back to source controls