One-cell and two-cell simple integrands

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoAlgebra
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_CrossOrthogonality

/-
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/CrossVariation.lean; Apache-2.0; locally patched, see formalization/vendor/port.patch; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal
namespace LevyStochCalc
namespace Brownian
namespace Ito
universe u
variable {Ω : Type u} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
  {ℱ : Filtration ℝ ‹MeasurableSpace Ω›}
section TwoCell
/-- The simple integrand carrying a coefficient on one cell `(a, b]` and nothing before it. -/
noncomputable def twoCell {a b : ℝ} (ha : 0 < a) (hab : a < b) (Z : Ω → ℝ)
    (hZm : Measurable Z) {M : ℝ} (hZb : ∀ ω, |Z ω| ≤ M) : SimplePredictable Ω b where
  N := 2
  partition := ![0, a, b]
  partition_zero := rfl
  partition_le_T := le_rfl
  partition_strictMono := by
    refine Fin.strictMono_iff_lt_succ.mpr fun i => ?_
    fin_cases i
    · simpa using ha
    · simpa using hab
  ξ := ![fun _ => 0, Z]
  ξ_bounded := by
    intro i
    fin_cases i
    · exact ⟨0, fun ω => by simp⟩
    · exact ⟨M, hZb⟩
  ξ_measurable := by
    intro i
    fin_cases i
    · simp
    · simpa using hZm
theorem twoCell_adapted {a b : ℝ} (ha : 0 < a) (hab : a < b) {Z : Ω → ℝ} (hZm : Measurable Z)
    {M : ℝ} (hZb : ∀ ω, |Z ω| ≤ M) (hZa : StronglyMeasurable[ℱ a] Z) :
    ∀ i : Fin (twoCell ha hab Z hZm hZb).N,
      StronglyMeasurable[ℱ ((twoCell ha hab Z hZm hZb).partition i.castSucc)]
        ((twoCell ha hab Z hZm hZb).ξ i) := by
  intro i
  fin_cases i
  · change StronglyMeasurable[ℱ 0] fun _ : Ω => (0 : ℝ)
    exact stronglyMeasurable_const
  · change StronglyMeasurable[ℱ a] Z
    exact hZa
/-- The simple integrand carrying a coefficient on the single cell `(0, b]`. -/
noncomputable def oneCell {b : ℝ} (hb : 0 < b) (Z : Ω → ℝ)
    (hZm : Measurable Z) {M : ℝ} (hZb : ∀ ω, |Z ω| ≤ M) : SimplePredictable Ω b where
  N := 1
  partition := ![0, b]
  partition_zero := rfl
  partition_le_T := le_rfl
  partition_strictMono := by
    refine Fin.strictMono_iff_lt_succ.mpr fun i => ?_
    fin_cases i
    simpa using hb
  ξ := ![Z]
  ξ_bounded := by
    intro i
    fin_cases i
    exact ⟨M, hZb⟩
  ξ_measurable := by
    intro i
    fin_cases i
    simpa using hZm
theorem oneCell_adapted {b : ℝ} (hb : 0 < b) {Z : Ω → ℝ} (hZm : Measurable Z)
    {M : ℝ} (hZb : ∀ ω, |Z ω| ≤ M) (hZ0 : StronglyMeasurable[ℱ 0] Z) :
    ∀ i : Fin (oneCell hb Z hZm hZb).N,
      StronglyMeasurable[ℱ ((oneCell hb Z hZm hZb).partition i.castSucc)]
        ((oneCell hb Z hZm hZb).ξ i) := by
  intro i
  fin_cases i
  change StronglyMeasurable[ℱ 0] Z
  exact hZ0
end TwoCell
end Ito
end Brownian
end LevyStochCalc