Martingale reindexing by a monotone map

Definition

KLSModular_BrownianMotion_Auxiliary_Martingale

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-contextvendored-brownianmotion

Vendored from the BrownianMotion library (https://github.com/RemyDegenne/brownian-motion, commit a7ad7af662044313bc80a7c0756360fb3745f931). Martingale.indexComap states that if $X$ is a martingale for a filtration $\mathcal F$ , then $X\circ f$ is a martingale for 𝓕.indexComap hf whenever $f$ is monotone. The result preserves the original measure and uses the reindexed filtration described by Filtration.indexComap.

Original module imports

public import BrownianMotion.Auxiliary.Filtration
public import Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
public import Mathlib.Probability.Martingale.Basic

Original declaration excerpt

Shown in the original module context.

lemma Martingale.indexComap (hX : Martingale X 𝓕 P) (hf : Monotone f) :
    Martingale (X ∘ f) (𝓕.indexComap hf) P :=
  ⟨hX.stronglyAdapted.indexComap hf, fun _ _ hij ↦ hX.condExp_ae_eq (hf hij)⟩

Module navigation

Direct project imports: BrownianMotion/Auxiliary/Filtration.

Project result: The KLS conjecture.

Original module · BrownianMotion.Auxiliary.Martingale · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_BrownianMotion_Auxiliary_Filtration
import Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
import Mathlib.Probability.Martingale.Basic

/-
Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne, Thomas Zhu
-/
-- Vendored from https://github.com/RemyDegenne/brownian-motion at commit a7ad7af662044313bc80a7c0756360fb3745f931 (upstream path BrownianMotion/Auxiliary/Martingale.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
section
namespace MeasureTheory
variable {ι Ω E : Type*} [Preorder ι] [NormedAddCommGroup E] [NormedSpace ℝ E]
  {mΩ : MeasurableSpace Ω} {P : Measure Ω} {X : ι → Ω → E} {𝓕 : Filtration ι mΩ}
section IndexComap
variable {ι' : Type*} [Preorder ι'] {f : ι' → ι}
/-- A martingale reindexed by a monotone map is a martingale for the reindexed filtration. -/
lemma Martingale.indexComap (hX : Martingale X 𝓕 P) (hf : Monotone f) :
    Martingale (X ∘ f) (𝓕.indexComap hf) P :=
  ⟨hX.stronglyAdapted.indexComap hf, fun _ _ hij ↦ hX.condExp_ae_eq (hf hij)⟩
end IndexComap
end MeasureTheory

Source

Lean source: https://github.com/RemyDegenne/brownian-motion/blob/a7ad7af662044313bc80a7c0756360fb3745f931/BrownianMotion/Auxiliary/Martingale.lean#L58-L61 (repository human-ai-mathematics/kls-lean, commit 408915f, module `BrownianMotion.Auxiliary.Martingale`, definition bundle `KLSModular_BrownianMotion_Auxiliary_Martingale`; the repository is private at upload time). Vendored from https://github.com/RemyDegenne/brownian-motion at commit a7ad7af662044313bc80a7c0756360fb3745f931 (Apache-2.0; upstream copyright notice retained in the Lean text).

View graph