Stat.Recurrent­Event.Counting­Process.Finite­Jump

theorem SampleModel.subject_integral_isometry (S : SampleModel n Ω μ) [IsProbabilityMeasure μ] (H : ℝ → (Fin n → Ω) → ℝ) (hH : S.LeftPredictable H) (hbound : ∃ C : ℝ, ∀ t x, |H t x| ≤ C) (i : Fin n) : (∫ x, (S.subjectIntegral H i x) ^ 2 ∂finiteSampleLaw n μ) = ∫ x, S.subjectEnergy H i x ∂finiteSampleLaw n μ := by exact (S.process i).stochasticIntegral_isometry H (S.process_predictable H hH i) hbound

theorem SampleModel.crossPayoff_integrable (S : SampleModel n Ω μ) [IsProbabilityMeasure μ] (H : ℝ → (Fin n → Ω) → ℝ) (hH : S.LeftPredictable H) (hbound : ∃ C : ℝ, ∀ t x, |H t x| ≤ C) (i j : Fin n) : Integrable ((S.process i).jumpIntegral (fun t x => |S.crossPayoff H j t x|) (S.process i).horizon) (finiteSampleLaw n μ) ∧ Integrable ((S.process i).energyIntegral (fun t x => |S.crossPayoff H j t x|) (S.process i).horizon) (finiteSampleLaw n μ) := by exact ⟨S.crossPayoff_jump_abs_integrable H hH hbound i j, S.crossPayoff_energy_abs_integrable H hH hbound i j⟩

