Jump-diffusion coefficient bundles and hypotheses

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_Multidim
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_MultidimIto
import Definitions.Def_KLSModular_LevyStochCalc_Poisson_L2Isometry

/-
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/Ito/Setting.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 Ito
namespace Setting
universe u v
section Coefficients
variable {Ω : Type u} [MeasurableSpace Ω]
variable {E : Type v} [MeasurableSpace E]
/-- Coefficient bundle for a jump diffusion: drift `μ`, diffusion `σ`, jump
size `γ`. Lipschitz / measurability hypotheses live on the headline theorem. -/
structure JumpDiffusionCoeffs (n d : ℕ) (E : Type v) where
  μ : ℝ → (Fin n → ℝ) → (Fin n → ℝ)
  σ : ℝ → (Fin n → ℝ) → (Fin n → Fin d → ℝ)
  γ : ℝ → (Fin n → ℝ) → E → (Fin n → ℝ)
/-- Joint Lipschitz hypothesis on the jump-diffusion coefficients
`(μ, σ, γ)`. Required for `JumpDiffusion.exists_unique` (Applebaum 2009
Thm 6.2.9 — without this, Tanaka's example shows uniqueness can fail,
e.g. `dX_t = |X_t|^α dW_t` for `α < 1/2` has infinitely many strong
solutions; cf. Karatzas-Shreve 5.3.2). -/
def JumpDiffusionCoeffs.IsLipschitz {n d : ℕ}
    (coeffs : JumpDiffusionCoeffs n d E) (ν : Measure E) (L : ℝ) : Prop :=
  0 ≤ L ∧
  -- μ uniformly Lipschitz in x:
  (∀ s : ℝ, ∀ x₁ x₂ : Fin n → ℝ,
    ‖coeffs.μ s x₁ - coeffs.μ s x₂‖ ≤ L * ‖x₁ - x₂‖) ∧
  -- σ uniformly Lipschitz in x (with the Frobenius / Euclidean norm on matrices):
  (∀ s : ℝ, ∀ x₁ x₂ : Fin n → ℝ,
    (∑ i, ∑ j, (coeffs.σ s x₁ i j - coeffs.σ s x₂ i j) ^ 2)
      ≤ L ^ 2 * ‖x₁ - x₂‖ ^ 2) ∧
  -- γ uniformly Lipschitz in x (L²-in-e sense):
  (∀ s : ℝ, ∀ x₁ x₂ : Fin n → ℝ,
    ∫⁻ e, (‖coeffs.γ s x₁ e - coeffs.γ s x₂ e‖₊ : ℝ≥0∞) ^ 2 ∂ν
      ≤ ENNReal.ofReal (L ^ 2 * ‖x₁ - x₂‖ ^ 2))
/-- Regularity of the jump-diffusion coefficients in the time and mark variables: joint
measurability, and square integrability in `s` at a single state.

`JumpDiffusionCoeffs.IsLipschitz` constrains `(μ, σ, γ)` only in the state variable, while the
`is_solution` field of `JumpDiffusion` needs joint measurability, progressive measurability and
`L²` bounds of the integrands along the path. Together with the Lipschitz clauses, the bounds
below give those `L²` bounds along any `L²`-bounded path, since Lipschitz continuity in the
state gives `‖f s x‖ ≤ ‖f s 0‖ + L ‖x‖`. -/
def JumpDiffusionCoeffs.IsRegular {n d : ℕ}
    (coeffs : JumpDiffusionCoeffs n d E) (ν : Measure E) : Prop :=
  Measurable (Function.uncurry coeffs.μ) ∧
  Measurable (Function.uncurry coeffs.σ) ∧
  Measurable (fun p : ℝ × (Fin n → ℝ) × E => coeffs.γ p.1 p.2.1 p.2.2) ∧
  (∀ T : ℝ, 0 < T →
    ∫⁻ s in Set.Icc (0 : ℝ) T, (‖coeffs.μ s 0‖₊ : ℝ≥0∞) ^ 2 ∂volume < ⊤) ∧
  (∀ T : ℝ, 0 < T →
    ∫⁻ s in Set.Icc (0 : ℝ) T, ∑ i, ∑ j,
      (‖coeffs.σ s 0 i j‖₊ : ℝ≥0∞) ^ 2 ∂volume < ⊤) ∧
  (∀ T : ℝ, 0 < T →
    ∫⁻ s in Set.Icc (0 : ℝ) T, ∫⁻ e,
      (‖coeffs.γ s 0 e‖₊ : ℝ≥0∞) ^ 2 ∂ν ∂volume < ⊤)
end Coefficients
end Setting
end Ito
end LevyStochCalc