Vilin97 · Vilin97 · Sep 21, 2026 · Sep 21, 2026 · Sep 21, 2026 · Sep 22, 2026
diff --git a/LeanPool.lean b/LeanPool.lean
@@ -381,6 +381,44 @@ public import LeanPool.Besicovitch.SixPoint.WeightedFailure
 public import LeanPool.Besicovitch.SixPoint.WeightedReduction
 public import LeanPool.Besicovitch.Statement
 public import LeanPool.Besicovitch.Topology.ConnectedComponent
+public import LeanPool.BicausalOT
+public import LeanPool.BicausalOT.BicausalOT
+public import LeanPool.BicausalOT.BicausalOT.Basic
+public import LeanPool.BicausalOT.BicausalOT.BicausalOT
+public import LeanPool.BicausalOT.BicausalOT.Defs
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.AnalyticSet
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.AnalyticSigmaAlgebra
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.Capacitability
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.CouplingsCompact
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.CouplingsUHC
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.ENNRealTruncation
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.EpsOptimalSelection
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.JankovVonNeumann
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.KernelIntegral
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.LintegralLsc
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.LowerSemianalytic
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.LsaAlgebra
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.LscIntegral
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.MeasurableSelection
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.ProbabilityMeasurePolish
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.Tree
+public import LeanPool.BicausalOT.BicausalOT.Existence
+public import LeanPool.BicausalOT.BicausalOT.FeasNonempty
+public import LeanPool.BicausalOT.BicausalOT.LowerBound
+public import LeanPool.BicausalOT.BicausalOT.LscBellman
+public import LeanPool.BicausalOT.BicausalOT.MeasurableFeasibleStrategy
+public import LeanPool.BicausalOT.BicausalOT.MeasurableStrategy
+public import LeanPool.BicausalOT.BicausalOT.MultiPeriod
+public import LeanPool.BicausalOT.BicausalOT.MultiPeriodTopology
+public import LeanPool.BicausalOT.BicausalOT.Proposition1
+public import LeanPool.BicausalOT.BicausalOT.SemianalyticValue
+public import LeanPool.BicausalOT.BicausalOT.UpperBound
+public import LeanPool.BicausalOT.BicausalOT.ValueRepresentation
+public import LeanPool.BicausalOT.Solution
+public import LeanPool.BicausalOT.SolutionCapacitability
+public import LeanPool.BicausalOT.SolutionJvN
+public import LeanPool.BicausalOT.SolutionPolish
 public import LeanPool.Biswal
 public import LeanPool.Biswal.Theorem1
 public import LeanPool.Biswal.Theorem23