theorem Model.energyOccupation_indicator (M : Model Ω μ) [IsProbabilityMeasure μ] (S : Set (ℝ × Ω)) (hS : MeasurableSet S) (henergy : Integrable (M.energyIntegral (fun t ω => S.indicator (fun _ => (1 : ℝ)) (t, ω)) M.horizon) μ) : (M.energyOccupation S).toReal = ∫ ω, M.energyIntegral (fun t ω => S.indicator (fun _ => (1 : ℝ)) (t, ω)) M.horizon ω ∂μ := by let r : ℝ × Ω → ℝ := fun p => M.atRisk p.1 p.2 * M.intensity p.1 p.2 let f : ℝ × Ω → ℝ := fun p => S.indicator (fun _ => (1 : ℝ)) p * r p have hrmeas : Measurable r := M.atRisk_joint_measurable.mul M.intensity_joint_measurable have hfmeas : Measurable f := (measurable_const.indicator hS).mul hrmeas have hfnonneg : ∀ p, 0 ≤ f p := by intro p by_cases hp : p ∈ S <;> simp [f, r, indicator, hp, mul_nonneg (M.atRisk_nonneg p.1 p.2) (M.intensity_nonneg p.1 p.2)] have hsection (ω : Ω) : Integrable (fun t => f (t, ω)) (volume.restrict (Ioc 0 M.horizon)) := by have hs : MeasurableSet {t : ℝ | (t, ω) ∈ S} := hS.preimage measurable_prodMk_right have h := (M.rate_integrable ω).indicator hs change Integrable (indicator {t : ℝ | (t, ω) ∈ S} (fun t => M.atRisk t ω * M.intensity t ω)) (volume.restrict (Ioc 0 M.horizon)) at h convert h using 1 funext t by_cases ht : (t, ω) ∈ S <;> simp [f, r, indicator, ht] have htime (ω : Ω) : ∫⁻ t, ofReal (f (t, ω)) ∂(volume.restrict (Ioc 0 M.horizon)) = ofReal (M.energyIntegral (fun t ω => S.indicator (fun _ => (1 : ℝ)) (t, ω)) M.horizon ω) := by rw [← ofReal_integral_eq_lintegral_ofReal (hsection ω) (Filter.Eventually.of_forall (fun t => hfnonneg (t, ω)))] rfl have hmass : M.energyOccupation S = ∫⁻ ω, ofReal (M.energyIntegral (fun t ω => S.indicator (fun _ => (1 : ℝ)) (t, ω)) M.horizon ω) ∂μ := by rw [Model.energyOccupation, withDensity_apply _ hS] rw [← lintegral_indicator hS] have hpoint : S.indicator (fun p => ofReal (r p)) = fun p => ofReal (f p) := by funext p by_cases hp : p ∈ S <;> simp [f, indicator, hp] rw [hpoint, lintegral_prod_symm' _ hfmeas.ennreal_ofReal] simp_rw [htime] have hnonneg : ∀ ω, 0 ≤ M.energyIntegral (fun t ω => S.indicator (fun _ => (1 : ℝ)) (t, ω)) M.horizon ω := by intro ω change 0 ≤ ∫ t in Ioc 0 M.horizon, f (t, ω) ∂volume exact integral_nonneg (fun t => hfnonneg (t, ω)) have hreal := ofReal_integral_eq_lintegral_ofReal henergy (Filter.Eventually.of_forall hnonneg) rw [← hmass] at hreal rw [← hreal] exact ENNReal.toReal_ofReal (integral_nonneg hnonneg)

theorem Model.jumpIntegral_eq_sum_jumpTime (M : Model Ω μ) (H : ℝ → Ω → ℝ) (ω : Ω) : M.jumpIntegral H M.horizon ω = ∑ k ∈ range (M.eventTimes ω).card, H (M.jumpTime k ω) ω := by classical let s := M.eventTimes ω have hfilter : s.filter (· ≤ M.horizon) = s := Finset.filter_eq_self.mpr (fun t ht => (M.events_in_horizon ω t ht).2) have hsub : (range s.card).image (fun k => M.jumpTime k ω) ⊆ s := by intro t ht obtain ⟨k, hk, rfl⟩ := Finset.mem_image.mp ht exact M.jumpTime_mem k ω (Finset.mem_range.mp hk) have hinj : InjOn (fun k => M.jumpTime k ω) (range s.card) := by intro i hi j hj hij exact M.jumpTime_injective ω i j (Finset.mem_range.mp hi) (Finset.mem_range.mp hj) hij have himage : (range s.card).image (fun k => M.jumpTime k ω) = s := by apply Finset.eq_of_subset_of_card_le hsub rw [Finset.card_image_of_injOn hinj, Finset.card_range] change (∑ t ∈ s.filter (· ≤ M.horizon), H t ω) = _ rw [hfilter, ← himage, Finset.sum_image hinj]

theorem Model.jumpOccupation_indicator (M : Model Ω μ) [IsProbabilityMeasure μ] (S : Set (ℝ × Ω)) (hS : MeasurableSet S) (hjump : Integrable (M.jumpIntegral (fun t ω => S.indicator (fun _ => (1 : ℝ)) (t, ω)) M.horizon) μ) : (M.jumpOccupation S).toReal = ∫ ω, M.jumpIntegral (fun t ω => S.indicator (fun _ => (1 : ℝ)) (t, ω)) M.horizon ω ∂μ := by let F : Ω → ℝ := M.jumpIntegral (fun t ω => S.indicator (fun _ => (1 : ℝ)) (t, ω)) M.horizon have hnonneg : ∀ ω, 0 ≤ F ω := by intro ω change 0 ≤ M.jumpIntegral (fun t ω => S.indicator (fun _ => (1 : ℝ)) (t, ω)) M.horizon ω rw [M.jumpIntegral_eq_sum_jumpTime] apply Finset.sum_nonneg intro k hk unfold indicator split_ifs <;> norm_num have hlintegral : ofReal (∫ ω, F ω ∂μ) = M.jumpOccupation S := by rw [M.jumpOccupation_apply S hS] exact ofReal_integral_eq_lintegral_ofReal hjump (Filter.Eventually.of_forall hnonneg) rw [← hlintegral] exact ENNReal.toReal_ofReal (integral_nonneg hnonneg)

theorem Model.tendsto_expected_jumpIntegral (M : Model Ω μ) [IsProbabilityMeasure μ] (G : ℕ → ℝ → Ω → ℝ) (H : ℝ → Ω → ℝ) (hG : ∀ k, M.Predictable (G k)) (C : ℝ) (hbound : ∀ k t ω, |G k t ω| ≤ C) (hlim : ∀ t ω, Tendsto (fun k => G k t ω) atTop (nhds (H t ω))) : Tendsto (fun k => ∫ ω, M.jumpIntegral (G k) M.horizon ω ∂μ) atTop (nhds (∫ ω, M.jumpIntegral H M.horizon ω ∂μ)) := by /- First commute the limit with the fixed finite event sum on each path (`tendsto_finset_sum`). The integrable envelope is C times event count, from `integrable_eventCount` and `abs_jumpIntegral_le_card`. Use Mathlib's `tendsto_integral_of_dominated_convergence`; no intensity identity is used. -/ classical apply tendsto_integral_of_dominated_convergence (fun ω => C * ((M.eventTimes ω).card : ℝ)) · intro k exact (M.measurable_jumpIntegral (G k) (M.predictable_joint_measurable (G k) (hG k))).aestronglyMeasurable · exact M.integrable_eventCount.const_mul C · intro k exact Eventually.of_forall (fun ω => by simpa only [Real.norm_eq_abs] using M.abs_jumpIntegral_le_card (G k) C (hbound k) ω) · apply Eventually.of_forall intro ω unfold Model.jumpIntegral exact tendsto_finsetSum _ (fun t _ => hlim t ω)

theorem Model.integrable_jump (M : Model Ω μ) [IsProbabilityMeasure μ] (H : ℝ → Ω → ℝ) (hH : M.Predictable H) (hbound : ∃ C : ℝ, ∀ t ω, |H t ω| ≤ C) : Integrable (M.jumpIntegral H M.horizon) μ := by obtain ⟨C, hC⟩ := hbound apply (M.integrable_eventCount.const_mul |C|).mono' (M.measurable_jumpIntegral H (M.predictable_joint_measurable H hH)).aestronglyMeasurable filter_upwards [] with ω simpa only [Real.norm_eq_abs] using M.abs_jumpIntegral_le_card H |C| (fun t ω => (hC t ω).trans (le_abs_self C)) ω

theorem Model.predictable_compensator (M : Model Ω μ) [IsProbabilityMeasure μ] (G : ℝ → Ω → ℝ) (hG : M.Predictable G) (hjumpAbs : Integrable (M.jumpIntegral (fun t ω => |G t ω|) M.horizon) μ) : (∫ ω, M.jumpIntegral G M.horizon ω ∂μ) = ∫ ω, M.energyIntegral G M.horizon ω ∂μ := by /- Cutoffs are bounded and dominated by |G|. Absolute time-sample integrability is derived, not added as a new caller hypothesis. -/ let A (k : ℕ) (t : ℝ) (ω : Ω) : ℝ := if |G t ω| ≤ (k : ℝ) then G t ω else 0 have hA (k : ℕ) : M.Predictable (A k) := by letI : MeasurableSpace (ℝ × Ω) := predictableSpace M.filtration change Measurable[predictableSpace M.filtration] (fun p : ℝ × Ω => if |G p.1 p.2| ≤ (k : ℝ) then G p.1 p.2 else 0) apply Measurable.ite · exact hG.abs measurableSet_Iic · exact hG · exact measurable_const have hbound (k : ℕ) : ∃ C : ℝ, ∀ t ω, |A k t ω| ≤ C := by refine ⟨(k : ℝ), ?_⟩ intro t ω dsimp [A] split_ifs with h · exact h · simp have hdom : ∀ k t ω, |A k t ω| ≤ |G t ω| := by intro k t ω dsimp [A] split_ifs <;> simp have hlim (t : ℝ) (ω : Ω) : Tendsto (fun k => A k t ω) atTop (nhds (G t ω)) := by obtain ⟨K, hK⟩ := exists_nat_ge |G t ω| apply tendsto_const_nhds.congr' filter_upwards [eventually_ge_atTop K] with k hk simp [A, hK.trans (Nat.cast_le.mpr hk)] have hj := M.tendsto_expected_jumpIntegral_of_dominated A G hA hdom hjumpAbs hlim have he := M.tendsto_expected_energyIntegral_of_dominated A G hA hG hdom (M.predictable_rate_product_integrable G hG hjumpAbs) hlim have heq (k : ℕ) : (∫ ω, M.jumpIntegral (A k) M.horizon ω ∂μ) = ∫ ω, M.energyIntegral (A k) M.horizon ω ∂μ := M.bounded_predictable_compensator (A k) (hA k) (hbound k) exact tendsto_nhds_unique hj (by simpa only [heq] using he)

theorem Model.energyIntegral_square (M : Model Ω μ) (H : ℝ → Ω → ℝ) (hH : M.Predictable H) (hbound : ∃ C : ℝ, ∀ t ω, |H t ω| ≤ C) (ω : Ω) : (M.energyIntegral H M.horizon ω) ^ 2 = 2 * ∫ t in Ioc 0 M.horizon, M.energyIntegral H t ω * (H t ω * (M.atRisk t ω * M.intensity t ω)) ∂volume := by let f : ℝ → ℝ := fun t => H t ω * (M.atRisk t ω * M.intensity t ω) let F : ℝ → ℝ := fun t => ∫ s in (0 : ℝ)..t, f s have hHjoint : Measurable (fun p : ℝ × Ω => H p.1 p.2) := by apply Measurable.le ?_ hH apply (MeasurableSpace.generateFrom_le_iff _).mpr rintro S ⟨a, b, B, hB, rfl⟩ exact measurableSet_Ioc.prod ((M.filtration_le a) B hB) have hHm : Measurable (fun t => H t ω) := hHjoint.comp (measurable_id.prodMk measurable_const) have hrate : Integrable (fun t => M.atRisk t ω * M.intensity t ω) (volume.restrict (Ioc 0 M.horizon)) := M.rate_integrable ω obtain ⟨C, hC⟩ := hbound have hf : Integrable f (volume.restrict (Ioc 0 M.horizon)) := by apply Integrable.mono' (hrate.abs.const_mul |C|) · exact (hHm.mul ((M.atRisk_joint_measurable.comp (measurable_id.prodMk measurable_const)).mul (M.intensity_joint_measurable.comp (measurable_id.prodMk measurable_const)))).aestronglyMeasurable · filter_upwards with t simp only [Real.norm_eq_abs, f, abs_mul] have hle : |H t ω| ≤ |C| := (hC t ω).trans (le_abs_self C) exact mul_le_mul_of_nonneg_right hle (mul_nonneg (abs_nonneg _) (abs_nonneg _)) have hfi : IntervalIntegrable f volume 0 M.horizon := (intervalIntegrable_iff_integrableOn_Ioc_of_le M.horizon_pos.le).2 hf have hF : AbsolutelyContinuousOnInterval F 0 M.horizon := hfi.absolutelyContinuousOnInterval_intervalIntegral (by simp) have hprod := hF.integral_deriv_mul_eq_sub hF have hderiv := hfi.ae_hasDerivAt_integral have heq : (∫ t in (0 : ℝ)..M.horizon, deriv F t * F t + F t * deriv F t) = ∫ t in (0 : ℝ)..M.horizon, 2 * F t * f t := by apply intervalIntegral.integral_congr_ae filter_upwards [hderiv] with t ht htm have htIcc : t ∈ Icc (0 : ℝ) M.horizon := by simpa [uIcc_of_le M.horizon_pos.le] using (uIoc_subset_uIcc htm) have hd : deriv F t = f t := (ht (by simpa [uIcc_of_le M.horizon_pos.le] using htIcc) 0 (by simp)).deriv rw [hd] ring rw [heq] at hprod have hzero : F 0 = 0 := by simp [F] have hfinal : F M.horizon = M.energyIntegral H M.horizon ω := by simp [F, f, Model.energyIntegral, intervalIntegral.integral_of_le M.horizon_pos.le] rw [hzero, hfinal] at hprod simp only [zero_mul, sub_zero] at hprod calc (M.energyIntegral H M.horizon ω) ^ 2 = ∫ t in (0 : ℝ)..M.horizon, 2 * F t * f t := by nlinarith [hprod] _ = 2 * ∫ t in Ioc 0 M.horizon, M.energyIntegral H t ω * (H t ω * (M.atRisk t ω * M.intensity t ω)) ∂volume := by rw [intervalIntegral.integral_of_le M.horizon_pos.le, ← integral_const_mul] apply integral_congr_ae filter_upwards [ae_restrict_mem measurableSet_Ioc] with t ht have ht0 : 0 ≤ t := le_of_lt ht.1 simp only [F, f, Model.energyIntegral, intervalIntegral.integral_of_le ht0] ring

theorem SampleModel.subject_product_pathwise (S : SampleModel n Ω μ) (H : ℝ → (Fin n → Ω) → ℝ) (hH : S.LeftPredictable H) (hbound : ∃ C : ℝ, ∀ t x, |H t x| ≤ C) (i j : Fin n) (x : Fin n → Ω) (hdisjoint : Disjoint ((S.process i).eventTimes x) ((S.process j).eventTimes x)) : S.subjectIntegral H i x * S.subjectIntegral H j x = (S.process i).jumpIntegral (S.crossPayoff H j) (S.process i).horizon x + (S.process j).jumpIntegral (S.crossPayoff H i) (S.process j).horizon x - (S.process i).energyIntegral (S.crossPayoff H j) (S.process i).horizon x - (S.process j).energyIntegral (S.crossPayoff H i) (S.process j).horizon x := by /- Instantiate finiteJump_sum_product on the two event sets, and finiteJump_sum_integral_product in both orientations with the respective H-weighted rates. Use integral_prefix_product for the two continuous parts. Every component horizon is S.horizon by process_horizon. The existing square_pathwise proof gives the local measurability, bounded strict-prefix and continuous-prefix integrability needed to distribute subtraction through the two time integrals. Assemble the identities with finite-sum linearity and ring; no moment premise enters. All three deterministic prerequisites in PathwiseCrossAlgebra are now proved. This is the only open proof in the dependency closure. Work at a fixed x with T := S.horizon, E := (S.process i).eventTimes x, F := (S.process j).eventTimes x, f t := H t x * rate_i t and g t := H t x * rate_j t. Weighted-rate integrability follows exactly as hf in Model.square_pathwise (joint measurability from predictability, dominated by |C| times the integrable absolute rate). Strict jump-prefix functions are measurable finite sums of Ioi indicators and bounded by the finite sum of absolute event payoffs. Continuous prefixes are continuous on Icc 0 T by the interval primitive theorem, hence bounded; their products with either weighted rate are integrable. These facts justify integral_sub when expanding each cross energy payoff. Model.events_in_horizon removes each t ≤ horizon event filter. The mixed sum/integral identities are instantiated twice; the continuous product identity supplies both continuous-prefix terms. Normalize crossPayoff, prefixIntegral, energyIntegral and the common horizons, distribute finite sums and the justified time subtractions, then ring with the four deterministic equalities. Do not add any hypothesis or invoke probabilistic independence in this pathwise proof. -/ classical let T := S.horizon let E (k : Fin n) := (S.process k).eventTimes x let r (k : Fin n) (t : ℝ) := (S.process k).atRisk t x * (S.process k).intensity t x let f (k : Fin n) (t : ℝ) := H t x * r k t let J (k : Fin n) (t : ℝ) := ∑ s ∈ (E k).filter (fun s => s < t), H s x let A (k : Fin n) (t : ℝ) := ∫ s in Ioc 0 t, f k s ∂volume have hT : 0 ≤ T := S.horizon_pos.le have hE (k : Fin n) (t : ℝ) (ht : t ∈ E k) : 0 < t ∧ t ≤ T := by simpa only [S.process_horizon] using (S.process k).events_in_horizon x t ht have hfilter (k : Fin n) : (E k).filter (fun t => t ≤ T) = E k := Finset.filter_eq_self.mpr (fun t ht => (hE k t ht).2) have hHm : Measurable (fun t => H t x) := ((S.process i).predictable_joint_measurable H (S.process_predictable H hH i)).comp (measurable_id.prodMk measurable_const) obtain ⟨C, hC⟩ := hbound have hf (k : Fin n) : IntegrableOn (f k) (Ioc 0 T) volume := by have hrm : Measurable (r k) := ((S.process k).atRisk_joint_measurable.comp (measurable_id.prodMk measurable_const)).mul ((S.process k).intensity_joint_measurable.comp (measurable_id.prodMk measurable_const)) have hr : Integrable (r k) (volume.restrict (Ioc 0 T)) := by simpa only [S.process_horizon, r, T, IntegrableOn] using (S.process k).rate_integrable x apply Integrable.mono' (hr.abs.const_mul |C|) · exact (hHm.mul hrm).aestronglyMeasurable · filter_upwards with t simp only [Real.norm_eq_abs, f, abs_mul] exact mul_le_mul_of_nonneg_right ((hC t x).trans (le_abs_self C)) (abs_nonneg (r k t)) have hJm (k : Fin n) : Measurable (J k) := by dsimp [J] simp_rw [Finset.sum_filter] apply Finset.measurable_sum intro s hs exact Measurable.ite measurableSet_Ioi measurable_const measurable_const have hJbound (k : Fin n) (t : ℝ) : |J k t| ≤ ∑ s ∈ E k, |H s x| := by calc _ ≤ ∑ s ∈ (E k).filter (fun s => s < t), |H s x| := Finset.abs_sum_le_sum_abs _ _ _ ≤ _ := Finset.sum_le_sum_of_subset_of_nonneg (filter_subset _ _) (by intro s hs hns; exact abs_nonneg _) have hJf (k l : Fin n) : IntegrableOn (fun t => J k t * f l t) (Ioc 0 T) volume := by apply (hf l).bdd_mul (c := ∑ s ∈ E k, |H s x|) (hJm k).aestronglyMeasurable filter_upwards with t simpa only [Real.norm_eq_abs] using hJbound k t have hAf (k l : Fin n) : IntegrableOn (fun t => A k t * f l t) (Ioc 0 T) volume := by let B : ℝ → ℝ := fun t => ∫ s in (0 : ℝ)..t, f k s have hki : IntervalIntegrable (f k) volume 0 T := (intervalIntegrable_iff_integrableOn_Ioc_of_le hT).2 (hf k) have hli : IntervalIntegrable (f l) volume 0 T := (intervalIntegrable_iff_integrableOn_Ioc_of_le hT).2 (hf l) have hB : ContinuousOn B (uIcc 0 T) := (hki.absolutelyContinuousOnInterval_intervalIntegral (by simp)).continuousOn have hb := (intervalIntegrable_iff_integrableOn_Ioc_of_le hT).1 (hli.continuousOn_mul hB) apply hb.congr filter_upwards [ae_restrict_mem measurableSet_Ioc] with t ht simp only [B, A, intervalIntegral.integral_of_le ht.1.le] have hcross (k l : Fin n) : (S.process k).energyIntegral (S.crossPayoff H l) (S.process k).horizon x = (∫ t in Ioc 0 T, J l t * f k t ∂volume) - ∫ t in Ioc 0 T, A l t * f k t ∂volume := by unfold Model.energyIntegral SampleModel.crossPayoff Model.prefixIntegral rw [S.process_horizon k] calc _ = ∫ t in Ioc 0 T, (J l t * f k t - A l t * f k t) ∂volume := by apply integral_congr_ae filter_upwards with t dsimp [J, A, f, r, E, Model.energyIntegral] ring _ = _ := integral_sub (hJf l k) (hAf l k) have hj := finiteJump_sum_product (E i) (E j) (fun t => H t x) (fun t => H t x) hdisjoint have hij := finiteJump_sum_integral_product (E i) (fun t => H t x) (f j) T hT (hE i) (hf j) have hji := finiteJump_sum_integral_product (E j) (fun t => H t x) (f i) T hT (hE j) (hf i) have ha := integral_prefix_product (f i) (f j) T hT (hf i) (hf j) rw [hcross i j, hcross j i] unfold SampleModel.subjectIntegral Model.stochasticIntegral Model.jumpIntegral Model.energyIntegral SampleModel.crossPayoff Model.prefixIntegral simp only [S.process_horizon] change ((∑ s ∈ (E i).filter (fun t => t ≤ T), H s x) - A i T) * ((∑ s ∈ (E j).filter (fun t => t ≤ T), H s x) - A j T) = (∑ s ∈ (E i).filter (fun t => t ≤ T), H s x * (J j s - A j s)) + (∑ s ∈ (E j).filter (fun t => t ≤ T), H s x * (J i s - A i s)) - ((∫ t in Ioc 0 T, J j t * f i t ∂volume) - ∫ t in Ioc 0 T, A j t * f i t ∂volume) - ((∫ t in Ioc 0 T, J i t * f j t ∂volume) - ∫ t in Ioc 0 T, A i t * f j t ∂volume) rw [hfilter i, hfilter j] simp only [mul_sub, Finset.sum_sub_distrib] dsimp only [J, A] at ⊢ nlinarith [hj, hij, hji, ha]

theorem Model.tendsto_expected_energyIntegral_of_dominated (M : Model Ω μ) [IsProbabilityMeasure μ] (G : ℕ → ℝ → Ω → ℝ) (H : ℝ → Ω → ℝ) (hG : ∀ k, M.Predictable (G k)) (hH : M.Predictable H) (hdom : ∀ k t ω, |G k t ω| ≤ |H t ω|) (hproduct : Integrable (fun p : ℝ × Ω => |H p.1 p.2| * (M.atRisk p.1 p.2 * M.intensity p.1 p.2)) ((volume.restrict (Ioc 0 M.horizon)).prod μ)) (hlim : ∀ t ω, Tendsto (fun k => G k t ω) atTop (nhds (H t ω))) : Tendsto (fun k => ∫ ω, M.energyIntegral (G k) M.horizon ω ∂μ) atTop (nhds (∫ ω, M.energyIntegral H M.horizon ω ∂μ)) := by /- Apply DCT once on the time-sample product, then rewrite each product integral as the sample expectation of the time integral using `integral_prod_symm`. Nonnegative rates convert norm domination into `hdom`. Use `Integrable.mono'` to derive product integrability of each approximant and of H from hproduct and joint measurability. Alternatively `integrable_prod_iff'` supplies a.e. integrable time sections and the integrable absolute energy envelope for two successive applications of DCT. Do not infer section integrability solely from integrability of a totalized pathwise Bochner integral. -/ let ν := volume.restrict (Ioc 0 M.horizon) let rate : ℝ × Ω → ℝ := fun p => M.atRisk p.1 p.2 * M.intensity p.1 p.2 have hrmeas : Measurable rate := M.atRisk_joint_measurable.mul M.intensity_joint_measurable have hrnonneg (p : ℝ × Ω) : 0 ≤ rate p := mul_nonneg (M.atRisk_nonneg p.1 p.2) (M.intensity_nonneg p.1 p.2) have hmeas (k : ℕ) : Measurable (fun p : ℝ × Ω => G k p.1 p.2 * rate p) := (M.predictable_joint_measurable (G k) (hG k)).mul hrmeas have hbound (k : ℕ) (p : ℝ × Ω) : ‖G k p.1 p.2 * rate p‖ ≤ |H p.1 p.2| * rate p := by rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg (hrnonneg p)] exact mul_le_mul_of_nonneg_right (hdom k p.1 p.2) (hrnonneg p) have hGi (k : ℕ) : Integrable (fun p : ℝ × Ω => G k p.1 p.2 * rate p) (ν.prod μ) := hproduct.mono' (hmeas k).aestronglyMeasurable (Eventually.of_forall (hbound k)) have hHi : Integrable (fun p : ℝ × Ω => H p.1 p.2 * rate p) (ν.prod μ) := by apply hproduct.mono' ((M.predictable_joint_measurable H hH).mul hrmeas).aestronglyMeasurable apply Eventually.of_forall intro p change ‖H p.1 p.2 * rate p‖ ≤ |H p.1 p.2| * rate p rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg (hrnonneg p)] have hconv : Tendsto (fun k => ∫ p, G k p.1 p.2 * rate p ∂(ν.prod μ)) atTop (nhds (∫ p, H p.1 p.2 * rate p ∂(ν.prod μ))) := by apply tendsto_integral_of_dominated_convergence (fun p => |H p.1 p.2| * rate p) · exact fun k => (hmeas k).aestronglyMeasurable · exact hproduct · exact fun k => Eventually.of_forall (hbound k) · exact Eventually.of_forall (fun p => (hlim p.1 p.2).mul tendsto_const_nhds) have hGeq (k : ℕ) : (∫ p, G k p.1 p.2 * rate p ∂(ν.prod μ)) = ∫ ω, M.energyIntegral (G k) M.horizon ω ∂μ := integral_prod_symm _ (hGi k) have hHeq : (∫ p, H p.1 p.2 * rate p ∂(ν.prod μ)) = ∫ ω, M.energyIntegral H M.horizon ω ∂μ := integral_prod_symm _ hHi simpa only [hGeq, hHeq] using hconv

