Past-weighted interval-step integrands

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoIncrement

/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Modified 2026-10-12 by the KLS formalization project: ported to Lean v4.33.0 and
-- Mathlib db584cd. The changes are listed in vendor/README.md and vendor/port.patch.
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Brownian/ItoPullOut.lean; Apache-2.0; locally patched, see formalization/vendor/port.patch; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
namespace LevyStochCalc
namespace Brownian
namespace Ito
open MeasureTheory ProbabilityTheory
open scoped NNReal ENNReal
universe u
variable {Ω : Type u} [MeasurableSpace Ω]
/-- The simple integrand `V · 1_{(a, b]}`, for `0 < a < b` and a bounded measurable `V`. -/
noncomputable def stepIocMul (Ω) [MeasurableSpace Ω] {a b : ℝ} (ha : 0 < a) (hab : a < b)
    (V : Ω → ℝ) (hVb : ∃ M : ℝ, ∀ ω, |V ω| ≤ M) (hVm : Measurable V) :
    SimplePredictable Ω b where
  N := 2
  partition := ![0, a, b]
  partition_zero := by simp
  partition_le_T := by simp
  partition_strictMono := by
    refine Fin.strictMono_iff_lt_succ.mpr fun i => ?_
    fin_cases i
    · simpa using ha
    · simpa using hab
  ξ := ![fun _ => 0, V]
  ξ_bounded := by
    intro i
    fin_cases i
    · exact ⟨0, fun ω => by norm_num⟩
    · exact hVb
  ξ_measurable := by
    intro i
    fin_cases i
    · exact measurable_const
    · exact hVm
/-- The simple integrand `V · 1_{(0, b]}`, for `0 < b` and a bounded measurable `V`. -/
noncomputable def stepIocMul₀ (Ω) [MeasurableSpace Ω] {b : ℝ} (hb : 0 < b)
    (V : Ω → ℝ) (hVb : ∃ M : ℝ, ∀ ω, |V ω| ≤ M) (hVm : Measurable V) :
    SimplePredictable Ω b where
  N := 1
  partition := ![0, b]
  partition_zero := by simp
  partition_le_T := by simp
  partition_strictMono := by
    refine Fin.strictMono_iff_lt_succ.mpr fun i => ?_
    fin_cases i
    simpa using hb
  ξ := ![V]
  ξ_bounded := by intro i; fin_cases i; exact hVb
  ξ_measurable := by intro i; fin_cases i; exact hVm
end Ito
end Brownian
end LevyStochCalc