Independence After Joining the Left Sigma-Algebras

Proved

LevyStochCalc.Probability.indep_sup_left_of_indep_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concavevendored-levystochcalc

This is a sigma-algebra join lemma for independence.

Let $(\Omega,\mathcal F,P)$ be a probability space and let $m_1,m_2,m_3\subseteq\mathcal F$ be measurable spaces. Assume:

$m_1\perp m_3$ under $P$ .
$m_2\perp(m_1\vee m_3)$ under $P$ .

Then the join of the first two sigma-algebras is independent of the third:

m_1\vee m_2\perp m_3.

This technical result packages the product-measure calculation needed to iterate independence along an ordered family of sigma-algebras.

Original Lean declaration header

Within namespace LevyStochCalc.Probability. Shown in its original module context. Proof omitted.

theorem indep_sup_left_of_indep (h₁ : m₁ ≤ mΩ) (h₂ : m₂ ≤ mΩ) (h₃ : m₃ ≤ mΩ)
    (h13 : Indep m₁ m₃ P) (h2 : Indep m₂ (m₁ ⊔ m₃) P) : Indep (m₁ ⊔ m₂) m₃ P

Module navigation

Module: LevyStochCalc/Probability/IndepJoin.

Next: indep_iSup_of_finset.

Source excerpt, lines 48–49 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_LevyStochCalc_Probability_IndepJoin

/-
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/Probability/IndepJoin.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory
variable {Ω : Type*} {m₁ m₂ m₃ mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]

Formal statement


theorem LevyStochCalc.Probability.indep_sup_left_of_indep_readable (h₁ : m₁ ≤ mΩ) (h₂ : m₂ ≤ mΩ) (h₃ : m₃ ≤ mΩ)
    (h13 : Indep m₁ m₃ P) (h2 : Indep m₂ (m₁ ⊔ m₃) P) : Indep (m₁ ⊔ m₂) m₃ P := by sorry

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Probability/IndepJoin.lean#L47-L62 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Probability.IndepJoin`, declaration `LevyStochCalc.Probability.indep_sup_left_of_indep`; 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