theorem Model.jumpIntegral_square (M : Model Ω μ) (H : ℝ → Ω → ℝ) (ω : Ω) : (M.jumpIntegral H M.horizon ω) ^ 2 = M.jumpIntegral (fun t ω => (H t ω) ^ 2) M.horizon ω + M.jumpIntegral (fun t ω => 2 * H t ω * (∑ s ∈ (M.eventTimes ω).filter (fun s => s < t), H s ω)) M.horizon ω := by /- Order the finite set of event times. Every unordered pair contributes twice, and has exactly one strictly later endpoint. -/ classical have hs (s : Finset ℝ) (f : ℝ → ℝ) : (∑ t ∈ s, f t) ^ 2 = (∑ t ∈ s, (f t) ^ 2) + ∑ t ∈ s, 2 * f t * (∑ u ∈ s.filter (fun u => u < t), f u) := by induction s using Finset.induction_on_max with | empty => simp | @insert a s ha ih => have han : a ∉ s := fun h => (lt_irrefl a) (ha a h) have hlt (t : ℝ) (ht : t ∈ s) : ¬ a < t := (ha t ht).not_gt simp only [Finset.sum_insert han, Finset.filter_insert] simp only [if_neg (lt_irrefl a)] have hfilt : s.filter (fun u => u < a) = s := Finset.filter_true_of_mem (fun u hu => ha u hu) simp only [hfilt] have hsum : (∑ t ∈ s, 2 * f t * ∑ u ∈ (if a < t then insert a (s.filter (fun u => u < t)) else s.filter (fun u => u < t)), f u) = ∑ t ∈ s, 2 * f t * ∑ u ∈ s.filter (fun u => u < t), f u := by apply Finset.sum_congr rfl intro t ht rw [if_neg (hlt t ht)] rw [hsum] nlinarith [ih] have hfin : (M.eventTimes ω).filter (fun t => t ≤ M.horizon) = M.eventTimes ω := Finset.filter_true_of_mem (fun t ht => (M.events_in_horizon ω t ht).2) simpa [Model.jumpIntegral, hfin] using hs (M.eventTimes ω) (fun t => H t ω)

