Poisson filtrations

Definition

KLSModular_LevyStochCalc_Poisson_Filtered

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

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

Vendored from the LevyStochCalc library (https://github.com/cgarryZA/LevyStochCalc), commit 984dbf0b790031eac05d56fe5a84b65e15e1e932. IsPoissonFiltration N ℱ requires counts on measurable subsets of $(-\infty,t]\times E$ to be $\mathcal F_t$ -measurable. It also requires, for every $s\ge0$ , independence under $P$ between $\mathcal F_s$ and the sigma-algebra generated by counts on all measurable subsets of $(s,\infty)\times E$ . IsPoissonFiltration.indep derives independence from $\mathcal F_s$ for a finite-mark-measure strip $(s,t]\times A$ when $0\le s<t$ .

Original module imports

import LevyStochCalc.Poisson.PastFutureIndependence
import LevyStochCalc.Probability.ComapTuple
import LevyStochCalc.Probability.IndepJoin
import LevyStochCalc.Probability.IndepLimit

Original declaration excerpt

Shown in the original module context.

structure IsPoissonFiltration (N : PoissonRandomMeasure P ν)
    (ℱ : Filtration ℝ ‹MeasurableSpace Ω›) : Prop where
  measurable : ∀ ⦃t : ℝ⦄ ⦃B : Set (ℝ × E)⦄, B ⊆ Set.Iic t ×ˢ Set.univ → MeasurableSet B →
    Measurable[ℱ t] (fun ω => N.N ω B)
  indep_future : ∀ ⦃s : ℝ⦄, 0 ≤ s →
    Indep (ℱ s) (⨆ D ∈ {D : Set (ℝ × E) | D ⊆ Set.Ioi s ×ˢ Set.univ ∧ MeasurableSet D},
      MeasurableSpace.comap (fun ω => N.N ω D) inferInstance) P

Module navigation

Direct project imports: LevyStochCalc/Poisson/PastFutureIndependence, LevyStochCalc/Probability/ComapTuple, LevyStochCalc/Probability/IndepJoin, LevyStochCalc/Probability/IndepLimit.

Project result: The KLS conjecture.

Original module · LevyStochCalc.Poisson.Filtered · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_LevyStochCalc_Poisson_PastFutureIndependence
import Definitions.Def_KLSModular_LevyStochCalc_Probability_ComapTuple
import Definitions.Def_KLSModular_LevyStochCalc_Probability_IndepJoin
import Definitions.Def_KLSModular_LevyStochCalc_Probability_IndepLimit

/-
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/Poisson/Filtered.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory Filter Topology
open scoped ENNReal
namespace LevyStochCalc
namespace Poisson
universe u v
variable {Ω : Type u} [MeasurableSpace Ω] {E : Type v} [MeasurableSpace E]
  {P : Measure Ω} [IsProbabilityMeasure P] {ν : Measure E} [SigmaFinite ν]
/-- `N` is a Poisson random measure for the filtration `ℱ`: its counts on measurable regions
of `(-∞, t] × E` are `ℱ t`-measurable, and for `0 ≤ s` the σ-algebra `ℱ s` is independent of
the σ-algebra generated by the counts on the measurable regions of `(s, ∞) × E`. -/
structure IsPoissonFiltration (N : PoissonRandomMeasure P ν)
    (ℱ : Filtration ℝ ‹MeasurableSpace Ω›) : Prop where
  measurable : ∀ ⦃t : ℝ⦄ ⦃B : Set (ℝ × E)⦄, B ⊆ Set.Iic t ×ˢ Set.univ → MeasurableSet B →
    Measurable[ℱ t] (fun ω => N.N ω B)
  indep_future : ∀ ⦃s : ℝ⦄, 0 ≤ s →
    Indep (ℱ s) (⨆ D ∈ {D : Set (ℝ × E) | D ⊆ Set.Ioi s ×ˢ Set.univ ∧ MeasurableSet D},
      MeasurableSpace.comap (fun ω => N.N ω D) inferInstance) P
/-- The σ-algebra `ℱ s` is independent of the count on a future strip `(s, t] × A` of finite
mark measure. -/
theorem IsPoissonFiltration.indep {N : PoissonRandomMeasure P ν}
    {ℱ : Filtration ℝ ‹MeasurableSpace Ω›} (h : IsPoissonFiltration N ℱ) :
    ∀ ⦃s t : ℝ⦄, 0 ≤ s → s < t → ∀ ⦃A : Set E⦄, MeasurableSet A → ν A ≠ ⊤ →
      Indep (ℱ s) (MeasurableSpace.comap (fun ω => N.N ω (Set.Ioc s t ×ˢ A)) inferInstance) P := by
  intro s t hs _ A hA _
  exact indep_of_indep_of_le_right (h.indep_future hs)
    (le_iSup₂_of_le (Set.Ioc s t ×ˢ A)
      ⟨Set.prod_mono Set.Ioc_subset_Ioi_self (Set.subset_univ A), measurableSet_Ioc.prod hA⟩ le_rfl)
end Poisson
end LevyStochCalc

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Poisson/Filtered.lean#L34-L54 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Poisson.Filtered`, definition bundle `KLSModular_LevyStochCalc_Poisson_Filtered`; 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