Independence and integrability of compensated Poisson boxes

import Definitions.Def_KLSModular_LevyStochCalc_Poisson_CompensatedMartingaleAdapted

/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Poisson/CompensatedMartingaleIncrement.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory
open scoped NNReal ENNReal
namespace LevyStochCalc
namespace Poisson
namespace Compensated
universe u v
variable {Ω : Type u} [MeasurableSpace Ω]
variable {E : Type v} [MeasurableSpace E]
/-- **Past-independence of a future box increment.** For a box `B = Ioc a b ×ˢ A`
(`0 ≤ a`, `A` measurable with finite `ν`-mass) and any `f` measurable w.r.t. the
"past at `a`" σ-algebra, `f` and `Ñ(B)` are independent. Repackages
`joint_past_future_independent` at the level of `IndepFun`. -/
lemma indepFun_past_compensated_box
    {P : Measure Ω} [IsProbabilityMeasure P]
    {ν : Measure E} [SigmaFinite ν]
    (N : LevyStochCalc.Poisson.PoissonRandomMeasure P ν)
    (ℱ : Filtration ℝ ‹MeasurableSpace Ω›) (hℱ : IsPoissonFiltration N ℱ)
    {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) {A : Set E} (hA : MeasurableSet A) (hAf : ν A ≠ ⊤)
    {f : Ω → ℝ}
    (hf : @MeasureTheory.StronglyMeasurable Ω ℝ _
      (ℱ a) f) :
    ProbabilityTheory.IndepFun f (fun ω => N.compensated (Set.Ioc a b ×ˢ A) ω) P := by
  have h_box_meas : MeasurableSet (Set.Ioc a b ×ˢ A) := measurableSet_Ioc.prod hA
  have hf_comap_le : MeasurableSpace.comap f inferInstance ≤ ℱ a :=
    hf.measurable.comap_le
  have hÑ_comap_le :
      MeasurableSpace.comap (fun ω => N.compensated (Set.Ioc a b ×ˢ A) ω) inferInstance ≤
        MeasurableSpace.comap (fun ω => N.N ω (Set.Ioc a b ×ˢ A)) inferInstance := by
    intro u hu
    obtain ⟨v, hv, rfl⟩ := hu
    refine ⟨(fun x : ℝ≥0∞ => x.toReal -
      (LevyStochCalc.Poisson.referenceIntensity ν (Set.Ioc a b ×ˢ A)).toReal) ⁻¹' v, ?_, ?_⟩
    · exact (ENNReal.measurable_toReal.sub_const _) hv
    · ext ω; rfl
  rw [ProbabilityTheory.IndepFun_iff]
  intro u v hu hv
  have h_indep := hℱ.indep ha hab hA hAf
  rw [ProbabilityTheory.Indep_iff] at h_indep
  exact h_indep u v (hf_comap_le u hu) (hÑ_comap_le v hv)
/-- Cross-integrability of two compensated masses: `Ñ(B)·Ñ(C)` is `P`-integrable
when both `B`, `C` have finite intensity (each `Ñ ∈ L²`, dominated by
`½(Ñ(B)² + Ñ(C)²)`). -/
lemma compensated_cross_integrable
    {P : Measure Ω} [IsProbabilityMeasure P]
    {ν : Measure E} [SigmaFinite ν]
    (N : LevyStochCalc.Poisson.PoissonRandomMeasure P ν)
    {B C : Set (ℝ × E)} (hB : MeasurableSet B) (hC : MeasurableSet C)
    (hBf : LevyStochCalc.Poisson.referenceIntensity ν B ≠ ⊤)
    (hCf : LevyStochCalc.Poisson.referenceIntensity ν C ≠ ⊤) :
    MeasureTheory.Integrable (fun ω => N.compensated B ω * N.compensated C ω) P := by
  have hBsq := compensated_sq_integrable N hB hBf
  have hCsq := compensated_sq_integrable N hC hCf
  have hmeas : Measurable (fun ω => N.compensated B ω * N.compensated C ω) := by
    unfold LevyStochCalc.Poisson.PoissonRandomMeasure.compensated
    exact ((ENNReal.measurable_toReal.comp (N.measurable_eval hB)).sub_const _).mul
      ((ENNReal.measurable_toReal.comp (N.measurable_eval hC)).sub_const _)
  refine MeasureTheory.Integrable.mono'
    (hBsq.add hCsq) hmeas.aestronglyMeasurable ?_
  filter_upwards with ω
  change ‖N.compensated B ω * N.compensated C ω‖ ≤ (N.compensated B ω)^2 + (N.compensated C ω)^2
  rw [Real.norm_eq_abs]
  rcases abs_cases (N.compensated B ω * N.compensated C ω) with ⟨he, _⟩ | ⟨he, _⟩ <;> rw [he] <;>
    nlinarith [two_mul_le_add_sq (N.compensated B ω) (N.compensated C ω),
      two_mul_le_add_sq (N.compensated B ω) (-N.compensated C ω),
      sq_nonneg (N.compensated B ω), sq_nonneg (N.compensated C ω)]
end Compensated
end Poisson
end LevyStochCalc