theorem Model.stochasticIntegral_isometry (M : Model Ω μ) (H : ℝ → Ω → ℝ) (hH : M.Predictable H) (hbound : ∃ C : ℝ, ∀ t ω, |H t ω| ≤ C) : (∫ ω, (M.stochasticIntegral H M.horizon ω) ^ 2 ∂μ) = ∫ ω, M.energyIntegral (M.quadraticPayoff H) M.horizon ω ∂μ := by have hjq := M.integrable_quadratic_jump H hH hbound have heq := M.integrable_quadratic_energy H hH hbound have hjp := M.integrable_prefix_jump H hH hbound have hep := M.integrable_prefix_energy H hH hbound have hquad : ∃ C : ℝ, ∀ t ω, |M.quadraticPayoff H t ω| ≤ C := by obtain ⟨C, hC⟩ := hbound refine ⟨C ^ 2, ?_⟩ intro t ω simpa [Model.quadraticPayoff, abs_pow] using (pow_le_pow_left₀ (abs_nonneg (H t ω)) (hC t ω) 2) have hcq := M.bounded_predictable_compensator (M.quadraticPayoff H) (M.predictable_quadratic H hH) hquad have hcp := M.predictable_compensator (M.prefixPayoff H) (M.predictable_prefix_payoff H hH) (M.integrable_prefix_jump_abs H hH hbound) calc (∫ ω, (M.stochasticIntegral H M.horizon ω) ^ 2 ∂μ) = ∫ ω, M.jumpIntegral (M.quadraticPayoff H) M.horizon ω + M.jumpIntegral (M.prefixPayoff H) M.horizon ω - M.energyIntegral (M.prefixPayoff H) M.horizon ω ∂μ := integral_congr_ae (Filter.Eventually.of_forall (M.square_pathwise H hH hbound)) _ = (∫ ω, M.jumpIntegral (M.quadraticPayoff H) M.horizon ω ∂μ) + (∫ ω, M.jumpIntegral (M.prefixPayoff H) M.horizon ω ∂μ) - (∫ ω, M.energyIntegral (M.prefixPayoff H) M.horizon ω ∂μ) := by change (∫ ω, (M.jumpIntegral (M.quadraticPayoff H) M.horizon + M.jumpIntegral (M.prefixPayoff H) M.horizon - M.energyIntegral (M.prefixPayoff H) M.horizon) ω ∂μ) = _ rw [integral_sub' (hjq.add hjp) hep, integral_add' hjq hjp] _ = ∫ ω, M.energyIntegral (M.quadraticPayoff H) M.horizon ω ∂μ := by rw [hcq, hcp] ring