diff --git a/LeanPool/BicausalOT.lean b/LeanPool/BicausalOT.lean
@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2026 KT. Wu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: KT. Wu
+-/
+
+module
+
+public import LeanPool.BicausalOT.BicausalOT
+public import LeanPool.BicausalOT.BicausalOT.Basic
+public import LeanPool.BicausalOT.BicausalOT.BicausalOT
+public import LeanPool.BicausalOT.BicausalOT.Defs
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.AnalyticSet
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.AnalyticSigmaAlgebra
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.Capacitability
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.CouplingsCompact
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.CouplingsUHC
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.EpsOptimalSelection
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.JankovVonNeumann
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.KernelIntegral
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.LintegralLsc
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.LowerSemianalytic
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.LsaAlgebra
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.LscIntegral
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.MeasurableSelection
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.ProbabilityMeasurePolish
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.Tree
+public import LeanPool.BicausalOT.BicausalOT.Existence
+public import LeanPool.BicausalOT.BicausalOT.FeasNonempty
+public import LeanPool.BicausalOT.BicausalOT.LowerBound
+public import LeanPool.BicausalOT.BicausalOT.LscBellman
+public import LeanPool.BicausalOT.BicausalOT.MeasurableFeasibleStrategy
+public import LeanPool.BicausalOT.BicausalOT.MeasurableStrategy
+public import LeanPool.BicausalOT.BicausalOT.MultiPeriod
+public import LeanPool.BicausalOT.BicausalOT.MultiPeriodTopology
+public import LeanPool.BicausalOT.BicausalOT.Proposition1
+public import LeanPool.BicausalOT.BicausalOT.SemianalyticValue
+public import LeanPool.BicausalOT.BicausalOT.UpperBound
+public import LeanPool.BicausalOT.BicausalOT.ValueRepresentation
+public import LeanPool.BicausalOT.Solution
+public import LeanPool.BicausalOT.SolutionCapacitability
+public import LeanPool.BicausalOT.SolutionJvN
+public import LeanPool.BicausalOT.SolutionPolish
+
+
+/-!
+# BicausalOT: measurable selection and coupling strategies
+
+Source: url:https://github.com/maxwellapexlab/bicausalot-palomar
+Authors: KT. Wu
+Status: verified
+Main declarations: `MeasurableSelection.exists_measurable_selection`
+Tags: probability
+MSC: 28B20, 54C65, 54H05, 03E15, 28A20, 68V20
+-/
+
+/-! ## Scope
+
+The Bellman identities compare nested strategy costs with Bellman recursions over locally
+feasible one-step couplings. The development does not establish equivalence with minimization
+over bicausal measures on a path space. Exact Borel measurable strategies and optimal initial
+couplings are obtained for weakly continuous probability kernels and nonnegative extended-real
+lower semicontinuous costs on Polish Borel spaces; see
+`MultiPeriod.bellman_value_attained_multi`.
+
+The basic analytic-set capacitability and universal measurability results overlap with
+`LeanPool.FormalLearningTheory.PureMath.ChoquetCapacity` and
+`LeanPool.FormalLearningTheory.PureMath.AnalyticMeasurability`. This development also proves
+analytic superlevel sets for finite-kernel sections, measurable selection, and coupling-strategy
+results. Its local Souslin-scheme construction supports the kernel-section proof.
+-/
+
+@[expose] public section
diff --git a/LeanPool/BicausalOT/BicausalOT.lean b/LeanPool/BicausalOT/BicausalOT.lean
@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2026 KT. Wu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: KT. Wu
+-/
+-- This module serves as the root of the `BicausalOT` library.
+-- Import modules here that should be built as part of the library.
+module
+
+public import LeanPool.BicausalOT.BicausalOT.Basic
+
+
+/-!
+# BicausalOT
+
+Supporting results for bicausal optimal transport and measurable selection.
+-/
+
+@[expose] public section
diff --git a/LeanPool/BicausalOT/BicausalOT/Basic.lean b/LeanPool/BicausalOT/BicausalOT/Basic.lean
@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 KT. Wu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: KT. Wu
+-/
+-- Re-export all modules
+module
+
+public import LeanPool.BicausalOT.BicausalOT.Defs
+public import LeanPool.BicausalOT.BicausalOT.Proposition1
+public import LeanPool.BicausalOT.BicausalOT.LowerBound
+public import LeanPool.BicausalOT.BicausalOT.UpperBound
+public import LeanPool.BicausalOT.BicausalOT.ValueRepresentation
+public import LeanPool.BicausalOT.BicausalOT.Existence
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.AnalyticSet
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.LowerSemianalytic
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.Tree
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.JankovVonNeumann
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.Capacitability
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.KernelIntegral
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.ProbabilityMeasurePolish
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.LsaAlgebra
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.CouplingsCompact
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.LintegralLsc
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.MeasurableSelection
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.EpsOptimalSelection
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.CouplingsUHC
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.LscIntegral
+public import LeanPool.BicausalOT.BicausalOT.MultiPeriod
+public import LeanPool.BicausalOT.BicausalOT.MultiPeriodTopology
+public import LeanPool.BicausalOT.BicausalOT.FeasNonempty
+public import LeanPool.BicausalOT.BicausalOT.SemianalyticValue
+public import LeanPool.BicausalOT.BicausalOT.MeasurableStrategy
+public import LeanPool.BicausalOT.BicausalOT.LscBellman
+public import LeanPool.BicausalOT.BicausalOT.MeasurableFeasibleStrategy
+
+
+/-!
+# Basic
+
+Supporting results for bicausal optimal transport and measurable selection.
+-/
+
+@[expose] public section
diff --git a/LeanPool/BicausalOT/BicausalOT/BicausalOT.lean b/LeanPool/BicausalOT/BicausalOT/BicausalOT.lean
@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2026 KT. Wu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: KT. Wu
+-/
+/-
+  Bicausal Optimal Transport — Bellman Recursion (T=1)
+  Formally verified in Lean 4 + Mathlib.
+
+  Main result: bellman_value_eq (Value Representation Theorem)
+
+  Structure:
+    Defs.lean                              — definitions
+    Proposition1.lean                      — bicausal ↔ kernel decomposition
+    LowerBound.lean                        — Step 2: ∫V₀ ≤ totalCost
+    UpperBound.lean                        — Step 3: ε-optimal construction
+    ValueRepresentation.lean               — Step 4: equality (main theorem)
+    Existence.lean                         — Step 5: optimal coupling exists
+    DescriptiveSetTheory/
+      Tree.lean                            — Jankov–von Neumann uniformization (Kechris 18.1)
+      JankovVonNeumann.lean                — ε-optimal selection
+      AnalyticSigmaAlgebra.lean            — σ(Σ₁¹), analytical measurability
+      LowerSemianalytic.lean               — lower semianalytic functions (BS 7.21, 7.47)
+      Capacitability.lean                  — Choquet capacitability (Kechris 30.13, BS 7.42)
+      KernelIntegral.lean                  — kernel integration of l.s.a. functions (BS 7.48)
+    AxiomsAudit.lean                       — #print axioms for every theorem
+
+  Status: 0 error, 0 warning, 0 sorry, 0 custom axioms project-wide
+          (machine-checked: every audited theorem depends only on
+           [propext, Classical.choice, Quot.sound])
+-/
+module
+
+public import LeanPool.BicausalOT.BicausalOT.Defs
+public import LeanPool.BicausalOT.BicausalOT.Proposition1
+public import LeanPool.BicausalOT.BicausalOT.LowerBound
+public import LeanPool.BicausalOT.BicausalOT.UpperBound
+public import LeanPool.BicausalOT.BicausalOT.ValueRepresentation
+public import LeanPool.BicausalOT.BicausalOT.Existence
+
+
+/-!
+# BicausalOT
+
+Supporting results for bicausal optimal transport and measurable selection.
+-/
+
+@[expose] public section
diff --git a/LeanPool/BicausalOT/BicausalOT/Defs.lean b/LeanPool/BicausalOT/BicausalOT/Defs.lean
@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2026 KT. Wu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: KT. Wu
+-/
+/-
+  Bicausal OT — Definitions
+  Couplings, feasible sets, kernel decomposition, bicausality, Bellman value.
+-/
+module
+
+public import Mathlib.Algebra.Order.Module.Field
+public import Mathlib.Data.EReal.Inv
+public import Mathlib.Tactic.Measurability
+public import Mathlib.Topology.Algebra.InfiniteSum.Order
+public import Mathlib.Topology.MetricSpace.Bounded
+public import Mathlib.MeasureTheory.Measure.Prod
+public import Mathlib.Probability.Kernel.Basic
+
+
+/-!
+# Defs
+
+Supporting results for bicausal optimal transport and measurable selection.
+-/
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory Set ENNReal
+
+noncomputable section
+
+variable {X₀ X₁ Y₀ Y₁ : Type*}
+variable [MeasurableSpace X₀] [MeasurableSpace X₁]
+variable [MeasurableSpace Y₀] [MeasurableSpace Y₁]
+
+/-- The measures coupling the two initial marginals. -/
+def CouplingSet₀ (μ₀ : Measure X₀) (ν₀ : Measure Y₀) :
+    Set (Measure (X₀ × Y₀)) :=
+  { γ | γ.map Prod.fst = μ₀ ∧ γ.map Prod.snd = ν₀ }
+
+/-- The measures coupling the next-step conditional marginals at a given initial pair. -/
+def FeasibleSet₀
+    (κ_μ : X₀ → Measure X₁) (κ_ν : Y₀ → Measure Y₁)
+    (z₀ : X₀ × Y₀) : Set (Measure (X₁ × Y₁)) :=
+  { γ | γ.map Prod.fst = κ_μ z₀.1 ∧ γ.map Prod.snd = κ_ν z₀.2 }
+
+/-- An initial coupling and a measurable conditional kernel disintegrating a two-step plan. -/
+structure KernelDecomp
+    (π : Measure ((X₀ × X₁) × (Y₀ × Y₁))) where
+  /-- The initial coupling in the decomposition. -/
+  γ₀ : Measure (X₀ × Y₀)
+  /-- The conditional coupling kernel for the second time step. -/
+  γ₁ : X₀ × Y₀ → Measure (X₁ × Y₁)
+  γ₁_measurable : Measurable γ₁
+  decomp : ∀ ⦃s : Set ((X₀ × X₁) × (Y₀ × Y₁))⦄,
+    MeasurableSet s →
+    π s = ∫⁻ z₀, (γ₁ z₀) {z₁ | ((z₀.1, z₁.1), (z₀.2, z₁.2)) ∈ s} ∂γ₀
+
+/-- A two-step plan admits a kernel decomposition with the prescribed marginals at each step. -/
+def IsBicausal₂
+    (μ₀ : Measure X₀) (ν₀ : Measure Y₀)
+    (κ_μ : X₀ → Measure X₁) (κ_ν : Y₀ → Measure Y₁)
+    (π : Measure ((X₀ × X₁) × (Y₀ × Y₁))) : Prop :=
+  ∃ (kd : KernelDecomp π),
+    kd.γ₀ ∈ CouplingSet₀ μ₀ ν₀ ∧
+    ∀ᵐ z₀ ∂kd.γ₀, kd.γ₁ z₀ ∈ FeasibleSet₀ κ_μ κ_ν z₀
+
+variable (c₀ : X₀ × Y₀ → ENNReal) (c₁ : (X₀ × Y₀) × (X₁ × Y₁) → ENNReal)
+
+/-- The initial cost plus the infimum of conditional continuation costs over feasible couplings. -/
+def V₀ (κ_μ : X₀ → Measure X₁) (κ_ν : Y₀ → Measure Y₁)
+    (z₀ : X₀ × Y₀) : ENNReal :=
+  c₀ z₀ + ⨅ (γ : Measure (X₁ × Y₁)) (_ : γ ∈ FeasibleSet₀ κ_μ κ_ν z₀),
+    ∫⁻ z₁, c₁ (z₀, z₁) ∂γ
+
+/-- The expected sum of the initial and continuation costs under the decomposed plan. -/
+def totalCost (kd_γ₀ : Measure (X₀ × Y₀))
+    (kd_γ₁ : X₀ × Y₀ → Measure (X₁ × Y₁)) : ENNReal :=
+  ∫⁻ z₀, (c₀ z₀ + ∫⁻ z₁, c₁ (z₀, z₁) ∂(kd_γ₁ z₀)) ∂kd_γ₀
+
+end
diff --git a/LeanPool/BicausalOT/BicausalOT/DescriptiveSetTheory.lean b/LeanPool/BicausalOT/BicausalOT/DescriptiveSetTheory.lean
@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2026 KT. Wu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: KT. Wu
+-/
+
+module
+
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.AnalyticSet
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.AnalyticSigmaAlgebra
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.Capacitability
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.CouplingsCompact
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.CouplingsUHC
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.EpsOptimalSelection
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.JankovVonNeumann
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.KernelIntegral
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.LintegralLsc
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.LowerSemianalytic
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.LsaAlgebra
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.LscIntegral
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.MeasurableSelection
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.ProbabilityMeasurePolish
+public import LeanPool.BicausalOT.BicausalOT.DescriptiveSetTheory.Tree
+
+
+/-!
+# DescriptiveSetTheory
+
+Supporting modules for BicausalOT.
+-/
+
+@[expose] public section
diff --git a/LeanPool/BicausalOT/BicausalOT/DescriptiveSetTheory/AnalyticSet.lean b/LeanPool/BicausalOT/BicausalOT/DescriptiveSetTheory/AnalyticSet.lean
@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2026 KT. Wu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: KT. Wu
+-/
+/-
+  Analytic Sets — re-exported from Mathlib
+
+  Mathlib already has the full theory in:
+    Mathlib.MeasureTheory.Constructions.Polish.Basic
+
+  Key results available:
+    - `MeasureTheory.AnalyticSet` (definition)
+    - `MeasurableSet.analyticSet` (Borel ⊆ Analytic)
+    - `AnalyticSet.image_of_continuous` (continuous image)
+    - `AnalyticSet.iUnion` (countable union)
+    - `AnalyticSet.iInter` (countable intersection)
+    - `AnalyticSet.measurablySeparable` (Lusin separation)
+
+  NO sorry needed — everything is already in Mathlib.
+-/
+module
+
+public import Mathlib.MeasureTheory.Constructions.Polish.Basic
+
+
+/-!
+# AnalyticSet
+
+Supporting results for bicausal optimal transport and measurable selection.
+-/
+
+@[expose] public section
+
+-- Re-export for downstream modules
+open MeasureTheory