Coefficient truncation for simple predictable integrands

Definition

KLSModular_LevyStochCalc_Brownian_ItoFourthMomentLintegral

by Lazyfill · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-contextvendored-levystochcalc

Vendored from the LevyStochCalc library at https://github.com/cgarryZA/LevyStochCalc, commit 984dbf0b790031eac05d56fe5a84b65e15e1e932. SimplePredictable.truncate G C preserves the partition and replaces every coefficient of the simple predictable integrand $G$ by $\max(-C,\min(C,G))$ , so the coefficients lie in $[-|C|,|C|]$ and remain measurable.

Original module imports

import LevyStochCalc.Brownian.ItoFourthMomentPartialSums

Original declaration excerpt

Shown in the original module context. Body omitted.

noncomputable def SimplePredictable.truncate {T : ℝ} (G : SimplePredictable Ω T) (C : ℝ) :
    SimplePredictable Ω T

Module navigation

Direct project imports: LevyStochCalc/Brownian/ItoFourthMomentPartialSums.

Theorems in source order:

Project result: The KLS conjecture.

Original module · LevyStochCalc.Brownian.ItoFourthMomentLintegral · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoFourthMomentPartialSums

/-
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/Brownian/ItoFourthMomentLintegral.lean; Apache-2.0; 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 coefficients of a simple integrand clamped to `[-C, C]`. -/
noncomputable def SimplePredictable.truncate {T : ℝ} (G : SimplePredictable Ω T) (C : ℝ) :
    SimplePredictable Ω T where
  N := G.N
  partition := G.partition
  partition_zero := G.partition_zero
  partition_le_T := G.partition_le_T
  partition_strictMono := G.partition_strictMono
  ξ := fun i ω => max (-C) (min C (G.ξ i ω))
  ξ_bounded := fun i => ⟨|C|, fun ω => abs_le.mpr
    ⟨le_max_of_le_left (neg_le_neg (le_abs_self C)),
      max_le (neg_le_abs C) ((min_le_left C (G.ξ i ω)).trans (le_abs_self C))⟩⟩
  ξ_measurable := fun i =>
    measurable_const.max (measurable_const.min (G.ξ_measurable i))
end Ito
end Brownian
end LevyStochCalc

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Brownian/ItoFourthMomentLintegral.lean#L57-L70 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Brownian.ItoFourthMomentLintegral`, definition bundle `KLSModular_LevyStochCalc_Brownian_ItoFourthMomentLintegral`; the repository is private at upload time). Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (Apache-2.0; upstream copyright notice retained in the Lean text).

View graph