theorem SampleModel.no_common_jumps {n : ℕ} (S : SampleModel n Ω μ) [IsProbabilityMeasure μ] (i j : Fin n) (hij : i ≠ j) : ∀ᵐ x ∂finiteSampleLaw n μ, Disjoint ((S.process i).eventTimes x) ((S.process j).eventTimes x) := by /- Apply independent_time_avoids_events to each i jumpTime and process j. The maps (eventCard, jumpTime k) depend only on their subject coordinate: process_events identifies their event sets, and jumpTime is defined from the filtered counts. For a measurable coordinate factorization, compose these already-measurable maps with a constant sample updated at i or j (the probability law supplies Nonempty Ω). Use iIndepFun_pi and IndepFun.comp for the two coordinate maps. Intersect over k, then use the finite enumeration to obtain disjointness. No independence of H is required. -/ classical let ω₀ : Ω := choice (nonempty_of_isProbabilityMeasure μ) let lift : Fin n → Ω → (Fin n → Ω) := fun a ω => update (fun _ => ω₀) a ω have hlift (a : Fin n) : Measurable (lift a) := by apply measurable_pi_lambda intro b by_cases hab : b = a · subst b intro A hA simpa [lift] using hA · simp [lift, Function.update_of_ne hab] have hevents (a : Fin n) (x : Fin n → Ω) : (S.process a).eventTimes (lift a (x a)) = (S.process a).eventTimes x := by simp [S.process_events, lift] have hjump (a : Fin n) (k : ℕ) (x : Fin n → Ω) : (S.process a).jumpTime k (lift a (x a)) = (S.process a).jumpTime k x := by unfold Model.jumpTime Model.count rw [hevents] have hcoords : iIndepFun (fun a : Fin n => fun x : Fin n → Ω => x a) (finiteSampleLaw n μ) := ProbabilityTheory.iIndepFun_pi (X := fun _ => id) (fun _ => aemeasurable_id) have havoid (k : ℕ) : ∀ᵐ x ∂finiteSampleLaw n μ, (S.process i).jumpTime k x ∉ (S.process j).eventTimes x := by apply (S.process j).independent_time_avoids_events ((S.process i).jumpTime k) ((S.process i).measurable_jumpTime k) intro l have h := (hcoords.indepFun hij).comp (((S.process i).measurable_jumpTime k).comp (hlift i)) ((((S.process j).measurable_eventCard).prodMk ((S.process j).measurable_jumpTime l)).comp (hlift j)) simpa only [Function.comp_def, hevents, hjump] using h filter_upwards [ae_all_iff.mpr havoid] with x hx apply Finset.disjoint_left.mpr intro t hi hj rw [← (S.process i).eventTimes_eq_image x] at hi obtain ⟨k, hk, heq⟩ := Finset.mem_image.mp hi exact hx k (heq.symm ▸ hj)

