Affine grid for Brownian cross-variation arguments

Definition

KLSModular_LevyStochCalc_Brownian_CrossOrthogonalityDirectCross

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. MultidimBrownianMotion.affineGrid a h k is the arithmetic grid point $a+kh$ for $a,h\in\mathbb R$ and $k\in\mathbb N$ .

Original module imports

import LevyStochCalc.Brownian.MultidimFiltered
import LevyStochCalc.Brownian.AugmentedFiltration
import LevyStochCalc.Brownian.ItoFourthMoment

Original declaration excerpt

Shown in the original module context.

noncomputable def affineGrid (a h : ℝ) (k : ℕ) : ℝ := a + k * h

Module navigation

Direct project imports: LevyStochCalc/Brownian/MultidimFiltered, LevyStochCalc/Brownian/AugmentedFiltration, LevyStochCalc/Brownian/ItoFourthMoment.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_MultidimFiltered
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_AugmentedFiltration
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/CrossOrthogonalityDirectCross.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 Brownian
universe u
variable {Ω : Type u} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P] {d : ℕ}
namespace Multidim
namespace MultidimBrownianMotion
section DirectCross
/-- The uniform grid `a, a + h, a + 2h, …`. -/
noncomputable def affineGrid (a h : ℝ) (k : ℕ) : ℝ := a + k * h
end DirectCross
end MultidimBrownianMotion
end Multidim
end Brownian
end LevyStochCalc

Source

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