Stat.Recurrent­Event.Counting­Process

theorem subject_event_square_expectation {n : ℕ} (failureLaw censorLaw : Measure ℝ) (hazard : ℝ → ℝ) (hFailure : NonnegativeTimeLaw failureLaw) (hHazard : HasCensorHazard censorLaw hazard) (H : ℝ → Sample n → ℝ) (hPredictable : LeftPredictable H) (hMeasurable : Measurable (fun p : ℝ × Sample n => H p.1 p.2)) (i : Fin n) (u : ℝ) (hQuadratic : QuadraticEnergyFinite failureLaw censorLaw hazard H u) : (∫ x : Sample n, (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then H (x i).2 x else 0) ^ 2 ∂sampleLaw n failureLaw censorLaw) = ∫ x : Sample n, (∫ s in Icc 0 u, (H s x) ^ 2 * hazard s * riskIndicator i s x ∂volume) ∂sampleLaw n failureLaw censorLaw := by classical let μ := sampleLaw n failureLaw censorLaw let Q : ℝ → Sample n → ℝ := fun s x => (H s x) ^ 2 have hQpred : LeftPredictable Q := by intro s x y hxy simpa [Q] using congrArg (fun z : ℝ => z ^ 2) (hPredictable s x y hxy) have hQmeas : Measurable (fun p : ℝ × Sample n => Q p.1 p.2) := by exact hMeasurable.pow_const 2 have hQnonneg : ∀ s x, 0 ≤ Q s x := fun s x => sq_nonneg _ have hlin := predictable_censor_compensator_lintegral failureLaw censorLaw hazard hFailure hHazard Q hQpred hQmeas hQnonneg i u have hfinite : (∫⁻ x : Sample n, ∫⁻ s in Icc 0 u, ofReal (Q s x * hazard s * riskIndicator i s x) ∂volume ∂μ) ≠ ⊤ := by have hle : (∫⁻ x : Sample n, ∫⁻ s in Icc 0 u, ofReal (Q s x * hazard s * riskIndicator i s x) ∂volume ∂μ) ≤ ∫⁻ x : Sample n, ∫⁻ s in Icc 0 u, ofReal ((H s x) ^ 2 * hazard s * (∑ j : Fin n, riskIndicator j s x)) ∂volume ∂μ := by apply lintegral_mono intro x apply lintegral_mono intro s apply ENNReal.ofReal_le_ofReal dsimp [Q] apply mul_le_mul_of_nonneg_left · exact Finset.single_le_sum (f := fun j : Fin n => riskIndicator j s x) (fun j hj => by unfold riskIndicator split_ifs <;> norm_num) (Finset.mem_univ i) · exact mul_nonneg (sq_nonneg _) (hHazard.2.2.1 s) exact ne_top_of_le_ne_top hQuadratic hle have hEventInt : Integrable (fun x : Sample n => if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then Q (x i).2 x else 0) μ := by have hm : Measurable (fun x : Sample n => if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then Q (x i).2 x else 0) := by have hc : Measurable (fun x : Sample n => (x i).2) := by fun_prop have hf : Measurable (fun x : Sample n => (x i).1) := by fun_prop exact (hQmeas.comp (hc.prodMk measurable_id)).ite ((measurableSet_le hc measurable_const).inter (measurableSet_lt hc hf)) measurable_const apply (lintegral_ofReal_ne_top_iff_integrable hm.aestronglyMeasurable (by filter_upwards [] with x split_ifs <;> positivity)).1 rw [hlin] exact hfinite have hcomp := predictable_censor_compensator_nonnegative failureLaw censorLaw hazard hFailure hHazard Q hQpred hQmeas hQnonneg i u hEventInt convert hcomp using 1 <;> simp only [Q, ite_pow, zero_pow (by decide : (2 : ℕ) ≠ 0)]