theorem integral_prefix_product (f g : ℝ → ℝ) (T : ℝ) (hT : 0 ≤ T) (hf : IntegrableOn f (Ioc 0 T) volume) (hg : IntegrableOn g (Ioc 0 T) volume) : (∫ t in Ioc 0 T, f t ∂volume) * (∫ t in Ioc 0 T, g t ∂volume) = (∫ t in Ioc 0 T, (∫ s in Ioc 0 t, f s ∂volume) * g t ∂volume) + (∫ t in Ioc 0 T, (∫ s in Ioc 0 t, g s ∂volume) * f t ∂volume) := by let F : ℝ → ℝ := fun t => ∫ s in (0 : ℝ)..t, f s let G : ℝ → ℝ := fun t => ∫ s in (0 : ℝ)..t, g s have hfi : IntervalIntegrable f volume 0 T := (intervalIntegrable_iff_integrableOn_Ioc_of_le hT).2 hf have hgi : IntervalIntegrable g volume 0 T := (intervalIntegrable_iff_integrableOn_Ioc_of_le hT).2 hg have hF : AbsolutelyContinuousOnInterval F 0 T := hfi.absolutelyContinuousOnInterval_intervalIntegral (by simp) have hG : AbsolutelyContinuousOnInterval G 0 T := hgi.absolutelyContinuousOnInterval_intervalIntegral (by simp) have hprod := hF.integral_deriv_mul_eq_sub hG have heq : (∫ t in (0 : ℝ)..T, deriv F t * G t + F t * deriv G t) = ∫ t in (0 : ℝ)..T, (∫ s in Ioc 0 t, f s ∂volume) * g t + (∫ s in Ioc 0 t, g s ∂volume) * f t := by apply intervalIntegral.integral_congr_ae filter_upwards [hfi.ae_hasDerivAt_integral, hgi.ae_hasDerivAt_integral] with t hft hgt htm have htIcc : t ∈ Icc (0 : ℝ) T := by simpa [uIcc_of_le hT] using (uIoc_subset_uIcc htm) have hdF : deriv F t = f t := (hft (by simpa [uIcc_of_le hT] using htIcc) 0 (by simp)).deriv have hdG : deriv G t = g t := (hgt (by simpa [uIcc_of_le hT] using htIcc) 0 (by simp)).deriv rw [hdF, hdG] simp only [F, G, intervalIntegral.integral_of_le htIcc.1] ring have hfg : IntegrableOn (fun t => (∫ s in Ioc 0 t, f s ∂volume) * g t) (Ioc 0 T) volume := by have h : IntegrableOn (fun t => F t * g t) (Ioc 0 T) volume := (intervalIntegrable_iff_integrableOn_Ioc_of_le hT).1 (hgi.continuousOn_mul (by simpa [uIcc_of_le hT] using hF.continuousOn)) apply h.congr filter_upwards [ae_restrict_mem measurableSet_Ioc] with t ht simp only [F, intervalIntegral.integral_of_le ht.1.le] have hgf : IntegrableOn (fun t => (∫ s in Ioc 0 t, g s ∂volume) * f t) (Ioc 0 T) volume := by have h : IntegrableOn (fun t => G t * f t) (Ioc 0 T) volume := (intervalIntegrable_iff_integrableOn_Ioc_of_le hT).1 (hfi.continuousOn_mul (by simpa [uIcc_of_le hT] using hG.continuousOn)) apply h.congr filter_upwards [ae_restrict_mem measurableSet_Ioc] with t ht simp only [G, intervalIntegral.integral_of_le ht.1.le] rw [heq, intervalIntegral.integral_of_le hT, integral_add hfg hgf] at hprod simpa only [F, G, intervalIntegral.integral_of_le hT, intervalIntegral.integral_same, zero_mul, sub_zero] using hprod.symm

