Stat.Recurrent­Event

theorem Model.death_primitive_weighted (M : Model A X) (a : A) : Measure.map (fun ω : Outcome A X => ω.2.2.1) (M.primitiveLaw.restrict {ω | ω.1 = a ∧ ω.2.2.1 ≤ ω.2.2.2 ∧ ω.2.2.1 < M.horizon}) = (M.deathLaw.restrict (Ico 0 M.horizon)).withDensity (fun t => M.armLaw {a} * M.censorLaw (Ici t)) := by letI := M.armProb letI := M.pointProb letI := M.deathProb letI := M.censorProb have hzero : M.deathLaw (Ici (0 : ℝ)) = 1 := by simpa [hazardSurvival] using (M.death_survival 0 ⟨le_rfl, M.horizon_nonneg⟩) have hnonneg : ∀ᵐ t ∂M.deathLaw, 0 ≤ t := by rw [ae_iff] have hc : M.deathLaw (Ici (0 : ℝ))ᶜ = 0 := by rw [measure_compl measurableSet_Ici (by simp), hzero] simp have hset : {t : ℝ | ¬ 0 ≤ t} = (Ici (0 : ℝ))ᶜ := by ext t simp simpa only [hset] using hc apply Measure.ext intro s hs let E : Set (ℝ × ℝ) := {p | p.1 ∈ s ∧ p.1 ≤ p.2 ∧ p.1 < M.horizon} have hE : MeasurableSet E := by dsimp [E] measurability have htime : Measurable (fun ω : Outcome A X => ω.2.2.1) := by fun_prop have hset : {ω : Outcome A X | (ω.1 = a ∧ ω.2.2.1 ≤ ω.2.2.2 ∧ ω.2.2.1 < M.horizon) ∧ ω.2.2.1 ∈ s} = ({a} : Set A) ×ˢ (univ ×ˢ E) := by ext ω simp [E, and_comm, and_assoc] have hleft : (Measure.map (fun ω : Outcome A X => ω.2.2.1) (M.primitiveLaw.restrict {ω | ω.1 = a ∧ ω.2.2.1 ≤ ω.2.2.2 ∧ ω.2.2.1 < M.horizon})) s = M.armLaw {a} * (M.deathLaw.prod M.censorLaw) E := by rw [Measure.map_apply htime hs, Measure.restrict_apply (hs.preimage htime)] rw [Set.inter_comm] change M.primitiveLaw {ω : Outcome A X | (ω.1 = a ∧ ω.2.2.1 ≤ ω.2.2.2 ∧ ω.2.2.1 < M.horizon) ∧ ω.2.2.1 ∈ s} = _ rw [hset] unfold Model.primitiveLaw rw [Measure.prod_prod, Measure.prod_prod] simp rw [hleft] have hsection (t : ℝ) : M.censorLaw (Prod.mk t ⁻¹' E) = (s ∩ Iio M.horizon).indicator (fun u => M.censorLaw (Ici u)) t := by by_cases ht : t ∈ s ∩ Iio M.horizon · have heq : Prod.mk t ⁻¹' E = Ici t := by ext c have hlt : t < M.horizon := ht.2 simp [E, ht.1, hlt] simp [heq, ht] · have heq : Prod.mk t ⁻¹' E = ∅ := by ext c have hfail : t ∉ s ∨ ¬ t < M.horizon := by simpa [Set.mem_inter_iff] using (not_and_or.mp ht) rcases hfail with hns | hge · simp [E, hns] · simp [E, hge] simp [heq, ht] have hprod : (M.deathLaw.prod M.censorLaw) E = ∫⁻ t in s ∩ Iio M.horizon, M.censorLaw (Ici t) ∂M.deathLaw := by rw [Measure.prod_apply hE] simp_rw [hsection] exact lintegral_indicator (hs.inter measurableSet_Iio) _ have hsupport : M.deathLaw.restrict (s ∩ Iio M.horizon) = M.deathLaw.restrict (s ∩ Ico 0 M.horizon) := by apply Measure.restrict_congr_set filter_upwards [hnonneg] with t ht change (t ∈ s ∧ t < M.horizon) = (t ∈ s ∧ 0 ≤ t ∧ t < M.horizon) apply propext tauto have htail : Measurable (fun t : ℝ => M.censorLaw (Ici t)) := by let F : Set (ℝ × ℝ) := {p | p.1 ≤ p.2} have hF : MeasurableSet F := by dsimp [F] measurability have hf := measurable_measure_prodMk_left (ν := M.censorLaw) hF convert hf using 1 funext t congr 1 rw [hprod, withDensity_apply _ hs] rw [lintegral_const_mul (M.armLaw {a}) htail] rw [Measure.restrict_restrict hs] rw [hsupport]

theorem Model.recurrence_primitive_strict_tail (M : Model A X) (a : A) (s : Set ℝ) (hs : MeasurableSet s) : (∫⁻ ω, M.primitiveRecurrenceCountSet a s ω ∂M.primitiveLaw) = ∫⁻ t in s ∩ Ico (0 : ℝ) M.horizon, M.armLaw {a} * M.deathLaw (Ioi t) * M.censorLaw (Ioi t) * (M.intensity t : ℝ≥0∞) ∂volume := by classical letI := M.pointProb letI := M.armProb letI := M.deathProb letI := M.censorProb let μ := Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.finitePoissonSampleLaw M.pointLaw M.poissonRate let F : FiniteSample X × (ℝ × ℝ) → ℝ≥0∞ := fun z => ∑ i : Fin z.1.1, if M.time (z.1.2 i) ∈ s ∧ M.time (z.1.2 i) < z.2.1 ∧ M.time (z.1.2 i) < z.2.2 ∧ M.time (z.1.2 i) < M.horizon then 1 else 0 have hF : Measurable F := by have he (n : ℕ) : MeasurableEmbedding (fixedSizeEmbed (X := X) n) := by refine ⟨?_, ?_, ?_⟩ · intro x y h exact eq_of_heq (Sigma.mk.inj_iff.mp h).2 · exact measurable_fixedSizeEmbed n · intro u hu change @MeasurableSet _ (⨅ m, (inferInstance : MeasurableSpace (Fin m → X)).map (Sigma.mk m)) (fixedSizeEmbed n '' u) rw [MeasurableSpace.measurableSet_iInf] intro m change MeasurableSet ((fixedSizeEmbed (X := X) m) ⁻¹' ((fixedSizeEmbed (X := X) n) '' u)) by_cases h : m = n · subst m rw [Set.preimage_image_eq u (fun x y h => eq_of_heq (Sigma.mk.inj_iff.mp h).2)] exact hu · convert MeasurableSet.empty using 1 ext x simp only [Set.mem_preimage, Set.mem_image, Set.mem_empty_iff_false, iff_false] rintro ⟨y, _, heq⟩ exact h (congrArg fst heq).symm intro u hu have hset : F ⁻¹' u = ⋃ n : ℕ, (map (fixedSizeEmbed (X := X) n) id) '' {z : (Fin n → X) × (ℝ × ℝ) | F (⟨n, z.1⟩, z.2) ∈ u} := by ext ⟨⟨n, x⟩, dc⟩ constructor · intro ht refine Set.mem_iUnion.mpr ⟨n, ?_⟩ exact ⟨(x, dc), ht, rfl⟩ · intro ht obtain ⟨m, ⟨y, e⟩, hy, hz⟩ := Set.mem_iUnion.mp ht cases hz exact hy rw [hset] apply MeasurableSet.iUnion intro n apply ((he n).prodMap MeasurableEmbedding.id).measurableSet_image.mpr have hn : Measurable (fun z : (Fin n → X) × (ℝ × ℝ) => F (⟨n, z.1⟩, z.2)) := by change Measurable (fun z : (Fin n → X) × (ℝ × ℝ) => ∑ i : Fin n, if M.time (z.1 i) ∈ s ∧ M.time (z.1 i) < z.2.1 ∧ M.time (z.1 i) < z.2.2 ∧ M.time (z.1 i) < M.horizon then (1 : ℝ≥0∞) else 0) apply Finset.measurable_sum intro i hi have ht : Measurable (fun z : (Fin n → X) × (ℝ × ℝ) => M.time (z.1 i)) := M.measurable_time.comp ((measurable_pi_apply i).comp measurable_fst) apply Measurable.ite · convert ((hs.preimage ht).inter (measurableSet_lt ht (measurable_fst.comp measurable_snd))).inter ((measurableSet_lt ht (measurable_snd.comp measurable_snd)).inter (measurableSet_lt ht (measurable_const : Measurable (fun _ => M.horizon)))) using 1 <;> ext z <;> simp only [Set.mem_inter_iff, Set.mem_ofPred_eq, Set.mem_preimage, Function.comp_apply] <;> tauto · exact measurable_const · exact measurable_const exact hn hu let G : A × (FiniteSample X × (ℝ × ℝ)) → ℝ≥0∞ := fun z => if z.1 = a then F z.2 else 0 have hG : Measurable G := Measurable.ite ((measurableSet_singleton a).preimage measurable_fst) (hF.comp measurable_snd) measurable_const have hcount (z : Outcome A X) : M.primitiveRecurrenceCountSet a s z = G z := by unfold Model.primitiveRecurrenceCountSet G F Model.stopTime by_cases ha : z.1 = a · simp only [ha, if_true] apply Finset.sum_congr rfl intro i hi simp only [true_and, lt_min_iff] congr 1 apply propext tauto · simp [ha] have hprimitive : (∫⁻ z, M.primitiveRecurrenceCountSet a s z ∂M.primitiveLaw) = M.armLaw {a} * (∫⁻ z, F z ∂μ.prod (M.deathLaw.prod M.censorLaw)) := by change (∫⁻ z, M.primitiveRecurrenceCountSet a s z ∂M.armLaw.prod (μ.prod (M.deathLaw.prod M.censorLaw))) = _ simp_rw [hcount] rw [lintegral_prod_symm' G hG] have hinner (z : _) : (∫⁻ b, G (b, z) ∂M.armLaw) = M.armLaw {a} * F z := by change (∫⁻ b, ({a} : Set A).indicator (fun _ => F z) b ∂M.armLaw) = _ rw [lintegral_indicator_const (measurableSet_singleton a)] exact mul_comm _ _ simp_rw [hinner] rw [lintegral_const_mul (M.armLaw {a}) hF] rw [hprimitive] have hpoisson (dc : ℝ × ℝ) : (∫⁻ sample, F (sample, dc) ∂μ) = ∫⁻ t in Ico (0 : ℝ) M.horizon, (if t ∈ s ∧ t < dc.1 ∧ t < dc.2 then (M.intensity t : ℝ≥0∞) else 0) ∂volume := by let f : ℝ → ℝ≥0∞ := fun t => if t ∈ s ∧ t < dc.1 ∧ t < dc.2 ∧ t < M.horizon then 1 else 0 have hf : Measurable f := by apply Measurable.ite · convert ((hs.inter (measurableSet_Iio : MeasurableSet (Iio dc.1))).inter (measurableSet_Iio : MeasurableSet (Iio dc.2))).inter (measurableSet_Iio : MeasurableSet (Iio M.horizon)) using 1 <;> ext t <;> simp only [Set.mem_inter_iff, Set.mem_ofPred_eq, Set.mem_Iio] <;> tauto · exact measurable_const · exact measurable_const calc (∫⁻ sample, F (sample, dc) ∂μ) = ∫⁻ t in Ico (0 : ℝ) M.horizon, f t * (M.intensity t : ℝ≥0∞) ∂volume := by exact M.poisson_time_lintegral f hf _ = _ := by apply setLIntegral_congr_fun measurableSet_Ico intro t ht simp only [f] have hth : t < M.horizon := ht.2 by_cases h : t ∈ s ∧ t < dc.1 ∧ t < dc.2 <;> simp [h, hth] have hswap : (∫⁻ z, F z ∂μ.prod (M.deathLaw.prod M.censorLaw)) = ∫⁻ t in Ico (0 : ℝ) M.horizon, ∫⁻ dc : ℝ × ℝ, if t ∈ s ∧ t < dc.1 ∧ t < dc.2 then (M.intensity t : ℝ≥0∞) else 0 ∂(M.deathLaw.prod M.censorLaw) ∂volume := by rw [lintegral_prod_symm' F hF] simp_rw [hpoisson] have hH : Measurable (fun z : (ℝ × ℝ) × ℝ => if z.2 ∈ s ∧ z.2 < z.1.1 ∧ z.2 < z.1.2 then (M.intensity z.2 : ℝ≥0∞) else 0) := by have ht : Measurable (fun z : (ℝ × ℝ) × ℝ => z.2) := measurable_snd exact Measurable.ite ((hs.preimage ht).inter ((measurableSet_lt ht (measurable_fst.comp measurable_fst)).inter (measurableSet_lt ht (measurable_snd.comp measurable_fst)))) (M.measurable_intensity.coe_nnreal_ennreal.comp ht) measurable_const exact lintegral_lintegral_swap hH.aemeasurable rw [hswap] have htail (t : ℝ) : (∫⁻ dc : ℝ × ℝ, if t ∈ s ∧ t < dc.1 ∧ t < dc.2 then (M.intensity t : ℝ≥0∞) else 0 ∂(M.deathLaw.prod M.censorLaw)) = if t ∈ s then M.deathLaw (Ioi t) * M.censorLaw (Ioi t) * (M.intensity t : ℝ≥0∞) else 0 := by by_cases ht : t ∈ s · simp only [ht, true_and, if_true] have hfun : (fun dc : ℝ × ℝ => if t < dc.1 ∧ t < dc.2 then (M.intensity t : ℝ≥0∞) else 0) = (Ioi t ×ˢ Ioi t).indicator (fun _ => (M.intensity t : ℝ≥0∞)) := by funext dc simp [indicator, Set.mem_prod] rw [hfun] rw [lintegral_indicator_const (measurableSet_Ioi.prod measurableSet_Ioi)] rw [Measure.prod_prod] exact mul_comm _ _ · simp [ht] simp_rw [htail] have htailMeas (ν : Measure ℝ) [SFinite ν] : Measurable (fun t : ℝ => ν (Ioi t)) := by let E : Set (ℝ × ℝ) := {p | p.1 < p.2} have hE : MeasurableSet E := by dsimp [E] exact measurableSet_lt measurable_fst measurable_snd have h := measurable_measure_prodMk_left (ν := ν) hE convert h using 1 funext t congr 1 have hscore : Measurable (fun t : ℝ => if t ∈ s then M.deathLaw (Ioi t) * M.censorLaw (Ioi t) * (M.intensity t : ℝ≥0∞) else 0) := by exact Measurable.ite hs (((htailMeas M.deathLaw).mul (htailMeas M.censorLaw)).mul M.measurable_intensity.coe_nnreal_ennreal) measurable_const rw [← lintegral_const_mul (M.armLaw {a}) hscore] calc (∫⁻ t in Ico (0 : ℝ) M.horizon, M.armLaw {a} * if t ∈ s then M.deathLaw (Ioi t) * M.censorLaw (Ioi t) * (M.intensity t : ℝ≥0∞) else 0 ∂volume) = ∫⁻ t in Ico (0 : ℝ) M.horizon, s.indicator (fun t => M.armLaw {a} * M.deathLaw (Ioi t) * M.censorLaw (Ioi t) * (M.intensity t : ℝ≥0∞)) t ∂volume := by congr 1 funext t by_cases ht : t ∈ s <;> simp [indicator, ht, mul_assoc] _ = _ := by rw [lintegral_indicator hs, Measure.restrict_restrict hs]

theorem Model.risk_factorization (M : Model A X) (a : A) (t : ℝ) (ht : t ∈ Icc (0 : ℝ) M.horizon) : M.riskProbability a t = M.armLaw {a} * M.deathLaw (Ici t) * M.censorLaw (Ici t) := by letI := M.armProb letI := M.pointProb letI := M.deathProb letI := M.censorProb have hs : MeasurableSet {y : A × (ℝ × (Bool × (ℕ → ℝ))) | y.1 = a ∧ t ≤ y.2.1} := by measurability have hpre : M.observe ⁻¹' {y : A × (ℝ × (Bool × (ℕ → ℝ))) | y.1 = a ∧ t ≤ y.2.1} = ({a} : Set A) ×ˢ (univ ×ˢ ((Ici t) ×ˢ (Ici t))) := by ext ω simp [Model.observe, Model.stopTime, ht.2, and_assoc, Prod.le_def] unfold Model.riskProbability Model.observedLaw rw [Measure.map_apply M.measurable_observe hs, hpre] unfold Model.primitiveLaw rw [Measure.prod_prod, Measure.prod_prod, Measure.prod_prod] simp only [measure_univ, one_mul, mul_assoc]

theorem Model.death_stopped_poisson_mean (M : Model A X) : M.deathStoppedCountMean = ∫⁻ t in Ico (0 : ℝ) M.horizon, M.deathLaw (Ici t) * (M.intensity t : ℝ≥0∞) ∂volume := by letI := M.pointProb letI := M.deathProb let μ := Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.finitePoissonSampleLaw M.pointLaw M.poissonRate let F : FiniteSample X × ℝ → ℝ≥0∞ := fun z => ∑ i : Fin z.1.1, if M.time (z.1.2 i) < z.2 ∧ M.time (z.1.2 i) < M.horizon then 1 else 0 have hF : Measurable F := by have he (n : ℕ) : MeasurableEmbedding (fixedSizeEmbed (X := X) n) := by refine ⟨?_, ?_, ?_⟩ · intro x y h exact eq_of_heq (Sigma.mk.inj_iff.mp h).2 · exact measurable_fixedSizeEmbed n · intro s hs change @MeasurableSet _ (⨅ m, (inferInstance : MeasurableSpace (Fin m → X)).map (Sigma.mk m)) (fixedSizeEmbed n '' s) rw [MeasurableSpace.measurableSet_iInf] intro m change MeasurableSet ((fixedSizeEmbed (X := X) m) ⁻¹' ((fixedSizeEmbed (X := X) n) '' s)) by_cases h : m = n · subst m rw [Set.preimage_image_eq s (fun x y h => eq_of_heq (Sigma.mk.inj_iff.mp h).2)] exact hs · convert MeasurableSet.empty using 1 ext x simp only [Set.mem_preimage, Set.mem_image, Set.mem_empty_iff_false, iff_false] rintro ⟨y, _, heq⟩ exact h (congrArg fst heq).symm intro t ht have hset : F ⁻¹' t = ⋃ n : ℕ, (map (fixedSizeEmbed (X := X) n) id) '' {z : (Fin n → X) × ℝ | F (⟨n, z.1⟩, z.2) ∈ t} := by ext ⟨⟨n, x⟩, d⟩ constructor · intro ht refine Set.mem_iUnion.mpr ⟨n, ?_⟩ exact ⟨(x, d), ht, rfl⟩ · intro ht obtain ⟨m, ⟨y, e⟩, hy, hz⟩ := Set.mem_iUnion.mp ht cases hz exact hy rw [hset] apply MeasurableSet.iUnion intro n apply ((he n).prodMap MeasurableEmbedding.id).measurableSet_image.mpr have hn : Measurable (fun z : (Fin n → X) × ℝ => F (⟨n, z.1⟩, z.2)) := by change Measurable (fun z : (Fin n → X) × ℝ => ∑ i : Fin n, if M.time (z.1 i) < z.2 ∧ M.time (z.1 i) < M.horizon then (1 : ℝ≥0∞) else 0) apply Finset.measurable_sum intro i hi apply Measurable.ite · exact (measurableSet_lt (M.measurable_time.comp ((measurable_pi_apply i).comp measurable_fst)) measurable_snd).inter (measurableSet_lt (M.measurable_time.comp ((measurable_pi_apply i).comp measurable_fst)) measurable_const) · exact measurable_const · exact measurable_const exact hn ht change (∫⁻ z, F z ∂μ.prod M.deathLaw) = _ rw [lintegral_prod_symm' F hF] calc (∫⁻ d, ∫⁻ s, F (s, d) ∂μ ∂M.deathLaw) = ∫⁻ d, ∫⁻ t in Ico (0 : ℝ) M.horizon, if t < d then (M.intensity t : ℝ≥0∞) else 0 ∂volume ∂M.deathLaw := by apply lintegral_congr intro d exact M.poisson_count_before_death d _ = ∫⁻ t in Ico (0 : ℝ) M.horizon, ∫⁻ d, if t < d then (M.intensity t : ℝ≥0∞) else 0 ∂M.deathLaw ∂volume := by have hG : Measurable (fun z : ℝ × ℝ => if z.2 < z.1 then (M.intensity z.2 : ℝ≥0∞) else 0) := by exact Measurable.ite (measurableSet_lt measurable_snd measurable_fst) (M.measurable_intensity.coe_nnreal_ennreal.comp measurable_snd) measurable_const exact lintegral_lintegral_swap hG.aemeasurable _ = ∫⁻ t in Ico (0 : ℝ) M.horizon, M.deathLaw (Ioi t) * (M.intensity t : ℝ≥0∞) ∂volume := by apply setLIntegral_congr_fun measurableSet_Ico intro t ht change (∫⁻ d, (Ioi t).indicator (fun _ => (M.intensity t : ℝ≥0∞)) d ∂M.deathLaw) = _ rw [lintegral_indicator_const measurableSet_Ioi] exact mul_comm _ _ _ = ∫⁻ t in Ico (0 : ℝ) M.horizon, M.deathLaw (Ici t) * (M.intensity t : ℝ≥0∞) ∂volume := by apply lintegral_congr_ae filter_upwards [ae_restrict_of_ae (ae_measure_Ioi_eq_Ici M.deathLaw)] with t ht rw [ht]

theorem Model.death_event_density (M : Model A X) (a : A) : M.deathEventMeasure a = (M.riskSetMeasure a).withDensity (fun t => (M.hazard t : ℝ≥0∞)) := by let μ : Measure ℝ := volume.restrict (Ico 0 M.horizon) let w : ℝ → ℝ≥0∞ := fun t => M.armLaw {a} * M.censorLaw (Ici t) let s : ℝ → ℝ≥0∞ := fun t => ofReal (hazardSurvival M.hazard t) let h : ℝ → ℝ≥0∞ := fun t => (M.hazard t : ℝ≥0∞) have hcensor : Measurable (fun t : ℝ => M.censorLaw (Ici t)) := Antitone.measurable (fun _ _ hxy => measure_mono (Ici_subset_Ici.mpr hxy)) have hw : Measurable w := measurable_const.mul hcensor have hh : Measurable h := M.measurable_hazard.coe_nnreal_ennreal have hs : AEMeasurable s μ := by apply aemeasurable_restrict_of_antitoneOn measurableSet_Ico intro x hx y hy hxy change ofReal (hazardSurvival M.hazard y) ≤ ofReal (hazardSurvival M.hazard x) rw [← M.death_survival x ⟨hx.1, hx.2.le⟩, ← M.death_survival y ⟨hy.1, hy.2.le⟩] exact measure_mono (Ici_subset_Ici.mpr hxy) have hf : AEMeasurable (s * h) μ := hs.mul hh.aemeasurable calc M.deathEventMeasure a = (M.deathLaw.restrict (Ico 0 M.horizon)).withDensity w := by rw [M.death_event_measure_primitive, M.death_primitive_weighted] _ = (μ.withDensity (s * h)).withDensity w := by rw [M.death_law_restrict_eq_withDensity] rfl _ = μ.withDensity ((s * h) * w) := (withDensity_mul₀ hf hw.aemeasurable).symm _ = μ.withDensity ((w * s) * h) := by congr 1 funext t simp only [Pi.mul_apply] ac_rfl _ = (μ.withDensity (w * s)).withDensity h := withDensity_mul₀ (hw.aemeasurable.mul hs) hh.aemeasurable _ = (M.riskSetMeasure a).withDensity h := by congr 1 unfold Model.riskSetMeasure μ w s apply withDensity_congr_ae filter_upwards [ae_restrict_mem measurableSet_Ico] with t ht simp only [Pi.mul_apply] rw [M.death_survival t ⟨ht.1, ht.2.le⟩] ac_rfl

theorem Model.death_law_restrict_eq_withDensity (M : Model A X) : M.deathLaw.restrict (Ico 0 M.horizon) = (volume.restrict (Ico 0 M.horizon)).withDensity (fun t => ofReal (hazardSurvival M.hazard t) * (M.hazard t : ℝ≥0∞)) := by letI := M.deathProb let f : ℝ → ℝ≥0∞ := fun t => ofReal (hazardSurvival M.hazard t) * (M.hazard t : ℝ≥0∞) let ν : Measure ℝ := (volume.restrict (Ico 0 M.horizon)).withDensity f have hν : ν = (volume.withDensity f).restrict (Ico 0 M.horizon) := (restrict_withDensity measurableSet_Ico f).symm change M.deathLaw.restrict (Ico 0 M.horizon) = ν apply Measure.ext_of_Ico' · intro a b hab exact measure_ne_top _ _ · intro a b hab let c := max a 0 let d := min b M.horizon have hset : Ico a b ∩ Ico 0 M.horizon = Ico c d := Set.Ico_inter_Ico have hsub : Ico c d ⊆ Ico 0 M.horizon := by intro t ht exact ⟨le_trans (le_max_right _ _) ht.1, lt_of_lt_of_le ht.2 (min_le_right _ _)⟩ have hleft : (M.deathLaw.restrict (Ico 0 M.horizon)) (Ico a b) = M.deathLaw (Ico c d) := by rw [Measure.restrict_apply measurableSet_Ico, hset] have hright : ν (Ico a b) = ν (Ico c d) := by calc ν (Ico a b) = (volume.withDensity f) (Ico c d) := by rw [hν, Measure.restrict_apply measurableSet_Ico, hset] _ = ν (Ico c d) := by rw [hν, Measure.restrict_apply measurableSet_Ico, Set.inter_eq_self_of_subset_left hsub] rw [hleft, hright] by_cases hcd : c ≤ d · have hc : 0 ≤ c := le_max_right _ _ have hd : d ≤ M.horizon := min_le_right _ _ change M.deathLaw (Ico c d) = ((volume.restrict (Ico 0 M.horizon)).withDensity f) (Ico c d) rw [M.death_law_Ico_eq_survival_sub c d hc hcd hd, M.survival_hazard_density_Ico c d hc hcd hd] · have hempty : Ico c d = ∅ := Set.Ico_eq_empty_of_le (le_of_not_ge hcd) simp [hempty]

theorem Model.identify_densities (M : Model A X) (N : Model A Y) (a : A) (T : ℝ) (hTM : T < M.horizon) (hTN : T < N.horizon) (hobs : M.observedLaw = N.observedLaw) (haM : 0 < M.armLaw {a}) (hcM : ∀ t ∈ Icc (0 : ℝ) T, 0 < M.censorLaw (Ici t)) : ∀ᵐ t ∂(volume.restrict (Icc (0 : ℝ) T)), M.hazard t = N.hazard t ∧ M.intensity t = N.intensity t := by let s : Set ℝ := Icc 0 T let wM : ℝ → ℝ≥0∞ := fun t => M.armLaw {a} * M.deathLaw (Ici t) * M.censorLaw (Ici t) let wN : ℝ → ℝ≥0∞ := fun t => N.armLaw {a} * N.deathLaw (Ici t) * N.censorLaw (Ici t) have hsM : s ⊆ Ico 0 M.horizon := by intro t ht exact ⟨ht.1, lt_of_le_of_lt ht.2 hTM⟩ have hsN : s ⊆ Ico 0 N.horizon := by intro t ht exact ⟨ht.1, lt_of_le_of_lt ht.2 hTN⟩ have hw : ∀ t ∈ s, wM t = wN t := by intro t ht calc wM t = M.riskProbability a t := (M.risk_factorization a t ⟨ht.1, le_trans ht.2 hTM.le⟩).symm _ = N.riskProbability a t := by simp [Model.riskProbability, hobs] _ = wN t := N.risk_factorization a t ⟨ht.1, le_trans ht.2 hTN.le⟩ have hrisk : (M.riskSetMeasure a).restrict s = (N.riskSetMeasure a).restrict s := by change ((volume.restrict (Ico 0 M.horizon)).withDensity wM).restrict s = ((volume.restrict (Ico 0 N.horizon)).withDensity wN).restrict s rw [restrict_withDensity measurableSet_Icc, restrict_withDensity measurableSet_Icc, Measure.restrict_restrict_of_subset hsM, Measure.restrict_restrict_of_subset hsN] exact withDensity_congr_ae ((ae_restrict_mem measurableSet_Icc).mono fun t ht => hw t ht) have hdeath : M.deathEventMeasure a = N.deathEventMeasure a := by simp only [Model.deathEventMeasure, hobs] have hrec : M.recurrenceEventMeasure a = N.recurrenceEventMeasure a := by simp only [Model.recurrenceEventMeasure, hobs] have htail (ν : Measure ℝ) : Measurable (fun t : ℝ => ν (Ici t)) := Antitone.measurable (fun x y hxy => measure_mono (Ici_subset_Ici.mpr hxy)) have hmeas : Measurable wM := by dsimp [wM] exact (measurable_const.mul (htail M.deathLaw)).mul (htail M.censorLaw) letI := M.armProb letI := M.deathProb letI := M.censorProb have hfinite : ∀ t, wM t ≠ ⊤ := by intro t dsimp [wM] exact ENNReal.mul_ne_top (ENNReal.mul_ne_top (measure_ne_top M.armLaw {a}) (measure_ne_top M.deathLaw (Ici t))) (measure_ne_top M.censorLaw (Ici t)) haveI : SigmaFinite ((M.riskSetMeasure a).restrict s) := by have heq : (M.riskSetMeasure a).restrict s = (volume.restrict s).withDensity wM := by change ((volume.restrict (Ico 0 M.horizon)).withDensity wM).restrict s = _ rw [restrict_withDensity measurableSet_Icc, Measure.restrict_restrict_of_subset hsM] rw [heq] exact SigmaFinite.withDensity_of_ne_top (Filter.Eventually.of_forall hfinite) have hmh : (fun t => (M.hazard t : ℝ≥0∞)) =ᵐ[(M.riskSetMeasure a).restrict s] (fun t => (N.hazard t : ℝ≥0∞)) := by apply (withDensity_eq_iff_of_sigmaFinite M.measurable_hazard.coe_nnreal_ennreal.aemeasurable N.measurable_hazard.coe_nnreal_ennreal.aemeasurable).mp calc _ = (M.deathEventMeasure a).restrict s := by rw [← restrict_withDensity measurableSet_Icc, ← M.death_event_density] _ = (N.deathEventMeasure a).restrict s := by rw [hdeath] _ = _ := by rw [N.death_event_density, restrict_withDensity measurableSet_Icc, ← hrisk] have hmi : (fun t => (M.intensity t : ℝ≥0∞)) =ᵐ[(M.riskSetMeasure a).restrict s] (fun t => (N.intensity t : ℝ≥0∞)) := by apply (withDensity_eq_iff_of_sigmaFinite M.measurable_intensity.coe_nnreal_ennreal.aemeasurable N.measurable_intensity.coe_nnreal_ennreal.aemeasurable).mp calc _ = (M.recurrenceEventMeasure a).restrict s := by rw [← restrict_withDensity measurableSet_Icc, ← M.recurrence_event_density] _ = (N.recurrenceEventMeasure a).restrict s := by rw [hrec] _ = _ := by rw [N.recurrence_event_density, restrict_withDensity measurableSet_Icc, ← hrisk] have hpos : ∀ t ∈ s, wM t ≠ 0 := by intro t ht have hd : 0 < M.deathLaw (Ici t) := by rw [M.death_survival t ⟨ht.1, le_trans ht.2 hTM.le⟩] exact ENNReal.ofReal_pos.mpr (Real.exp_pos _) exact (ENNReal.mul_pos (ne_of_gt (ENNReal.mul_pos (ne_of_gt haM) (ne_of_gt hd))) (ne_of_gt (hcM t ht))).ne' have heq : (M.riskSetMeasure a).restrict s = (volume.restrict s).withDensity wM := by change ((volume.restrict (Ico 0 M.horizon)).withDensity wM).restrict s = _ rw [restrict_withDensity measurableSet_Icc, Measure.restrict_restrict_of_subset hsM] have hmh' := (ae_withDensity_iff hmeas).mp (heq ▸ hmh) have hmi' := (ae_withDensity_iff hmeas).mp (heq ▸ hmi) filter_upwards [hmh', hmi', ae_restrict_mem measurableSet_Icc] with t hh hi ht exact ⟨by exact_mod_cast (hh (hpos t ht)), by exact_mod_cast (hi (hpos t ht))⟩

theorem Model.measurable_observe (M : Model A X) : Measurable M.observe := by have hstop : Measurable M.stopTime := by unfold Model.stopTime fun_prop have hdeath : Measurable (fun ω : Outcome A X => decide (ω.2.2.1 ≤ ω.2.2.2 ∧ ω.2.2.1 < M.horizon)) := by change Measurable (fun ω : Outcome A X => if ω.2.2.1 ≤ ω.2.2.2 ∧ ω.2.2.1 < M.horizon then true else false) apply Measurable.ite ((measurableSet_le (show Measurable (fun ω : Outcome A X => ω.2.2.1) by fun_prop) (show Measurable (fun ω : Outcome A X => ω.2.2.2) by fun_prop)).inter (measurableSet_lt (show Measurable (fun ω : Outcome A X => ω.2.2.1) by fun_prop) measurable_const)) all_goals exact measurable_const have hsample (n : ℕ) : Measurable (fun s : FiniteSample X => if h : n < s.1 then M.time (s.2 ⟨n, h⟩) else M.horizon + 1) := by intro t ht rw [MeasurableSpace.measurableSet_iInf] intro m change MeasurableSet ((fun x : Fin m → X => if h : n < m then M.time (x ⟨n, h⟩) else M.horizon + 1) ⁻¹' t) by_cases h : n < m · simp only [dif_pos h] exact ht.preimage (M.measurable_time.comp (measurable_pi_apply (⟨n, h⟩ : Fin m))) · simp only [dif_neg h] exact measurable_const ht have hcoord (n : ℕ) : Measurable (fun ω : Outcome A X => if h : n < ω.2.1.1 then if M.time (ω.2.1.2 ⟨n, h⟩) < M.stopTime ω then M.time (ω.2.1.2 ⟨n, h⟩) else M.horizon + 1 else M.horizon + 1) := by let f : Outcome A X → ℝ := fun ω => if h : n < ω.2.1.1 then M.time (ω.2.1.2 ⟨n, h⟩) else M.horizon + 1 have hf : Measurable f := (hsample n).comp (measurable_fst.comp measurable_snd) have hc : Measurable (fun ω : Outcome A X => ω.2.1.1) := Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.measurable_finiteSample_count.comp (measurable_fst.comp measurable_snd) have heq : (fun ω : Outcome A X => if h : n < ω.2.1.1 then if M.time (ω.2.1.2 ⟨n, h⟩) < M.stopTime ω then M.time (ω.2.1.2 ⟨n, h⟩) else M.horizon + 1 else M.horizon + 1) = (fun ω => if n < ω.2.1.1 ∧ f ω < M.stopTime ω then f ω else M.horizon + 1) := by funext ω by_cases h : n < ω.2.1.1 <;> simp [f, h] rw [heq] exact Measurable.ite ((measurableSet_lt measurable_const hc).inter (measurableSet_lt hf hstop)) hf measurable_const unfold Model.observe exact measurable_fst.prodMk (hstop.prodMk (hdeath.prodMk (measurable_pi_lambda _ hcoord)))

theorem finitePoissonSample_lintegral_sum (P : Measure X) [IsProbabilityMeasure P] (rate : ℝ≥0) (f : X → ℝ≥0∞) (hf : Measurable f) : (∫⁻ s, ∑ i : Fin s.1, f (s.2 i) ∂Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.finitePoissonSampleLaw P rate) = ∫⁻ x, f x ∂((rate : ℝ≥0∞) • P) := by /- Partition by the Poisson count using the finite-sample count-fibre theorem; exchange the finite point sum with the iid product integral; finish with the first moment of the scalar Poisson count. -/ classical let μ := Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.finitePoissonSampleLaw P rate let g : FiniteSample X → ℝ≥0∞ := fun s => ∑ i : Fin s.1, f (s.2 i) have hg : Measurable g := by intro t ht change @MeasurableSet _ (⨅ n, (inferInstance : MeasurableSpace (Fin n → X)).map (Sigma.mk n)) (g ⁻¹' t) rw [MeasurableSpace.measurableSet_iInf] intro n change MeasurableSet ((fun x : Fin n → X => ∑ i, f (x i)) ⁻¹' t) exact (Finset.measurable_sum _ (fun i _ => hf.comp (measurable_pi_apply i))) ht have hcount (n : ℕ) : (∫⁻ s, g s ∂μ.restrict (count ⁻¹' ({n} : Set ℕ))) = (poissonMeasure rate) {n} * (n : ℝ≥0∞) * (∫⁻ x, f x ∂P) := by rw [finitePoissonSampleLaw_restrict_count_eq] rw [lintegral_smul_measure, lintegral_map hg (measurable_fixedSizeEmbed n)] change (poissonMeasure rate) {n} * (∫⁻ x : Fin n → X, ∑ i : Fin n, f (x i) ∂Measure.pi (fun _ => P)) = _ rw [lintegral_finsetSum] swap · intro i _ exact hf.comp (measurable_pi_apply i) have hi (i : Fin n) : (∫⁻ x : Fin n → X, f (x i) ∂Measure.pi (fun _ => P)) = ∫⁻ x, f x ∂P := by exact (measurePreserving_eval (μ := fun _ : Fin n => P) i).lintegral_comp hf simp only [hi, Finset.sum_const, Finset.card_fin, nsmul_eq_mul] simp [mul_assoc] have hpart : (∫⁻ s, g s ∂μ) = ∑' n : ℕ, ∫⁻ s, g s ∂μ.restrict (count ⁻¹' ({n} : Set ℕ)) := by let S : ℕ → Set (FiniteSample X) := fun n => count ⁻¹' ({n} : Set ℕ) have hU : (⋃ n, S n) = univ := by ext s simp [S] rw [← lintegral_iUnion (μ := μ) (s := S)] · simp [hU, S] · intro n exact measurable_finiteSample_count (X := X) (MeasurableSet.singleton n) · intro i j hij exact Set.disjoint_left.mpr (by intro s hi hj exact hij (by simpa [S] using hi.symm.trans hj)) rw [hpart] simp_rw [hcount] rw [ENNReal.tsum_mul_right] have hm : (∫⁻ n : ℕ, (n : ℝ≥0∞) ∂poissonMeasure rate) = (rate : ℝ≥0∞) := by have h := poisson_natCast_first_moment rate have hi := (poisson_natCast_memLp_two rate).integrable (by norm_num) have hr := ofReal_integral_eq_lintegral_ofReal hi (Filter.Eventually.of_forall (fun n : ℕ => Nat.cast_nonneg n)) rw [h] at hr simpa [ENNReal.ofReal_natCast, ENNReal.ofReal_coe_nnreal] using hr.symm have hsum : (∑' n : ℕ, (poissonMeasure rate) {n} * (n : ℝ≥0∞)) = (rate : ℝ≥0∞) := by rw [lintegral_countable'] at hm simpa only [mul_comm] using hm rw [hsum, lintegral_smul_measure, smul_eq_mul]

theorem Model.recurrence_event_density (M : Model A X) (a : A) : M.recurrenceEventMeasure a = (M.riskSetMeasure a).withDensity (fun t => (M.intensity t : ℝ≥0∞)) := by letI := M.deathProb letI := M.censorProb let μ : Measure ℝ := volume.restrict (Ico 0 M.horizon) let w : ℝ → ℝ≥0∞ := fun t => M.armLaw {a} * M.deathLaw (Ici t) * M.censorLaw (Ici t) let h : ℝ → ℝ≥0∞ := fun t => (M.intensity t : ℝ≥0∞) have hdeath : Measurable (fun t : ℝ => M.deathLaw (Ici t)) := Antitone.measurable (fun _ _ hxy => measure_mono (Ici_subset_Ici.mpr hxy)) have hcensor : Measurable (fun t : ℝ => M.censorLaw (Ici t)) := Antitone.measurable (fun _ _ hxy => measure_mono (Ici_subset_Ici.mpr hxy)) have hw : Measurable w := (measurable_const.mul hdeath).mul hcensor have hh : Measurable h := M.measurable_intensity.coe_nnreal_ennreal apply Measure.ext intro s hs calc M.recurrenceEventMeasure a s = ∫⁻ t in s ∩ Ico (0 : ℝ) M.horizon, M.armLaw {a} * M.deathLaw (Ioi t) * M.censorLaw (Ioi t) * h t ∂volume := by rw [M.recurrence_event_measure_primitive a s hs, M.recurrence_primitive_strict_tail a s hs] _ = ∫⁻ t in s ∩ Ico (0 : ℝ) M.horizon, w t * h t ∂volume := by apply lintegral_congr_ae filter_upwards [ae_restrict_of_ae (ae_measure_Ioi_eq_Ici M.deathLaw), ae_restrict_of_ae (ae_measure_Ioi_eq_Ici M.censorLaw)] with t hd hc simp only [w, hd, hc] _ = (μ.withDensity (w * h)) s := by rw [withDensity_apply _ hs] simp only [μ] rw [Measure.restrict_restrict hs] congr 1 _ = ((μ.withDensity w).withDensity h) s := by rw [withDensity_mul₀ hw.aemeasurable hh.aemeasurable] _ = ((M.riskSetMeasure a).withDensity h) s := by rfl

theorem ae_measure_Ioi_eq_Ici (ν : Measure ℝ) [IsFiniteMeasure ν] : ∀ᵐ t ∂(volume : Measure ℝ), ν (Ioi t) = ν (Ici t) := by have hcount : {t : ℝ | 0 < ν {t}}.Countable := by simpa only [id_eq, ofPred_eq_eq_singleton] using (Measure.countable_meas_level_set_pos (μ := ν) (g := id) measurable_id) filter_upwards [hcount.ae_notMem (volume : Measure ℝ)] with t ht have hz : ν {t} = 0 := nonpos_iff_eq_zero.mp (not_lt.mp ht) have hdecomp : Ici t = {t} ∪ Ioi t := by simpa only [Icc_self] using (Icc_union_Ioi_eq_Ici (a := t) (b := t) le_rfl).symm have hdisj : Disjoint ({t} : Set ℝ) (Ioi t) := by simp calc ν (Ioi t) = ν {t} + ν (Ioi t) := by simp [hz] _ = ν ({t} ∪ Ioi t) := (measure_union hdisj measurableSet_Ioi).symm _ = ν (Ici t) := by rw [← hdecomp]