theorem subjectIntegralBefore_leftPredictable {n : ℕ} (hazard : ℝ → ℝ) (H : ℝ → Sample n → ℝ) (hPredictable : LeftPredictable H) (i : Fin n) : LeftPredictable (subjectIntegralBefore hazard H i) := by have hRisk (t : ℝ) (z : Sample n) (hf : t ≠ (z i).1) (hc : t ≠ (z i).2) : riskIndicator i t z = if 0 ≤ t ∧ censorCount i t z = 0 ∧ failureCount i t z = 0 then 1 else 0 := by by_cases h0 : 0 ≤ t · rcases lt_or_gt_of_ne hf with htf | htf · rcases lt_or_gt_of_ne hc with htc | htc · simp [riskIndicator, censorCount, failureCount, h0, htf, htc, le_of_lt] · have hcf : (z i).2 < (z i).1 := lt_trans htc htf simp [riskIndicator, censorCount, failureCount, h0, htf, htc, hcf, le_of_lt] · rcases lt_or_gt_of_ne hc with htc | htc · have hfc : (z i).1 < (z i).2 := lt_trans htf htc simp [riskIndicator, censorCount, failureCount, h0, htf, htc, hfc, le_of_lt] · by_cases hfc : (z i).1 ≤ (z i).2 · simp [riskIndicator, censorCount, failureCount, h0, htf, htc, hfc, le_of_lt] · have hcf : (z i).2 < (z i).1 := lt_of_not_ge hfc simp [riskIndicator, censorCount, failureCount, h0, htf, htc, hcf, le_of_lt] · simp [riskIndicator, censorCount, failureCount, h0] have hNe (a : ℝ) : ∀ᵐ t ∂(volume : Measure ℝ), t ≠ a := by rw [ae_iff] simpa only [not_ne_iff, Set.ofPred_eq_eq_singleton] using (measure_singleton a : (volume : Measure ℝ) {a} = 0) intro s x y hHist have hInt : (∫ t in Icc 0 s, H t x * hazard t * riskIndicator i t x ∂volume) = ∫ t in Icc 0 s, H t y * hazard t * riskIndicator i t y ∂volume := by rw [integral_Icc_eq_integral_Ico, integral_Icc_eq_integral_Ico] apply integral_congr_ae have hxF := ae_restrict_of_ae (s := Ico 0 s) (hNe (x i).1) have hxC := ae_restrict_of_ae (s := Ico 0 s) (hNe (x i).2) have hyF := ae_restrict_of_ae (s := Ico 0 s) (hNe (y i).1) have hyC := ae_restrict_of_ae (s := Ico 0 s) (hNe (y i).2) have htMem : ∀ᵐ t ∂(volume : Measure ℝ).restrict (Ico 0 s), t ∈ Ico 0 s := ae_restrict_mem measurableSet_Ico filter_upwards [hxF, hxC, hyF, hyC, htMem] with t hxF hxC hyF hyC ht have hHistory := hHist i t ht.2 have hHt : H t x = H t y := hPredictable t x y (fun j u hu => hHist j u (lt_trans hu ht.2)) rw [hHt, hRisk t x hxF hxC, hRisk t y hyF hyC, hHistory.1, hHistory.2] have hEvent : (if (x i).2 < s ∧ (x i).2 < (x i).1 then H (x i).2 x else 0) = (if (y i).2 < s ∧ (y i).2 < (y i).1 then H (y i).2 y else 0) := by by_cases hx : (x i).2 < s ∧ (x i).2 < (x i).1 · have hxc : censorCount i (x i).2 x = 1 := by simp [censorCount, hx.2] have hyc : censorCount i (x i).2 y = 1 := by rw [← (hHist i (x i).2 hx.1).1, hxc] have hyEvent : (y i).2 ≤ (x i).2 ∧ (y i).2 < (y i).1 := by by_contra hn simp [censorCount, hn] at hyc have hy : (y i).2 < s ∧ (y i).2 < (y i).1 := ⟨lt_of_le_of_lt hyEvent.1 hx.1, hyEvent.2⟩ have hyc' : censorCount i (y i).2 y = 1 := by simp [censorCount, hy.2] have hxc' : censorCount i (y i).2 x = 1 := by rw [(hHist i (y i).2 hy.1).1, hyc'] have hxy : (x i).2 ≤ (y i).2 := by by_contra hn have hn' : ¬ ((x i).2 ≤ (y i).2 ∧ (x i).2 < (x i).1) := by simp [hn] simp [censorCount, hn'] at hxc' have heq : (x i).2 = (y i).2 := le_antisymm hxy hyEvent.1 have hH : H (x i).2 x = H (y i).2 y := by rw [← heq] exact hPredictable (x i).2 x y (fun j u hu => hHist j u (lt_trans hu hx.1)) simp [hx, hy, hH] · have hyFalse : ¬ ((y i).2 < s ∧ (y i).2 < (y i).1) := by intro hy have hyc : censorCount i (y i).2 y = 1 := by simp [censorCount, hy.2] have hxc : censorCount i (y i).2 x = 1 := by rw [(hHist i (y i).2 hy.1).1, hyc] have hxEvent : (x i).2 ≤ (y i).2 ∧ (x i).2 < (x i).1 := by by_contra hn simp [censorCount, hn] at hxc exact hx ⟨lt_of_le_of_lt hxEvent.1 hy.1, hxEvent.2⟩ simp [hx, hyFalse] simp only [subjectIntegralBefore, hEvent, hInt]

theorem distinct_subject_integral_product_pathwise {n : ℕ} (hazard : ℝ → ℝ) (H : ℝ → Sample n → ℝ) (i j : Fin n) (u : ℝ) (hu : 0 ≤ u) (x : Sample n) (hci0 : 0 ≤ (x i).2) (hcj0 : 0 ≤ (x j).2) (hCensorDistinct : (x i).2 ≠ (x j).2) (hPathi : Integrable (fun s => H s x * hazard s * riskIndicator i s x) (volume.restrict (Icc 0 u))) (hPathj : Integrable (fun s => H s x * hazard s * riskIndicator j s x) (volume.restrict (Icc 0 u))) : subjectIntegral hazard H i u x * subjectIntegral hazard H j u x = (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then H (x i).2 x * subjectIntegralBefore hazard H j (x i).2 x else 0) + (if (x j).2 ≤ u ∧ (x j).2 < (x j).1 then H (x j).2 x * subjectIntegralBefore hazard H i (x j).2 x else 0) - (∫ s in Icc 0 u, subjectIntegralBefore hazard H j s x * H s x * hazard s * riskIndicator i s x ∂volume) - (∫ s in Icc 0 u, subjectIntegralBefore hazard H i s x * H s x * hazard s * riskIndicator j s x ∂volume) := by let ci := (x i).2 let cj := (x j).2 let di := (x i).1 let dj := (x j).1 let fi : ℝ → ℝ := fun s => H s x * hazard s * riskIndicator i s x let fj : ℝ → ℝ := fun s => H s x * hazard s * riskIndicator j s x let Ai := H ci x let Aj := H cj x let Ii := ∫ s in Icc 0 u, fi s ∂volume let Ij := ∫ s in Icc 0 u, fj s ∂volume let Pi := fun s => ∫ t in Icc 0 s, fi t ∂volume let Pj := fun s => ∫ t in Icc 0 s, fj t ∂volume have hbilin := integral_prefix_mul_bilinear fi fj u hu hPathi hPathj have hcrossj := integral_before_cross fi fj Aj cj dj u hcj0 hu hPathi hPathj have hcrossi := integral_before_cross fj fi Ai ci di u hci0 hu hPathj hPathi have hR : (if ci ≤ u ∧ ci < di then Ai else 0) * (if cj ≤ u ∧ cj < dj then Aj else 0) = (if ci ≤ u ∧ ci < di then Ai else 0) * (if cj < ci ∧ cj < dj then Aj else 0) + (if cj ≤ u ∧ cj < dj then Aj else 0) * (if ci < cj ∧ ci < di then Ai else 0) := by change ci ≠ cj at hCensorDistinct by_cases hci : ci ≤ u ∧ ci < di · by_cases hcj : cj ≤ u ∧ cj < dj · rcases lt_or_gt_of_ne hCensorDistinct with hlt | hlt · have hnot : ¬ cj < ci := not_lt_of_ge (le_of_lt hlt) simp [hci, hcj, hlt, hnot, mul_comm] · have hnot : ¬ ci < cj := not_lt_of_ge (le_of_lt hlt) simp [hci, hcj, hlt, hnot] · have hnot : ¬ (cj < ci ∧ cj < dj) := by intro h exact hcj ⟨le_trans (le_of_lt h.1) hci.1, h.2⟩ simp [hci, hcj, hnot] · by_cases hcj : cj ≤ u ∧ cj < dj · have hnot : ¬ (ci < cj ∧ ci < di) := by intro h exact hci ⟨le_trans (le_of_lt h.1) hcj.1, h.2⟩ simp [hci, hcj, hnot] · simp [hci, hcj] have hmain : ((if ci ≤ u ∧ ci < di then Ai else 0) - Ii) * ((if cj ≤ u ∧ cj < dj then Aj else 0) - Ij) = (if ci ≤ u ∧ ci < di then Ai * ((if cj < ci ∧ cj < dj then Aj else 0) - Pj ci) else 0) + (if cj ≤ u ∧ cj < dj then Aj * ((if ci < cj ∧ ci < di then Ai else 0) - Pi cj) else 0) - (∫ s in Icc 0 u, ((if cj < s ∧ cj < dj then Aj else 0) - Pj s) * fi s ∂volume) - (∫ s in Icc 0 u, ((if ci < s ∧ ci < di then Ai else 0) - Pi s) * fj s ∂volume) := by rw [hcrossj, hcrossi] unfold Ii Ij Pi Pj at * by_cases hi : ci ≤ u ∧ ci < di · by_cases hj : cj ≤ u ∧ cj < dj · simp only [if_pos hi, if_pos hj] at hR ⊢ nlinarith [hR, hbilin] · simp only [if_pos hi, if_neg hj] at hR ⊢ nlinarith [hR, hbilin] · by_cases hj : cj ≤ u ∧ cj < dj · simp only [if_neg hi, if_pos hj] at hR ⊢ nlinarith [hR, hbilin] · simp only [if_neg hi, if_neg hj] at hR ⊢ nlinarith [hR, hbilin] simpa only [subjectIntegral, subjectIntegralBefore, ci, cj, di, dj, fi, fj, Ai, Aj, Ii, Ij, Pi, Pj, mul_assoc] using hmain

theorem predictable_censor_compensator {n : ℕ} (failureLaw censorLaw : Measure ℝ) (hazard : ℝ → ℝ) (hFailure : NonnegativeTimeLaw failureLaw) (hHazard : HasCensorHazard censorLaw hazard) (H : ℝ → Sample n → ℝ) (hPredictable : LeftPredictable H) (hMeasurable : Measurable (fun p : ℝ × Sample n => H p.1 p.2)) (i : Fin n) (u : ℝ) (hEvent : Integrable (fun x : Sample n => if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then H (x i).2 x else 0) (sampleLaw n failureLaw censorLaw)) : (∫ x : Sample n, (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then H (x i).2 x else 0) ∂sampleLaw n failureLaw censorLaw) = ∫ x : Sample n, (∫ s in Icc 0 u, H s x * hazard s * riskIndicator i s x ∂volume) ∂sampleLaw n failureLaw censorLaw := by /- Apply the nonnegative identity to the positive and negative parts. Its extended-integral proof also supplies integrability of their compensators and the almost-everywhere inner-integrability needed to subtract the time integrals. -/ classical let μ := sampleLaw n failureLaw censorLaw let Hpos : ℝ → Sample n → ℝ := fun s x => max (H s x) 0 let Hneg : ℝ → Sample n → ℝ := fun s x => max (-H s x) 0 have hp_pred : LeftPredictable Hpos := by intro s x y hxy simp only [Hpos, hPredictable s x y hxy] have hn_pred : LeftPredictable Hneg := by intro s x y hxy simp only [Hneg, hPredictable s x y hxy] have hp_meas : Measurable (fun p : ℝ × Sample n => Hpos p.1 p.2) := hMeasurable.max measurable_const have hn_meas : Measurable (fun p : ℝ × Sample n => Hneg p.1 p.2) := hMeasurable.neg.max measurable_const have hp_nonneg : ∀ s x, 0 ≤ Hpos s x := fun s x => le_max_right _ _ have hn_nonneg : ∀ s x, 0 ≤ Hneg s x := fun s x => le_max_right _ _ have hp_event : Integrable (fun x : Sample n => if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then Hpos (x i).2 x else 0) μ := by convert hEvent.sup (integrable_zero (Sample n) ℝ μ) using 1 funext x by_cases hx : (x i).2 ≤ u ∧ (x i).2 < (x i).1 <;> simp [Hpos, hx] have hn_event : Integrable (fun x : Sample n => if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then Hneg (x i).2 x else 0) μ := by convert hEvent.neg.sup (integrable_zero (Sample n) ℝ μ) using 1 funext x by_cases hx : (x i).2 ≤ u ∧ (x i).2 < (x i).1 <;> simp [Hneg, hx] have hp_comp := nonnegative_compensator_integrable failureLaw censorLaw hazard hFailure hHazard Hpos hp_pred hp_meas hp_nonneg i u hp_event have hn_comp := nonnegative_compensator_integrable failureLaw censorLaw hazard hFailure hHazard Hneg hn_pred hn_meas hn_nonneg i u hn_event have hp_eq := predictable_censor_compensator_nonnegative failureLaw censorLaw hazard hFailure hHazard Hpos hp_pred hp_meas hp_nonneg i u hp_event have hn_eq := predictable_censor_compensator_nonnegative failureLaw censorLaw hazard hFailure hHazard Hneg hn_pred hn_meas hn_nonneg i u hn_event have hevent_sub : (fun x : Sample n => (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then Hpos (x i).2 x else 0) - (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then Hneg (x i).2 x else 0)) = (fun x => if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then H (x i).2 x else 0) := by funext x by_cases hx : (x i).2 ≤ u ∧ (x i).2 < (x i).1 · simp [hx, Hpos, Hneg, max_zero_sub_max_neg_zero_eq_self] · simp [hx] have hcomp_sub : ∀ᵐ x ∂μ, (∫ s in Icc 0 u, Hpos s x * hazard s * riskIndicator i s x ∂volume) - (∫ s in Icc 0 u, Hneg s x * hazard s * riskIndicator i s x ∂volume) = ∫ s in Icc 0 u, H s x * hazard s * riskIndicator i s x ∂volume := by filter_upwards [hp_comp.2, hn_comp.2] with x hpi hni rw [← integral_sub hpi hni] congr 1 funext s dsimp [Hpos, Hneg] rw [← sub_mul, ← sub_mul, max_zero_sub_max_neg_zero_eq_self] calc (∫ x : Sample n, (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then H (x i).2 x else 0) ∂μ) = ∫ x : Sample n, ((if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then Hpos (x i).2 x else 0) - (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then Hneg (x i).2 x else 0)) ∂μ := by rw [hevent_sub] _ = (∫ x : Sample n, (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then Hpos (x i).2 x else 0) ∂μ) - (∫ x : Sample n, (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then Hneg (x i).2 x else 0) ∂μ) := integral_sub hp_event hn_event _ = (∫ x : Sample n, (∫ s in Icc 0 u, Hpos s x * hazard s * riskIndicator i s x ∂volume) ∂μ) - (∫ x : Sample n, (∫ s in Icc 0 u, Hneg s x * hazard s * riskIndicator i s x ∂volume) ∂μ) := by rw [hp_eq, hn_eq] _ = ∫ x : Sample n, ((∫ s in Icc 0 u, Hpos s x * hazard s * riskIndicator i s x ∂volume) - (∫ s in Icc 0 u, Hneg s x * hazard s * riskIndicator i s x ∂volume)) ∂μ := (integral_sub hp_comp.1 hn_comp.1).symm _ = ∫ x : Sample n, (∫ s in Icc 0 u, H s x * hazard s * riskIndicator i s x ∂volume) ∂μ := integral_congr_ae hcomp_sub

theorem censor_event_hazard_lintegral (censorLaw : Measure ℝ) (hazard g : ℝ → ℝ) (hHazard : HasCensorHazard censorLaw hazard) (hG : Measurable g) (f u : ℝ) : (∫⁻ c : ℝ, ofReal (if c ≤ u ∧ c < f then g c else 0) ∂censorLaw) = ∫⁻ s in Icc 0 u, ofReal (if s < f then g s * hazard s * (censorLaw (Ici s)).toReal else 0) ∂volume := by haveI : IsProbabilityMeasure censorLaw := ⟨hHazard.1.1⟩ have hsupport : Ici (0 : ℝ) ∈ ae censorLaw := (mem_ae_iff_prob_eq_one measurableSet_Ici).2 hHazard.1.2 have hsurv : Measurable (fun s : ℝ => censorLaw (Ici s)) := by apply Antitone.measurable intro a b hab exact measure_mono (Set.Ici_subset_Ici.mpr hab) have hdens : Measurable (fun s : ℝ => ofReal (hazard s * (censorLaw (Ici s)).toReal)) := (hHazard.2.1.mul hsurv.ennreal_toReal).ennreal_ofReal have hcut : Measurable (fun s : ℝ => ofReal (if s < f then g s else 0)) := by exact (Measurable.ite measurableSet_Iio hG measurable_const).ennreal_ofReal calc (∫⁻ c : ℝ, ofReal (if c ≤ u ∧ c < f then g c else 0) ∂censorLaw) = ∫⁻ c in Icc 0 u, ofReal (if c < f then g c else 0) ∂censorLaw := by rw [← lintegral_indicator measurableSet_Icc] apply lintegral_congr_ae filter_upwards [hsupport] with c hc simp only [Set.indicator_apply, Set.mem_Icc, Set.mem_Ici] at hc ⊢ by_cases hcu : c ≤ u <;> simp [hc, hcu] _ = ∫⁻ s in Icc 0 u, ofReal (hazard s * (censorLaw (Ici s)).toReal) * ofReal (if s < f then g s else 0) ∂volume := by simpa only [← hHazard.2.2.2.2, Pi.mul_apply] using (setLIntegral_withDensity_eq_lintegral_mul₀ (μ := volume) (s := Icc 0 u) hdens.aemeasurable hcut.aemeasurable measurableSet_Icc) _ = ∫⁻ s in Icc 0 u, ofReal (if s < f then g s * hazard s * (censorLaw (Ici s)).toReal else 0) ∂volume := by apply setLIntegral_congr_fun measurableSet_Icc intro s hs by_cases hsf : s < f · simp only [if_pos hsf] rw [← ENNReal.ofReal_mul (mul_nonneg (hHazard.2.2.1 s) ENNReal.toReal_nonneg)] congr 1 ring · simp [hsf]

theorem predictable_censor_compensator_lintegral {n : ℕ} (failureLaw censorLaw : Measure ℝ) (hazard : ℝ → ℝ) (hFailure : NonnegativeTimeLaw failureLaw) (hHazard : HasCensorHazard censorLaw hazard) (H : ℝ → Sample n → ℝ) (hPredictable : LeftPredictable H) (hMeasurable : Measurable (fun p : ℝ × Sample n => H p.1 p.2)) (hNonnegative : ∀ s x, 0 ≤ H s x) (i : Fin n) (u : ℝ) : (∫⁻ x : Sample n, ofReal (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then H (x i).2 x else 0) ∂sampleLaw n failureLaw censorLaw) = ∫⁻ x : Sample n, ∫⁻ s in Icc 0 u, ofReal (H s x * hazard s * riskIndicator i s x) ∂volume ∂sampleLaw n failureLaw censorLaw := by /- Disintegrate the finite product law at subject `i`. For a fixed `s`, `leftPredictable_censor_tail_invariant` identifies the value of H across all censor times at or after `s`; the two preceding lemmas identify both sides with the same resampled time integral. -/ exact (predictable_censor_event_hazard_lintegral failureLaw censorLaw hazard hFailure hHazard H hMeasurable hNonnegative i u).trans (predictable_censor_atRisk_hazard_lintegral failureLaw censorLaw hazard hFailure hHazard H hPredictable hMeasurable hNonnegative i u).symm

theorem leftPredictable_censor_tail_invariant {n : ℕ} (H : ℝ → Sample n → ℝ) (hH : LeftPredictable H) (s : ℝ) (x : Sample n) (i : Fin n) (c : ℝ) (hOld : s ≤ (x i).2) (hNew : s ≤ c) : H s x = H s (update x i ((x i).1, c)) := by /- For each t < s, neither censor time can have generated a censor event. A failure before t is observed under both censor times. Apply `hH` to the resulting equality of earlier event histories. -/ apply hH s x (update x i ((x i).1, c)) intro j t ht by_cases hji : j = i · subst j have htOld : t < (x i).2 := lt_of_lt_of_le ht hOld have htNew : t < c := lt_of_lt_of_le ht hNew have hcOld : ¬ (x i).2 ≤ t := not_le.mpr htOld have hcNew : ¬ c ≤ t := not_le.mpr htNew constructor · simp [censorCount, Function.update_self, hcOld, hcNew] · by_cases hf : (x i).1 ≤ t · have hfOld : (x i).1 ≤ (x i).2 := le_trans hf (le_of_lt htOld) have hfNew : (x i).1 ≤ c := le_trans hf (le_of_lt htNew) simp [failureCount, Function.update_self, hf, hfOld, hfNew] · simp [failureCount, Function.update_self, hf] · have hu := Function.update_of_ne hji ((x i).1, c) x simp [censorCount, failureCount, hu]

theorem integral_prefix_square (f : ℝ → ℝ) (u : ℝ) (hu : 0 ≤ u) (hf : Integrable f (volume.restrict (Icc 0 u))) : (∫ s in Icc 0 u, f s ∂volume) ^ 2 = ∫ s in Icc 0 u, 2 * (∫ t in Icc 0 s, f t ∂volume) * f s ∂volume := by let F : ℝ → ℝ := fun x => ∫ t in (0 : ℝ)..x, f t have hfi : IntervalIntegrable f volume 0 u := (intervalIntegrable_iff_integrableOn_Icc_of_le hu).2 hf have hF : AbsolutelyContinuousOnInterval F 0 u := hfi.absolutelyContinuousOnInterval_intervalIntegral (by simp) have hderiv := hfi.ae_hasDerivAt_integral have hprod := hF.integral_deriv_mul_eq_sub hF have heq : (∫ s in (0 : ℝ)..u, deriv F s * F s + F s * deriv F s) = ∫ s in (0 : ℝ)..u, 2 * (∫ t in Icc 0 s, f t ∂volume) * f s := by apply intervalIntegral.integral_congr_ae filter_upwards [hderiv] with s hs hsmem have hsIcc : s ∈ Icc (0 : ℝ) u := by simpa [Set.uIcc_of_le hu] using (Set.uIoc_subset_uIcc hsmem) have hds : deriv F s = f s := (hs (by simpa [Set.uIcc_of_le hu] using hsIcc) 0 (by simp)).deriv have hprefix : F s = ∫ t in Icc 0 s, f t ∂volume := by dsimp [F] rw [intervalIntegral.integral_of_le hsIcc.1, ← integral_Icc_eq_integral_Ioc] rw [hds, hprefix] ring rw [heq] at hprod have hzero : F 0 = 0 := by simp [F] have hfinal : F u = ∫ s in Icc 0 u, f s ∂volume := by dsimp [F] rw [intervalIntegral.integral_of_le hu, ← integral_Icc_eq_integral_Ioc] rw [hfinal, hzero] at hprod simpa [pow_two, intervalIntegral.integral_of_le hu, ← integral_Icc_eq_integral_Ioc] using hprod.symm

theorem aggregate_integral_isometry {n : ℕ} (failureLaw censorLaw : Measure ℝ) (hazard : ℝ → ℝ) (hFailure : NonnegativeTimeLaw failureLaw) (hHazard : HasCensorHazard censorLaw hazard) (H : ℝ → Sample n → ℝ) (hPredictable : LeftPredictable H) (hMeasurable : Measurable (fun p : ℝ × Sample n => H p.1 p.2)) (u : ℝ) (hu : 0 ≤ u) (hQuadratic : QuadraticEnergyFinite failureLaw censorLaw hazard H u) (hEnergy : Integrable (predictableEnergy hazard H u) (sampleLaw n failureLaw censorLaw)) : (∫ x : Sample n, (aggregateIntegral hazard H u x) ^ 2 ∂sampleLaw n failureLaw censorLaw) = ∫ x : Sample n, predictableEnergy hazard H u x ∂sampleLaw n failureLaw censorLaw := by /- For each i, derive integrability of the subject energy by domination by `predictableEnergy`. Derive subject square integrability directly from the event-payoff and hazard-payoff squares; isometry by itself is only an equality of Bochner integrals. Cauchy--Schwarz gives products. Expand `(∑ i, subjectIntegral ... i)^2` as a double sum, interchange each finite sum with the expectation, and use the subject isometry on diagonal terms and `distinct_subject_integrals_orthogonal` elsewhere. The sum of subject energies is `predictableEnergy` by linearity of the time integral (pathwise almost everywhere integrability follows from the finite quadratic-energy hypothesis). -/ classical let μ := sampleLaw n failureLaw censorLaw let J : Fin n → Sample n → ℝ := fun i x => subjectIntegral hazard H i u x let Q : Fin n → Sample n → ℝ := fun i x => ∫ s in Icc 0 u, (H s x) ^ 2 * hazard s * riskIndicator i s x ∂volume have hQ (i : Fin n) : Integrable (Q i) μ := subject_energy_integrable failureLaw censorLaw hazard hFailure hHazard H hMeasurable i u hQuadratic hEnergy have hSquare (i : Fin n) : AEStronglyMeasurable (J i) μ ∧ Integrable (fun x => (J i x) ^ 2) μ := by let E : Sample n → ℝ := fun x => if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then H (x i).2 x else 0 let A : Sample n → ℝ := fun x => ∫ s in Icc 0 u, H s x * hazard s * riskIndicator i s x ∂volume have hEmeas : Measurable E := by have hc : Measurable (fun x : Sample n => (x i).2) := by fun_prop have hf : Measurable (fun x : Sample n => (x i).1) := by fun_prop exact (hMeasurable.comp (hc.prodMk measurable_id)).ite ((measurableSet_le hc measurable_const).inter (measurableSet_lt hc hf)) measurable_const have hAmeas : Measurable A := by let F : Sample n × ℝ → ℝ := fun p => H p.2 p.1 * hazard p.2 * riskIndicator i p.2 p.1 have hrisk : Measurable (fun p : Sample n × ℝ => riskIndicator i p.2 p.1) := by unfold riskIndicator have hf : Measurable (fun p : Sample n × ℝ => (p.1 i).1) := by fun_prop have hc : Measurable (fun p : Sample n × ℝ => (p.1 i).2) := by fun_prop have hs : MeasurableSet {p : Sample n × ℝ | 0 ≤ p.2 ∧ p.2 ≤ (p.1 i).1 ∧ p.2 ≤ (p.1 i).2} := by simpa only [Set.ofPred_and, Set.inter_assoc, id_eq] using (((show MeasurableSet {p : Sample n × ℝ | (0 : ℝ) ≤ p.2} from measurableSet_le measurable_const measurable_snd).inter (measurableSet_le measurable_snd hf)).inter (measurableSet_le measurable_snd hc)) exact measurable_const.ite hs measurable_const have hF : Measurable F := ((hMeasurable.comp (measurable_snd.prodMk measurable_fst)).mul (hHazard.2.1.comp measurable_snd)).mul hrisk exact hF.stronglyMeasurable.integral_prod_right'.measurable have hELp : MemLp E 2 μ := (memLp_two_iff_integrable_sq hEmeas.aestronglyMeasurable).2 (subject_event_payoff_square_integrable failureLaw censorLaw hazard hFailure hHazard H hPredictable hMeasurable i u hQuadratic) have hALp : MemLp A 2 μ := (memLp_two_iff_integrable_sq hAmeas.aestronglyMeasurable).2 (subject_hazard_square_integrable failureLaw censorLaw hazard hFailure hHazard H hMeasurable i u hQuadratic) constructor · change AEStronglyMeasurable (E - A) μ exact (hEmeas.sub hAmeas).aestronglyMeasurable · simpa [J, subjectIntegral, E, A, Pi.sub_apply] using (hELp.sub hALp).integrable_sq have hProd (i j : Fin n) : Integrable (fun x => J i x * J j x) μ := ((memLp_two_iff_integrable_sq (hSquare i).1).2 (hSquare i).2).integrable_mul ((memLp_two_iff_integrable_sq (hSquare j).1).2 (hSquare j).2) have hIso (i : Fin n) : (∫ x, (J i x) ^ 2 ∂μ) = ∫ x, Q i x ∂μ := subject_integral_isometry failureLaw censorLaw hazard hFailure hHazard H hPredictable hMeasurable i u hu hQuadratic have hCross (i j : Fin n) (hij : i ≠ j) : (∫ x, J i x * J j x ∂μ) = 0 := distinct_subject_integrals_orthogonal failureLaw censorLaw hazard hFailure hHazard H hPredictable hMeasurable i j hij u hu hQuadratic have hEnergyPath : ∀ᵐ x ∂μ, IntegrableOn (fun s => (H s x) ^ 2 * hazard s * (∑ i : Fin n, riskIndicator i s x)) (Icc 0 u) volume := by let e : Sample n → ℝ → ℝ := fun x s => (H s x) ^ 2 * hazard s * (∑ i : Fin n, riskIndicator i s x) let ν := (volume : Measure ℝ).restrict (Icc 0 u) have he_meas : Measurable (fun p : Sample n × ℝ => e p.1 p.2) := by have hrisk (i : Fin n) : Measurable (fun p : Sample n × ℝ => riskIndicator i p.2 p.1) := by unfold riskIndicator have hf : Measurable (fun p : Sample n × ℝ => (p.1 i).1) := by fun_prop have hc : Measurable (fun p : Sample n × ℝ => (p.1 i).2) := by fun_prop have hs : MeasurableSet {p : Sample n × ℝ | 0 ≤ p.2 ∧ p.2 ≤ (p.1 i).1 ∧ p.2 ≤ (p.1 i).2} := by simpa only [Set.ofPred_and, Set.inter_assoc, id_eq] using (((show MeasurableSet {p : Sample n × ℝ | (0 : ℝ) ≤ p.2} from measurableSet_le measurable_const measurable_snd).inter (measurableSet_le measurable_snd hf)).inter (measurableSet_le measurable_snd hc)) exact measurable_const.ite hs measurable_const exact (((hMeasurable.comp (measurable_snd.prodMk measurable_fst)).pow_const 2).mul (hHazard.2.1.comp measurable_snd)).mul (Finset.measurable_fun_sum _ (fun i _ => hrisk i)) have he_nonneg (x : Sample n) (s : ℝ) : 0 ≤ e x s := by dsimp [e] exact mul_nonneg (mul_nonneg (sq_nonneg _) (hHazard.2.2.1 s)) (Finset.sum_nonneg (fun i _ => by unfold riskIndicator; split_ifs <;> norm_num)) have he_inner_meas : Measurable (fun x => ∫⁻ s, ofReal (e x s) ∂ν) := he_meas.ennreal_ofReal.lintegral_prod_right' have hfinite : (∫⁻ x, ∫⁻ s, ofReal (e x s) ∂ν ∂μ) ≠ ⊤ := hQuadratic filter_upwards [ae_lt_top he_inner_meas hfinite] with x hx exact (lintegral_ofReal_ne_top_iff_integrable (he_meas.comp (measurable_const.prodMk measurable_id)).aestronglyMeasurable (Filter.Eventually.of_forall (he_nonneg x))).1 hx.ne have hQPath : ∀ᵐ x ∂μ, ∀ i : Fin n, IntegrableOn (fun s => (H s x) ^ 2 * hazard s * riskIndicator i s x) (Icc 0 u) volume := by apply ae_all_iff.2 intro i filter_upwards [hEnergyPath] with x hx have hmeas : Measurable (fun s => (H s x) ^ 2 * hazard s * riskIndicator i s x) := by have hrisk : Measurable (fun s : ℝ => riskIndicator i s x) := by unfold riskIndicator have hs : MeasurableSet {s : ℝ | 0 ≤ s ∧ s ≤ (x i).1 ∧ s ≤ (x i).2} := by simpa only [Set.ofPred_and, Set.inter_assoc, id_eq] using (((show MeasurableSet {s : ℝ | (0 : ℝ) ≤ s} from measurableSet_le measurable_const measurable_id).inter (measurableSet_le measurable_id measurable_const)).inter (measurableSet_le measurable_id measurable_const)) exact measurable_const.ite hs measurable_const exact ((hMeasurable.comp (measurable_id.prodMk measurable_const)).pow_const 2 |>.mul hHazard.2.1).mul hrisk exact hx.mono' hmeas.aestronglyMeasurable (Filter.Eventually.of_forall (fun s => by rw [Real.norm_eq_abs, abs_of_nonneg (mul_nonneg (mul_nonneg (sq_nonneg _) (hHazard.2.2.1 s)) (by unfold riskIndicator; split_ifs <;> norm_num))] exact mul_le_mul_of_nonneg_left (Finset.single_le_sum (f := fun j : Fin n => riskIndicator j s x) (fun j hj => by unfold riskIndicator; split_ifs <;> norm_num) (Finset.mem_univ i)) (mul_nonneg (sq_nonneg _) (hHazard.2.2.1 s)))) have hEnergyEq : (fun x => ∑ i : Fin n, Q i x) =ᵐ[μ] predictableEnergy hazard H u := by filter_upwards [hQPath] with x hx simp only [Q, predictableEnergy] rw [← integral_finsetSum univ (fun i _ => hx i)] congr 1 funext s rw [Finset.mul_sum] calc (∫ x : Sample n, (aggregateIntegral hazard H u x) ^ 2 ∂μ) = ∫ x : Sample n, ∑ i : Fin n, ∑ j : Fin n, J i x * J j x ∂μ := by apply integral_congr_ae filter_upwards [] with x simp only [aggregateIntegral, J, pow_two, Finset.sum_mul_sum] _ = ∑ i : Fin n, ∑ j : Fin n, ∫ x : Sample n, J i x * J j x ∂μ := by rw [integral_finsetSum univ (fun i _ => integrable_finsetSum univ (fun j _ => hProd i j))] apply Finset.sum_congr rfl intro i _ rw [integral_finsetSum univ (fun j _ => hProd i j)] _ = ∑ i : Fin n, ∫ x : Sample n, Q i x ∂μ := by apply Finset.sum_congr rfl intro i _ rw [Finset.sum_eq_single i] · simpa [pow_two] using hIso i · intro j _ hji exact hCross i j (Ne.symm hji) · simp _ = ∫ x : Sample n, predictableEnergy hazard H u x ∂μ := by rw [← integral_finsetSum univ (fun i _ => hQ i)] exact integral_congr_ae hEnergyEq

theorem subject_energy_integrable {n : ℕ} (failureLaw censorLaw : Measure ℝ) (hazard : ℝ → ℝ) (hFailure : NonnegativeTimeLaw failureLaw) (hHazard : HasCensorHazard censorLaw hazard) (H : ℝ → Sample n → ℝ) (hMeasurable : Measurable (fun p : ℝ × Sample n => H p.1 p.2)) (i : Fin n) (u : ℝ) (hQuadratic : QuadraticEnergyFinite failureLaw censorLaw hazard H u) (hEnergy : Integrable (predictableEnergy hazard H u) (sampleLaw n failureLaw censorLaw)) : Integrable (fun x : Sample n => ∫ s in Icc 0 u, (H s x) ^ 2 * hazard s * riskIndicator i s x ∂volume) (sampleLaw n failureLaw censorLaw) := by /- The nonnegative subject energy density is bounded by the sum density. `hQuadratic` gives almost-everywhere path integrability via Tonelli. Use integral monotonicity on those paths and `hEnergy` for the outer domination; joint measurability supplies the subject integral's strong measurability. -/ classical haveI : IsProbabilityMeasure failureLaw := ⟨hFailure.1⟩ haveI : IsProbabilityMeasure censorLaw := ⟨hHazard.1.1⟩ let μ := sampleLaw n failureLaw censorLaw let ν := (volume : Measure ℝ).restrict (Icc 0 u) haveI : IsProbabilityMeasure μ := by dsimp [μ, sampleLaw] infer_instance let e : Sample n → ℝ → ℝ := fun x s => (H s x) ^ 2 * hazard s * (∑ j : Fin n, riskIndicator j s x) let f : Sample n → ℝ → ℝ := fun x s => (H s x) ^ 2 * hazard s * riskIndicator i s x have hrisk (j : Fin n) : Measurable (fun p : Sample n × ℝ => riskIndicator j p.2 p.1) := by unfold riskIndicator have hf : Measurable (fun p : Sample n × ℝ => (p.1 j).1) := by fun_prop have hc : Measurable (fun p : Sample n × ℝ => (p.1 j).2) := by fun_prop have hs : MeasurableSet {p : Sample n × ℝ | 0 ≤ p.2 ∧ p.2 ≤ (p.1 j).1 ∧ p.2 ≤ (p.1 j).2} := by simpa only [Set.ofPred_and, Set.inter_assoc, id_eq] using (((show MeasurableSet {p : Sample n × ℝ | (0 : ℝ) ≤ p.2} from measurableSet_le measurable_const measurable_snd).inter (measurableSet_le measurable_snd hf)).inter (measurableSet_le measurable_snd hc)) exact measurable_const.ite hs measurable_const have hbase : Measurable (fun p : Sample n × ℝ => (H p.2 p.1) ^ 2 * hazard p.2) := ((hMeasurable.comp (measurable_snd.prodMk measurable_fst)).pow_const 2).mul (hHazard.2.1.comp measurable_snd) have he_meas : Measurable (fun p : Sample n × ℝ => e p.1 p.2) := hbase.mul (Finset.measurable_fun_sum _ (fun j _ => hrisk j)) have hf_meas : Measurable (fun p : Sample n × ℝ => f p.1 p.2) := hbase.mul (hrisk i) have he_nonneg (x : Sample n) (s : ℝ) : 0 ≤ e x s := by dsimp [e] exact mul_nonneg (mul_nonneg (sq_nonneg _) (hHazard.2.2.1 s)) (Finset.sum_nonneg (fun j _ => by unfold riskIndicator; split_ifs <;> norm_num)) have hf_nonneg (x : Sample n) (s : ℝ) : 0 ≤ f x s := by dsimp [f] exact mul_nonneg (mul_nonneg (sq_nonneg _) (hHazard.2.2.1 s)) (by unfold riskIndicator split_ifs <;> norm_num) have hf_le (x : Sample n) (s : ℝ) : f x s ≤ e x s := by dsimp [f, e] exact mul_le_mul_of_nonneg_left (Finset.single_le_sum (f := fun j : Fin n => riskIndicator j s x) (fun j hj => by unfold riskIndicator; split_ifs <;> norm_num) (Finset.mem_univ i)) (mul_nonneg (sq_nonneg _) (hHazard.2.2.1 s)) have he_joint : Integrable (fun p : Sample n × ℝ => e p.1 p.2) (μ.prod ν) := by apply (lintegral_ofReal_ne_top_iff_integrable he_meas.aestronglyMeasurable (Filter.Eventually.of_forall (fun p => he_nonneg p.1 p.2))).1 rw [lintegral_prod _ he_meas.ennreal_ofReal.aemeasurable] exact hQuadratic have he_path : ∀ᵐ x ∂μ, Integrable (e x) ν := he_joint.prod_right_ae have hf_path : ∀ᵐ x ∂μ, Integrable (f x) ν := by filter_upwards [he_path] with x hx exact hx.mono' (hf_meas.comp (measurable_const.prodMk measurable_id)).aestronglyMeasurable (Filter.Eventually.of_forall (fun s => by rw [Real.norm_eq_abs, abs_of_nonneg (hf_nonneg x s)] exact hf_le x s)) have hf_outer_meas : AEStronglyMeasurable (fun x => ∫ s, f x s ∂ν) μ := hf_meas.stronglyMeasurable.integral_prod_right'.aestronglyMeasurable apply integrable_of_le_of_le hf_outer_meas (Filter.Eventually.of_forall (fun x => integral_nonneg (hf_nonneg x))) ?_ (integrable_const 0) hEnergy filter_upwards [hf_path, he_path] with x hx hxe exact integral_mono hx hxe (hf_le x)

theorem nelsonAalen_squared_risk {n : ℕ} (failureLaw censorLaw : Measure ℝ) (hazard : ℝ → ℝ) (hFailure : NonnegativeTimeLaw failureLaw) (hHazard : HasCensorHazard censorLaw hazard) (u : ℝ) (hu : 0 ≤ u) : (∫ x : Sample n, (nelsonAalenError hazard u x) ^ 2 ∂sampleLaw n failureLaw censorLaw) = ∫ s in Icc 0 u, hazard s * (∫ x : Sample n, inverseRisk s x ∂sampleLaw n failureLaw censorLaw) ∂volume := by letI : IsProbabilityMeasure failureLaw := ⟨hFailure.1⟩ letI : IsProbabilityMeasure censorLaw := ⟨hHazard.1.1⟩ letI : IsProbabilityMeasure (sampleLaw n failureLaw censorLaw) := by unfold sampleLaw infer_instance let μ := sampleLaw n failureLaw censorLaw let ν := volume.restrict (Icc 0 u) have hprod : Integrable (fun p : Sample n × ℝ => hazard p.2 * inverseRisk p.2 p.1) (μ.prod ν) := inverseRisk_hazard_integrable_prod failureLaw censorLaw hazard hFailure hHazard u have hrewrite (x : Sample n) (s : ℝ) : (inverseRisk s x) ^ 2 * hazard s * (∑ i : Fin n, riskIndicator i s x) = hazard s * inverseRisk s x := by calc _ = hazard s * ((inverseRisk s x) ^ 2 * (∑ i : Fin n, riskIndicator i s x)) := by ring _ = hazard s * inverseRisk s x := by rw [inverseRisk_square_risk] calc _ = ∫ x : Sample n, predictableEnergy hazard (inverseRisk (n := n)) u x ∂μ := by simpa only [nelsonAalenError, μ] using aggregate_integral_isometry failureLaw censorLaw hazard hFailure hHazard (inverseRisk (n := n)) inverseRisk_leftPredictable inverseRisk_jointMeasurable u hu (inverseRisk_quadratic_energy_finite failureLaw censorLaw hazard hFailure hHazard u) (inverseRisk_energy_integrable failureLaw censorLaw hazard hFailure hHazard u) _ = ∫ x : Sample n, ∫ s : ℝ, hazard s * inverseRisk s x ∂ν ∂μ := by simp_rw [predictableEnergy, hrewrite] rfl _ = ∫ s : ℝ, ∫ x : Sample n, hazard s * inverseRisk s x ∂μ ∂ν := by exact integral_integral_swap hprod _ = ∫ s : ℝ, hazard s * (∫ x : Sample n, inverseRisk s x ∂μ) ∂ν := by simp_rw [integral_const_mul] _ = _ := rfl

theorem distinct_censor_times_ae {n : ℕ} (failureLaw censorLaw : Measure ℝ) (hazard : ℝ → ℝ) (hFailure : NonnegativeTimeLaw failureLaw) (hHazard : HasCensorHazard censorLaw hazard) (i j : Fin n) (hij : i ≠ j) : ∀ᵐ x ∂sampleLaw n failureLaw censorLaw, (x i).2 ≠ (x j).2 := by haveI : IsProbabilityMeasure failureLaw := ⟨hFailure.1⟩ haveI : IsProbabilityMeasure censorLaw := ⟨hHazard.1.1⟩ haveI : NullSingletonClass censorLaw := by rw [hHazard.2.2.2.2] infer_instance haveI : IsProbabilityMeasure (failureLaw.prod censorLaw) := inferInstance haveI : IsProbabilityMeasure (sampleLaw n failureLaw censorLaw) := by unfold sampleLaw infer_instance have hmap (k : Fin n) : (sampleLaw n failureLaw censorLaw).map (fun x => (x k).2) = censorLaw := by change (Measure.pi (fun _ : Fin n => failureLaw.prod censorLaw)).map (fun x => (x k).2) = censorLaw calc _ = Measure.map snd (Measure.map (Function.eval k) (Measure.pi (fun _ : Fin n => failureLaw.prod censorLaw))) := by rw [Measure.map_map measurable_snd (measurable_pi_apply k)] rfl _ = censorLaw := by rw [(measurePreserving_eval (fun _ : Fin n => failureLaw.prod censorLaw) k).map_eq, Measure.map_snd_prod, measure_univ, one_smul] have hind : IndepFun (fun x : Sample n => (x i).2) (fun x : Sample n => (x j).2) (sampleLaw n failureLaw censorLaw) := by have h := ProbabilityTheory.iIndepFun_pi (μ := fun _ : Fin n => failureLaw.prod censorLaw) (X := fun _ => snd) (fun _ => measurable_snd.aemeasurable) exact h.indepFun hij have hprod : (∀ᵐ z ∂censorLaw.prod censorLaw, z.1 ≠ z.2) := by apply (Measure.ae_prod_iff_ae_ae (measurableSet_eq_fun measurable_fst measurable_snd).compl).2 filter_upwards [] with a exact (censorLaw.ae_ne a).mono (fun b hb => Ne.symm hb) have hpair := hind.map_prod_eq_prod_map_map ((measurable_pi_apply i).snd.aemeasurable : AEMeasurable (fun x : Sample n => (x i).2) (sampleLaw n failureLaw censorLaw)) ((measurable_pi_apply j).snd.aemeasurable : AEMeasurable (fun x : Sample n => (x j).2) (sampleLaw n failureLaw censorLaw)) rw [hmap i, hmap j] at hpair have hp : MeasurableSet {z : ℝ × ℝ | z.1 ≠ z.2} := (measurableSet_eq_fun measurable_fst measurable_snd).compl exact (ae_map_iff (by fun_prop : AEMeasurable (fun x : Sample n => ((x i).2, (x j).2)) (sampleLaw n failureLaw censorLaw)) hp).1 (hpair.symm ▸ hprod)

theorem subject_hazard_stops_at_censor {n : ℕ} (hazard : ℝ → ℝ) (H : ℝ → Sample n → ℝ) (i : Fin n) (x : Sample n) (u : ℝ) (hcu : (x i).2 ≤ u) : (∫ s in Icc 0 u, H s x * hazard s * riskIndicator i s x ∂volume) = ∫ s in Icc 0 (x i).2, H s x * hazard s * riskIndicator i s x ∂volume := by apply setIntegral_eq_of_subset_of_forall_sdiff_eq_zero measurableSet_Icc · exact Set.Icc_subset_Icc_right hcu · intro s hs have hcs : (x i).2 < s := by by_contra h exact hs.2 ⟨hs.1.1, le_of_not_gt h⟩ simp [riskIndicator, not_le.mpr hcs]

theorem subject_prefix_mixed_predictable {n : ℕ} (hazard : ℝ → ℝ) (H : ℝ → Sample n → ℝ) (hPredictable : LeftPredictable H) (i : Fin n) : LeftPredictable (fun s x => (∫ t in Icc 0 s, H t x * hazard t * riskIndicator i t x ∂volume) * H s x) := by have hRisk (t : ℝ) (z : Sample n) (hf : t ≠ (z i).1) (hc : t ≠ (z i).2) : riskIndicator i t z = if 0 ≤ t ∧ censorCount i t z = 0 ∧ failureCount i t z = 0 then 1 else 0 := by by_cases h0 : 0 ≤ t · rcases lt_or_gt_of_ne hf with htf | htf · rcases lt_or_gt_of_ne hc with htc | htc · simp [riskIndicator, censorCount, failureCount, h0, htf, htc, le_of_lt] · have hcf : (z i).2 < (z i).1 := lt_trans htc htf simp [riskIndicator, censorCount, failureCount, h0, htf, htc, hcf, le_of_lt] · rcases lt_or_gt_of_ne hc with htc | htc · have hfc : (z i).1 < (z i).2 := lt_trans htf htc simp [riskIndicator, censorCount, failureCount, h0, htf, htc, hfc, le_of_lt] · by_cases hfc : (z i).1 ≤ (z i).2 · simp [riskIndicator, censorCount, failureCount, h0, htf, htc, hfc, le_of_lt] · have hcf : (z i).2 < (z i).1 := lt_of_not_ge hfc simp [riskIndicator, censorCount, failureCount, h0, htf, htc, hcf, le_of_lt] · simp [riskIndicator, censorCount, failureCount, h0] have hNe (a : ℝ) : ∀ᵐ t ∂(volume : Measure ℝ), t ≠ a := by rw [ae_iff] simpa only [not_ne_iff, Set.ofPred_eq_eq_singleton] using (measure_singleton a : (volume : Measure ℝ) {a} = 0) intro s x y hHist have hHs : H s x = H s y := hPredictable s x y hHist have hInt : (∫ t in Icc 0 s, H t x * hazard t * riskIndicator i t x ∂volume) = ∫ t in Icc 0 s, H t y * hazard t * riskIndicator i t y ∂volume := by rw [integral_Icc_eq_integral_Ico, integral_Icc_eq_integral_Ico] apply integral_congr_ae have hxF := ae_restrict_of_ae (s := Ico 0 s) (hNe (x i).1) have hxC := ae_restrict_of_ae (s := Ico 0 s) (hNe (x i).2) have hyF := ae_restrict_of_ae (s := Ico 0 s) (hNe (y i).1) have hyC := ae_restrict_of_ae (s := Ico 0 s) (hNe (y i).2) have htMem : ∀ᵐ t ∂(volume : Measure ℝ).restrict (Ico 0 s), t ∈ Ico 0 s := ae_restrict_mem measurableSet_Ico filter_upwards [hxF, hxC, hyF, hyC, htMem] with t hxF hxC hyF hyC ht have hHistory := hHist i t ht.2 have hHt : H t x = H t y := hPredictable t x y (fun j u hu => hHist j u (lt_trans hu ht.2)) rw [hHt, hRisk t x hxF hxC, hRisk t y hyF hyC, hHistory.1, hHistory.2] change (∫ t in Icc 0 s, H t x * hazard t * riskIndicator i t x ∂volume) * H s x = (∫ t in Icc 0 s, H t y * hazard t * riskIndicator i t y ∂volume) * H s y rw [hInt, hHs]

theorem lintegral_resample_censor {n : ℕ} (failureLaw censorLaw : Measure ℝ) (hFailure : NonnegativeTimeLaw failureLaw) (hCensor : NonnegativeTimeLaw censorLaw) (F : Sample n → ENNReal) (hF : Measurable F) (i : Fin n) : (∫⁻ x : Sample n, F x ∂sampleLaw n failureLaw censorLaw) = ∫⁻ x : Sample n, ∫⁻ c : ℝ, F (update x i ((x i).1, c)) ∂censorLaw ∂sampleLaw n failureLaw censorLaw := by classical have : IsProbabilityMeasure failureLaw := ⟨hFailure.1⟩ have : IsProbabilityMeasure censorLaw := ⟨hCensor.1⟩ let μ : Fin n → Measure (ℝ × ℝ) := fun _ => failureLaw.prod censorLaw let G : Sample n → ENNReal := fun x => ∫⁻ c : ℝ, F (update x i ((x i).1, c)) ∂censorLaw have hG : Measurable G := by dsimp [G] apply Measurable.lintegral_prod_right fun_prop change (∫⁻ x, F x ∂Measure.pi μ) = ∫⁻ x, G x ∂Measure.pi μ apply lintegral_eq_of_lmarginal_eq {i} hF hG rw [lmarginal_singleton, lmarginal_singleton] funext x dsimp [μ, G] simp only [Function.update_idem] rw [lintegral_prod _ (by fun_prop)] rw [lintegral_prod _ (by fun_prop)] simp

theorem lintegral_random_horizon (evaluationLaw : Measure ℝ) (hEvaluation : NonnegativeTimeLaw evaluationLaw) (f : ℝ → ENNReal) (hf : Measurable f) : (∫⁻ u : ℝ, ∫⁻ s in Icc 0 u, f s ∂volume ∂evaluationLaw) = ∫⁻ s : ℝ, f s * evaluationLaw (Ici s) ∂(volume.restrict (Ici (0 : ℝ))) := by /- Use Tonelli on `(u,s) ↦ 1_{0≤s≤u} f(s)`; the `u` section is `evaluationLaw (Ici s)` and the `s` section is the restricted time integral. -/ classical haveI : IsProbabilityMeasure evaluationLaw := ⟨hEvaluation.1⟩ have hkernel : Measurable (fun p : ℝ × ℝ => (Icc 0 p.1).indicator f p.2) := by have hset : MeasurableSet {p : ℝ × ℝ | 0 ≤ p.2 ∧ p.2 ≤ p.1} := (measurableSet_le measurable_const measurable_snd).inter (measurableSet_le measurable_snd measurable_fst) simpa only [indicator, Set.mem_Icc, Function.comp_def] using (@Measurable.ite (ℝ × ℝ) ENNReal (f ∘ snd) (fun _ => 0) _ _ (fun p => 0 ≤ p.2 ∧ p.2 ≤ p.1) (Classical.decPred _) hset (hf.comp measurable_snd) measurable_const) calc (∫⁻ u : ℝ, ∫⁻ s in Icc 0 u, f s ∂volume ∂evaluationLaw) = ∫⁻ u : ℝ, ∫⁻ s : ℝ, (Icc 0 u).indicator f s ∂volume ∂evaluationLaw := by apply lintegral_congr intro u exact (lintegral_indicator measurableSet_Icc f).symm _ = ∫⁻ s : ℝ, ∫⁻ u : ℝ, (Icc 0 u).indicator f s ∂evaluationLaw ∂volume := lintegral_lintegral_swap hkernel.aemeasurable _ = ∫⁻ s : ℝ, (Ici (0 : ℝ)).indicator (fun s => f s * evaluationLaw (Ici s)) s ∂volume := by apply lintegral_congr intro s by_cases hs : 0 ≤ s · have hsection : (fun u : ℝ => (Icc 0 u).indicator f s) = (Ici s).indicator (fun _ => f s) := by funext u simp [indicator, hs, Set.mem_Icc, Set.mem_Ici] rw [hsection, lintegral_indicator_const measurableSet_Ici] simp [indicator, hs] · have hsection : (fun u : ℝ => (Icc 0 u).indicator f s) = fun _ => 0 := by funext u simp [indicator, hs, Set.mem_Icc] rw [hsection] simp [indicator, hs] _ = ∫⁻ s : ℝ, f s * evaluationLaw (Ici s) ∂(volume.restrict (Ici (0 : ℝ))) := lintegral_indicator measurableSet_Ici _

theorem subject_integral_isometry {n : ℕ} (failureLaw censorLaw : Measure ℝ) (hazard : ℝ → ℝ) (hFailure : NonnegativeTimeLaw failureLaw) (hHazard : HasCensorHazard censorLaw hazard) (H : ℝ → Sample n → ℝ) (hPredictable : LeftPredictable H) (hMeasurable : Measurable (fun p : ℝ × Sample n => H p.1 p.2)) (i : Fin n) (u : ℝ) (hu : 0 ≤ u) (hQuadratic : QuadraticEnergyFinite failureLaw censorLaw hazard H u) : (∫ x : Sample n, (subjectIntegral hazard H i u x) ^ 2 ∂sampleLaw n failureLaw censorLaw) = ∫ x : Sample n, (∫ s in Icc 0 u, (H s x) ^ 2 * hazard s * riskIndicator i s x ∂volume) ∂sampleLaw n failureLaw censorLaw := by /- Write the subject integral as J - B. `subject_event_square_expectation` gives E[J²] = E[energy], while `subject_jump_compensator_cancellation` gives E[2 J B - B²] = 0. Establish integrability of J² from the event-square bridge and of B² from `subject_hazard_square_integrable`; then split the integral of (J - B)², using the cancellation identity. -/ classical let μ := sampleLaw n failureLaw censorLaw let Q : ℝ → Sample n → ℝ := fun s x => (H s x) ^ 2 have hQpred : LeftPredictable Q := by intro s x y hxy simpa [Q] using congrArg (fun z : ℝ => z ^ 2) (hPredictable s x y hxy) have hQmeas : Measurable (fun p : ℝ × Sample n => Q p.1 p.2) := hMeasurable.pow_const 2 have hlin := predictable_censor_compensator_lintegral failureLaw censorLaw hazard hFailure hHazard Q hQpred hQmeas (fun s x => sq_nonneg _) i u have hfinite : (∫⁻ x : Sample n, ∫⁻ s in Icc 0 u, ofReal (Q s x * hazard s * riskIndicator i s x) ∂volume ∂μ) ≠ ⊤ := by have hle : (∫⁻ x : Sample n, ∫⁻ s in Icc 0 u, ofReal (Q s x * hazard s * riskIndicator i s x) ∂volume ∂μ) ≤ ∫⁻ x : Sample n, ∫⁻ s in Icc 0 u, ofReal ((H s x) ^ 2 * hazard s * (∑ j : Fin n, riskIndicator j s x)) ∂volume ∂μ := by apply lintegral_mono intro x apply lintegral_mono intro s apply ENNReal.ofReal_le_ofReal dsimp [Q] apply mul_le_mul_of_nonneg_left · exact Finset.single_le_sum (f := fun j : Fin n => riskIndicator j s x) (fun j hj => by unfold riskIndicator; split_ifs <;> norm_num) (Finset.mem_univ i) · exact mul_nonneg (sq_nonneg _) (hHazard.2.2.1 s) exact ne_top_of_le_ne_top hQuadratic hle have hEventQ : Integrable (fun x : Sample n => if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then Q (x i).2 x else 0) μ := by have hm : Measurable (fun x : Sample n => if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then Q (x i).2 x else 0) := by have hc : Measurable (fun x : Sample n => (x i).2) := by fun_prop have hf : Measurable (fun x : Sample n => (x i).1) := by fun_prop exact (hQmeas.comp (hc.prodMk measurable_id)).ite ((measurableSet_le hc measurable_const).inter (measurableSet_lt hc hf)) measurable_const apply (lintegral_ofReal_ne_top_iff_integrable hm.aestronglyMeasurable (by filter_upwards [] with x split_ifs <;> positivity)).1 rw [hlin] exact hfinite have hEventSquare : Integrable (fun x : Sample n => (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then H (x i).2 x else 0) ^ 2) μ := by convert hEventQ using 1 <;> simp only [Q, ite_pow, zero_pow (by decide : (2 : ℕ) ≠ 0)] have hSquare := subject_hazard_square_integrable failureLaw censorLaw hazard hFailure hHazard H hMeasurable i u hQuadratic haveI : IsProbabilityMeasure failureLaw := ⟨hFailure.1⟩ haveI : IsProbabilityMeasure censorLaw := ⟨hHazard.1.1⟩ haveI : IsProbabilityMeasure (failureLaw.prod censorLaw) := inferInstance have hCensor : ∀ᵐ c ∂censorLaw, 0 ≤ c := (mem_ae_iff_prob_eq_one measurableSet_Ici).2 hHazard.1.2 have hPair : ∀ᵐ z ∂failureLaw.prod censorLaw, 0 ≤ z.2 := by apply (Measure.ae_prod_iff_ae_ae (measurableSet_le measurable_const measurable_snd)).2 filter_upwards [] with a exact hCensor have hCensorSample : ∀ᵐ x ∂μ, 0 ≤ (x i).2 := by unfold μ sampleLaw exact (Measure.tendsto_eval_ae_ae (μ := fun _ : Fin n => failureLaw.prod censorLaw) (i := i)) hPair have hStopped := subject_prefix_mixed_event_integrable failureLaw censorLaw hazard hFailure hHazard H hPredictable hMeasurable i u hu hQuadratic have hMixedAE : (fun x : Sample n => if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then (∫ t in Icc 0 (x i).2, H t x * hazard t * riskIndicator i t x ∂volume) * H (x i).2 x else 0) =ᵐ[μ] (fun x : Sample n => (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then H (x i).2 x else 0) * (∫ s in Icc 0 u, H s x * hazard s * riskIndicator i s x ∂volume)) := by filter_upwards [hCensorSample, subject_hazard_path_integrable_ae failureLaw censorLaw hazard hHazard H hMeasurable i u hQuadratic] with x hc0 hPath by_cases hEvent : (x i).2 ≤ u ∧ (x i).2 < (x i).1 · simp only [if_pos hEvent] rw [mul_comm (H (x i).2 x), subject_mixed_event_stops hazard H i x u hEvent.1] · simp [hEvent] have hMixed := hStopped.congr hMixedAE have hCross : Integrable (fun x : Sample n => 2 * (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then H (x i).2 x else 0) * (∫ s in Icc 0 u, H s x * hazard s * riskIndicator i s x ∂volume)) μ := by apply (hMixed.const_mul 2).congr filter_upwards [] with x ring have hCancel := hCross.sub hSquare calc (∫ x : Sample n, (subjectIntegral hazard H i u x) ^ 2 ∂μ) = ∫ x : Sample n, (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then H (x i).2 x else 0) ^ 2 - (2 * (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then H (x i).2 x else 0) * (∫ s in Icc 0 u, H s x * hazard s * riskIndicator i s x ∂volume) - (∫ s in Icc 0 u, H s x * hazard s * riskIndicator i s x ∂volume) ^ 2) ∂μ := by apply integral_congr_ae filter_upwards [] with x unfold subjectIntegral ring _ = (∫ x : Sample n, (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then H (x i).2 x else 0) ^ 2 ∂μ) - (∫ x : Sample n, 2 * (if (x i).2 ≤ u ∧ (x i).2 < (x i).1 then H (x i).2 x else 0) * (∫ s in Icc 0 u, H s x * hazard s * riskIndicator i s x ∂volume) - (∫ s in Icc 0 u, H s x * hazard s * riskIndicator i s x ∂volume) ^ 2 ∂μ) := integral_sub hEventSquare hCancel _ = _ := by rw [subject_jump_compensator_cancellation failureLaw censorLaw hazard hFailure hHazard H hPredictable hMeasurable i u hu hQuadratic, sub_zero] exact subject_event_square_expectation failureLaw censorLaw hazard hFailure hHazard H hPredictable hMeasurable i u hQuadratic