theorem Model.bounded_predictable_approximation (M : Model Ω μ) (H : ℝ → Ω → ℝ) (hH : M.Predictable H) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ t ω, |H t ω| ≤ C) : ∃ G : ℕ → ℝ → Ω → ℝ, (∀ n, M.Predictable (G n)) ∧ (∀ n, Finite (range (fun p : ℝ × Ω => G n p.1 p.2))) ∧ (∀ n t ω, |G n t ω| ≤ C) ∧ (∀ t ω, Tendsto (fun n => G n t ω) atTop (nhds (H t ω))) := by letI : MeasurableSpace (ℝ × Ω) := predictableSpace M.filtration have hsm : StronglyMeasurable[predictableSpace M.filtration] (fun p : ℝ × Ω => H p.1 p.2) := hH.stronglyMeasurable refine ⟨fun n t ω => hsm.approxBounded C n (t, ω), ?_, ?_, ?_, ?_⟩ · intro n exact (hsm.approxBounded C n).measurable · intro n exact (hsm.approxBounded C n).finite_range · intro n t ω simpa only [Real.norm_eq_abs] using hsm.norm_approxBounded_le hC n (t, ω) · intro t ω apply hsm.tendsto_approxBounded_of_norm_le simpa only [Real.norm_eq_abs] using hbound t ω

