Finite-stopping strong Markov factorisation for continuous finite-dimensional rewards

import Mathlib.Probability.Process.Stopping
import Mathlib.Topology.Constructions
import Mathlib.MeasureTheory.Constructions.Pi
import Definitions.Def_AvramDividend_Classical_SpectrallyNegativeLevy
import Theorems.Thm_AvramDividend_Classical_levy_finiteStopping_boundedReward_scalar_markov

open MeasureTheory ProbabilityTheory Filter Set
open scoped NNReal ENNReal
open AvramDividend.Classical

theorem AvramDividend.Classical.levy_finiteStopping_continuousCylinderReward_scalar_markov
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (τ : Ω → ℝ≥0)
    (hstop : IsStoppingTime 𝓕 (fun ω => (τ ω : WithTop ℝ≥0)))
    (A : Set Ω)
    (hA : ∀ s : ℝ≥0,
      MeasurableSet[𝓕 s] (A ∩ {ω : Ω | τ ω ≤ s}))
    (J : Finset ℝ≥0)
    (h : (J → ℝ) → ℝ≥0∞)
    (hh : Continuous h) (hhm : Measurable h)
    (C : ℝ≥0∞) (hbound : ∀ z, h z ≤ C)
    (hfin : (∫⁻ _ : Ω, C ∂P) ≠ ∞)
    (hMeas : ∀ n : ℕ, Measurable (Set.indicator
      (A ∩ {ω' : Ω | τ ω' ≤ (n : ℝ≥0)})
      (fun ω' : Ω => h (fun j : J =>
        X.X (τ ω' + (j : ℝ≥0)) ω' - X.X (τ ω') ω')))) :
    (∫⁻ ω, Set.indicator A
      (fun ω' : Ω => h (fun j : J =>
        X.X (τ ω' + (j : ℝ≥0)) ω' - X.X (τ ω') ω')) ω ∂P) =
      P A * (∫⁻ y, h (fun j : J => y (j : ℝ≥0))
        ∂(Measure.map
          (fun ω : Ω => fun t : ℝ≥0 => X.X t ω) P)) := by
  sorry