Generalized interval-step integrand

Definition

KLSModular_LevyStochCalc_Brownian_ItoIncrementMomentRestrict

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. For $0\le a<b$ , stepIocGen Ω ha hab is the simple predictable integrand representing $1_{(a,b]}$ : it uses stepIoc when $a>0$ and stepIoc₀ when $a=0$ .

Original module imports

import LevyStochCalc.Brownian.ItoFourthMoment

Original declaration excerpt

Shown in the original module context.

noncomputable def stepIocGen (Ω) [MeasurableSpace Ω] {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) :
    SimplePredictable Ω b :=
  if h : 0 < a then stepIoc Ω h hab else stepIoc₀ Ω (lt_of_le_of_lt ha hab)

Module navigation

Direct project imports: LevyStochCalc/Brownian/ItoFourthMoment.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoFourthMoment

/-
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/ItoIncrementMomentRestrict.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 simple integrand `1_{(a, b]}` for `0 ≤ a < b`. -/
noncomputable def stepIocGen (Ω) [MeasurableSpace Ω] {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) :
    SimplePredictable Ω b :=
  if h : 0 < a then stepIoc Ω h hab else stepIoc₀ Ω (lt_of_le_of_lt ha hab)
end Ito
end Brownian
end LevyStochCalc

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Brownian/ItoIncrementMomentRestrict.lean#L137-L140 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Brownian.ItoIncrementMomentRestrict`, definition bundle `KLSModular_LevyStochCalc_Brownian_ItoIncrementMomentRestrict`; 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