Joint Measurability of the Eldan Path

Proved

FunctionalInequalities.KLS.BKL.Localization.IsEldanCutoff.measurable_uncurry_path_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This auxiliary measurability theorem concerns an IsEldanCutoff process $p_t(\omega)$ .

For the product space $\Omega\times\mathbb R$ , the map

(\omega,s)\longmapsto p_s(\omega)

is measurable.

This fact supports product-measure integration and Fubini or Tonelli arguments involving time and sample variables.

Formalization Note. The Lean expression is fun z : Ω × ℝ => p z.2 z.1; the order of the product coordinates is $(\omega,s)$ after projection.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.BKL.Localization. Shown in its original module context. Proof omitted.

theorem IsEldanCutoff.measurable_uncurry_path (h : IsEldanCutoff μ hc W ℱ hW γ p) :
    Measurable (fun z : Ω × ℝ => p z.2 z.1)

Module navigation

Module: KLS/BKL/Localization/Process/Integral.

Definition modules: KLS/BKL/Localization/Process/Basic, KLS/BKL/Localization/Coefficients, LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Multidim.

Previous: IsEldanCutoff.integrable_integral_of_ae_bound · Next: ae_prod_restrict_Ioc_of_ae.

Source excerpt, lines 109–110 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_Process_Integral

variable {n : ℕ} (μ : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))).support)
variable {μ hc} {Ω : Type*} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {W : LevyStochCalc.Brownian.Multidim.MultidimBrownianMotion P n} {ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›}
  {hW : ∀ k, LevyStochCalc.Brownian.IsBrownianFiltration (W.W k) ℱ} {γ : FunctionalInequalities.KLS.BKL.Localization.Param n → ℝ} {p : ℝ → Ω → FunctionalInequalities.KLS.BKL.Localization.Param n}

Formal statement


theorem FunctionalInequalities.KLS.BKL.Localization.IsEldanCutoff.measurable_uncurry_path_readable (h : IsEldanCutoff μ hc W ℱ hW γ p) :
    Measurable (fun z : Ω × ℝ => p z.2 z.1) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/Process/Integral.lean#L108-L123 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.Process.Integral`, declaration `FunctionalInequalities.KLS.BKL.Localization.IsEldanCutoff.measurable_uncurry_path`; the repository is private at upload time).

View graph