Prove2Me

Natural filtrations for multidimensional Brownian motion

Definition
KLSModular_LevyStochCalc_Brownian_MultidimFiltered

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

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

Vendored from LevyStochCalc (https://github.com/cgarryZA/LevyStochCalc). sigmaBrownian W is the sigma-algebra generated by all values of a scalar Brownian motion. MultidimBrownianMotion.naturalFiltration W is the pointwise supremum of the natural filtrations of the component Brownian motions. These are definitions of the generated measurable structures and filtration; the listed declarations do not assert the downstream Brownian-filtration property.

Original module imports

import LevyStochCalc.Brownian.Filtered
import LevyStochCalc.Brownian.Multidim

Original declaration excerpt

Shown in the original module context.

noncomputable abbrev sigmaBrownian (W : BrownianMotion P) : MeasurableSpace Ω :=
  ⨆ t, MeasurableSpace.comap (W.W t) inferInstance

Module navigation

Direct project imports: LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Multidim.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_Filtered
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_Multidim

/-
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/MultidimFiltered.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory
namespace LevyStochCalc
namespace Brownian
universe u
variable {Ω : Type u} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P] {d : ℕ}
/-- The σ-algebra generated by all the values of a Brownian motion. -/
noncomputable abbrev sigmaBrownian (W : BrownianMotion P) : MeasurableSpace Ω :=
  ⨆ t, MeasurableSpace.comap (W.W t) inferInstance
namespace Multidim
namespace MultidimBrownianMotion
/-- The joint natural filtration `⨆ i, ℱ^{Wⁱ}` of a multidimensional Brownian motion. -/
noncomputable def naturalFiltration (W : MultidimBrownianMotion P d) :
    Filtration ℝ ‹MeasurableSpace Ω› :=
  ⨆ i, Martingale.naturalFiltration (W.W i)
end MultidimBrownianMotion
end Multidim
end Brownian
end LevyStochCalc
Source
Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Brownian/MultidimFiltered.lean#L32-L82 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Brownian.MultidimFiltered`, definition bundle `KLSModular_LevyStochCalc_Brownian_MultidimFiltered`; 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