Restricted stopped-future finite-coordinate law on compact nonnegative tests

import Mathlib.MeasureTheory.Integral.Lebesgue.Map
import Mathlib.Topology.Instances.ENNReal.Lemmas
import Mathlib.Topology.ContinuousMap.CompactlySupported
import Theorems.Thm_AvramDividend_Classical_levy_finiteStopping_cylinderReward_scalar_markov_no_meas_premise
import Theorems.Thm_AvramDividend_Classical_levy_finiteStopping_stoppedFuturePath_measurable
import Theorems.Thm_AvramDividend_Classical_stoppedHistory_event_measurable
import Theorems.Thm_AvramDividend_Classical_compactTest_nnreal_uniformBound_finiteLintegral

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

theorem AvramDividend.Classical.levy_finiteStopping_restrictedFDD_compactTest_lintegral
    {Ω : 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}))
    (hP : P Set.univ ≠ ⊤)
    (J : Finset ℝ≥0)
    (f : CompactlySupportedContinuousMap (J → ℝ) ℝ≥0) :
    (∫⁻ z, ((f z : ℝ≥0) : ℝ≥0∞) ∂(Measure.map
      (fun ω : Ω => fun j : J =>
        X.X (τ ω + (j : ℝ≥0)) ω - X.X (τ ω) ω) (P.restrict A))) =
    P A * (∫⁻ y, ((f (fun j : J => y (j : ℝ≥0)) : ℝ≥0) : ℝ≥0∞)
      ∂(Measure.map (fun ω : Ω => fun t : ℝ≥0 => X.X t ω) P)) := by
  sorry