theorem Model.predictable_cylinder_compensator (M : Model Ω μ) [IsProbabilityMeasure μ] (a b : ℝ) (B : Set Ω) (hB : MeasurableSet[M.filtration a] B) (hjump : Integrable (M.jumpIntegral (fun t ω => (Ioc a b ×ˢ B).indicator (fun _ => (1 : ℝ)) (t, ω)) M.horizon) μ) (henergy : Integrable (M.energyIntegral (fun t ω => (Ioc a b ×ˢ B).indicator (fun _ => (1 : ℝ)) (t, ω)) M.horizon) μ) : (∫ ω, M.jumpIntegral (fun t ω => (Ioc a b ×ˢ B).indicator (fun _ => (1 : ℝ)) (t, ω)) M.horizon ω ∂μ) = ∫ ω, M.energyIntegral (fun t ω => (Ioc a b ×ˢ B).indicator (fun _ => (1 : ℝ)) (t, ω)) M.horizon ω ∂μ := by let u : ℝ := max 0 a let v : ℝ := min M.horizon b let F : Ω → ℝ := B.indicator (fun _ => 1) have htime (t : ℝ) (ht : 0 < t ∧ t ≤ M.horizon) : (a < t ∧ t ≤ b) ↔ (u < t ∧ t ≤ v) := by simp only [u, v, max_lt_iff, le_min_iff] exact ⟨fun h => ⟨⟨ht.1, h.1⟩, ⟨ht.2, h.2⟩⟩, fun h => ⟨h.1.2, h.2.2⟩⟩ have hJump (ω : Ω) : M.jumpIntegral (fun t ω => (Ioc a b ×ˢ B).indicator (fun _ => (1 : ℝ)) (t, ω)) M.horizon ω = F ω * (((M.eventTimes ω).filter (fun t => u < t ∧ t ≤ v)).card : ℝ) := by classical have hfilter : (M.eventTimes ω).filter (fun t => t ≤ M.horizon) = M.eventTimes ω := Finset.filter_eq_self.mpr (fun t ht => (M.events_in_horizon ω t ht).2) have heq (t : ℝ) (ht : t ∈ M.eventTimes ω) : (Ioc a b ×ˢ B).indicator (fun _ => (1 : ℝ)) (t, ω) = if u < t ∧ t ≤ v then F ω else 0 := by by_cases hb : ω ∈ B · simp [F, Set.indicator_apply, mem_prod, mem_Ioc, hb, htime t (M.events_in_horizon ω t ht)] · simp [F, mem_prod, hb] simp only [Model.jumpIntegral, hfilter] rw [Finset.sum_congr rfl heq] simp [Finset.sum_ite, Finset.sum_const, mul_comm] have hEnergy (ω : Ω) : M.energyIntegral (fun t ω => (Ioc a b ×ˢ B).indicator (fun _ => (1 : ℝ)) (t, ω)) M.horizon ω = F ω * (∫ t in Ioc u v, M.atRisk t ω * M.intensity t ω ∂volume) := by have heq : (fun t : ℝ => (Ioc a b ×ˢ B).indicator (fun _ => (1 : ℝ)) (t, ω) * (M.atRisk t ω * M.intensity t ω)) = (Ioc a b).indicator (fun t => F ω * (M.atRisk t ω * M.intensity t ω)) := by funext t by_cases hb : ω ∈ B · by_cases ht : t ∈ Ioc a b <;> simp [F, mem_prod, hb, ht] · simp [F, Set.indicator_apply, mem_prod, hb] change (∫ t in Ioc 0 M.horizon, (Ioc a b ×ˢ B).indicator (fun _ => (1 : ℝ)) (t, ω) * (M.atRisk t ω * M.intensity t ω) ∂volume) = _ rw [heq, setIntegral_indicator measurableSet_Ioc, Ioc_inter_Ioc, integral_const_mul] by_cases huv : u ≤ v · have hu0 : 0 ≤ u := le_max_left 0 a have hvT : v ≤ M.horizon := min_le_left _ _ have hFu : Measurable[M.filtration u] F := by have haU : a ≤ u := le_max_right 0 a exact (measurable_const.indicator ((M.filtration_mono haU) B hB)) have hbounded : ∃ C : ℝ, ∀ ω, |F ω| ≤ C := by refine ⟨1, ?_⟩ intro ω by_cases hb : ω ∈ B <;> simp [F, hb] have hc : Integrable (fun ω => F ω * (((M.eventTimes ω).filter (fun t => u < t ∧ t ≤ v)).card : ℝ)) μ := by simpa only [← hJump] using hjump have hr : Integrable (fun ω => F ω * ∫ t in Ioc u v, M.atRisk t ω * M.intensity t ω ∂volume) μ := by simpa only [← hEnergy] using henergy simpa only [hJump, hEnergy] using M.conditional_intensity_increment u v F hu0 huv hvT hFu hbounded hc hr · have hzero : Ioc u v = (∅ : Set ℝ) := Ioc_eq_empty_iff.mpr (not_lt_of_ge (le_of_not_ge huv)) have hcard (ω : Ω) : (M.eventTimes ω).filter (fun t => u < t ∧ t ≤ v) = ∅ := by apply Finset.filter_false_of_mem intro t _ ht exact huv (le_trans (le_of_lt ht.1) ht.2) simp [hJump, hEnergy, hzero, hcard]

theorem Model.abs_stochasticIntegral_le (M : Model Ω μ) (H : ℝ → Ω → ℝ) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hH : ∀ t ω, |H t ω| ≤ C) (hr : ∀ t ω, 0 ≤ t → t ≤ M.horizon → M.atRisk t ω * M.intensity t ω ≤ R) (ω : Ω) : |M.stochasticIntegral H M.horizon ω| ≤ C * ((M.eventTimes ω).card : ℝ) + C * (R * M.horizon) := by have hab : |M.stochasticIntegral H M.horizon ω| ≤ |M.jumpIntegral H M.horizon ω| + |M.energyIntegral H M.horizon ω| := by simpa [Model.stochasticIntegral] using (abs_sub_le (M.jumpIntegral H M.horizon ω) 0 (M.energyIntegral H M.horizon ω)) exact hab.trans (add_le_add (M.abs_jumpIntegral_le_card H C hH ω) (M.abs_energyIntegral_le_horizon H C R hC hR hH hr M.horizon ⟨M.horizon_pos.le, le_rfl⟩ ω))