Import measurable selection and finite-horizon coupling strategies

[Vilin97]

Imports the measurable-selection and finite-horizon coupling-strategy development from maxwellapexlab/bicausalot-palomar at 3fe500ff64a75d7ab71b474d0c656d5471f62992, retaining all 35 production Lean files and their proved solution bridges.

The principal selection theorem is Kuratowski–Ryll-Nardzewski for nonempty closed-valued, weakly measurable multifunctions into a Polish space. The Bellman identities optimize nested costs over locally feasible coupling strategies. Exact Borel measurable strategies and optimal initial couplings are proved for weakly continuous probability kernels and nonnegative extended-real lower semicontinuous costs on Polish Borel spaces. Equivalence with optimization over bicausal path laws is not established; the two-step IsBicausal₂ interface defines bicausality through kernel decomposition.

The import also includes Jankov–von Neumann uniformization, kernel-section analysis and probability-measure topology. Its basic analytic-set capacitability and universal-measurability support overlaps with FormalLearningTheory; the local Souslin construction is retained for the kernel-section extension. The kernel-section reference now distinguishes that proved finite-kernel variant from the related probability-measure statement in Bertsekas–Shreve, Corollary 7.43.1, p.170.

The Lean 4.34 port preserves KT. Wu's attribution, Apache-2.0 licensing and declared AI provenance. Audit harnesses and duplicate upstream open challenge surfaces are excluded; their production declarations and proved bridges are retained.

Validation: the incoming module-system migration at d21b68194 passed full-pool build/linter/quality/axiom checks and documentation CI. The scope/citation correction changes no Lean executable tokens. Its four changed modules elaborate warning-free, with scoped style, generated-index and project metadata/card/endpoint checks passing locally. Fresh CI for the final head remains required before merge. No checks or linter settings changed.

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.

[Vilin97]

Automation disposition: needs-maintainer

Reviewed exact head 14aa8ed095846f73989587b9643c80fb25b87f8a for this draft pooled-project/content import, Import full bicausal optimal transport development. The changed tree is a substantial source import (including LeanPool/BicausalOT.lean) with the pinned upstream source, project metadata, and generated index present. Observed exact-head required checks have no failures; profile evidence: no proof-profile comment was posted for this exact head.

No concrete author-actionable defect was established in this bounded review that would justify an ordinary change request. The PR is still marked draft, so protected merge is not permitted. Maintainer decision required: confirm the headline result's significance, faithfulness, novelty, source/provenance and scope, then ask the author to mark the PR ready (or give scope direction). This is a maintainer disposition, not an approval.

[Vilin97]

/review

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low risk] Adds mathematical library modules for optimal transport theory.

No new blocking issue was established, but the final-head CI checks are still required before merge.

Summary

The PR imports measurable-selection results and finite-horizon Bellman identities for locally feasible coupling strategies, with an explicit statement that equivalence to optimization over bicausal path laws is not proved.

• The catalog and entry module describe the narrower formalized scope.
• The previously reported duplicate proofs have been consolidated.
• No new actionable issue was established since the previous review. Fresh final-head CI remains pending.

_{Reviews (13) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..."}

[Vilin97]

🤖 LLM review (gpt-6-astra, 5 rubrics)

Reviewed head: c2fb5cd349ca15a9fdb4c7ab6b283f0068c2c315

Verdict: ✅ approve — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	The card faithfully describes the measurable-selection theorem and the restricted finite-horizon coupling-strategy results.
Novelty	✅ pass	Searches of the pinned Mathlib and existing pool found no duplicate of the measurable-selection, uniformization, or finite-horizon strategy headlines.
Significance	✅ pass	This is a substantial, self-contained theory-building project that clearly meets the pool’s significance bar.
Sources	✅ pass	The checked citations support the claims, including the explicitly labelled finite-kernel variant of Bertsekas–Shreve, Corollary 7.43.1, and the upstream formalization is credited.
Code quality (advisory)	✅ pass	The Lean is competently structured, with minor helper duplication that does not warrant delaying merge.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	Selection assumes a complete separable metric Borel target, nonempty closed values, and measurable open-set hit sets. Exact attainment assumes Polish Borel state spaces, probability initial marginals, weakly continuous probability kernels, and nonnegative extended-real lower semicontinuous costs. These match the disclosed regime; feasibility, compactness, and measurable minimizers are proved rather than postulated.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	graduate
Branch	measurable selection and stochastic control
Mode	theory_building
Code quality	3 / 5

Statement check: The headline proves an everywhere-defined selector measurable into the target’s Borel sigma-algebra; the Bellman results optimize nested strategy costs, with path-law equivalence explicitly excluded.

Kuratowski–Ryll-Nardzewski selection and Jankov–von Neumann uniformization support a connected development of finite-horizon Bellman identities and exact Borel optimal coupling strategies under weak continuity and lower semicontinuity assumptions.

Code quality findings (1)

• duplicate-proof — LeanPool/BicausalOT/BicausalOT/UpperBound.lean:32
  Several helpers retain independent copies of the same proof: eps_optimal_element duplicates eps_optimal_element' in DescriptiveSetTheory/JankovVonNeumann.lean:40 verbatim; ennreal_iSup_min_natCast in DescriptiveSetTheory/KernelIntegral.lean:102 is reproved in DescriptiveSetTheory/LintegralLsc.lean:63; and exists_range_measure_ball_compl_lt in DescriptiveSetTheory/ProbabilityMeasurePolish.lean:42 repeats the countable-cover argument later generalized by exists_measure_compl_partial_iUnion_lt at line 370. Consolidate these into shared lower-level lemmas and derive the specialized statements from them, reducing the number of proof bodies needing maintenance during Mathlib upgrades.
  Evidence: UpperBound.lean:32 declares theorem eps_optimal_element, while JankovVonNeumann.lean:40 declares private theorem eps_optimal_element'; both have the conclusion ∃ a ∈ S, f a ≤ (⨅ (x : α) (_ : x ∈ S), f x) + ε and identical proofs beginning by_contra h; simp only [not_exists, not_and, not_le] at h and ending exact absurd this (not_le.mpr (ENNReal.lt_add_right htop hε.ne')). KernelIntegral.lean:102 and LintegralLsc.lean:63 both independently prove ⨆ n : ℕ, min a (n : ℝ≥0∞) = a, beginning refine le_antisymm (iSup_le fun n => min_le_left _ _) ?_ and rcases eq_or_ne a ∞ with rfl | ha. ProbabilityMeasurePolish.lean's two cover proofs independently construct hanti, hinter, and htendsto, invoke tendsto_measure_iInter_atTop, and finish with exact (htendsto.eventually_lt_const hε).exists; the first specializes the second's sets s j to ball (D j) η.

---

Tokens: 10,445,517 in / 28,207 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $211.0259 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

[Vilin97]

Changes requested by automated review

Reviewed exact current head bec1cd1e8bd43c2ab7d25499a7b1db8013d8feaf.

The exact-head Build project check fails because LeanPool.BicausalOT is not module-compatible under the current module root. Port the imported entry and closure, regenerate LeanPool.lean, and rerun complete protected CI.

Acceptance condition: repair the named defect on a new head and make all required protected checks green. Do not change repository policy or add waivers.

[Vilin97]

Changes requested by automated review

Reviewed head 6a4952e2b77dc2b8d34ad905ff885b7557588e72. Selection and restricted Bellman results are substantial, but the advertised bicausal-plan scope needs correction.

1. Complete the pinned-toolchain integration. The exact-head build fails. Its concrete error includes:

   error: LeanPool.lean:1:0: cannot import non-`module` LeanPool.BicausalOT from `module`
   

   The file/dependency audit finds 37 changed Lean files without the required module form. Repair the affected dependency closure, regenerate the module index, and obtain a warning-free full pool build plus the unchanged linter, quality and axiom gates. A project-only or previous-head build does not resolve this failure.

2. Resolve the substantive source/interface defect. The advertised Bellman theorem over path-space bicausal plans is implemented over local strategies; the measurable bridge to bicausal path laws is not supplied. The measurable attainment result also requires the Feller/lower-semicontinuity regime. Supply the bridge or explicitly restrict the title/card/source discussion to the proved strategy theorem and its hypotheses. Disclose the existing analytic-capacitability support in FormalLearningTheory rather than describing that support as wholly new.

Review coverage: complete changed-file inventory and full diff retained; 37 changed project files, 6,743 lines, import reachability and executable trust-token scan; advertised endpoints and supporting definitions examined with bounded implementation sampling and existing review findings reconciled. Potential reusable value: Measurable-selection and transport kernels; Choquet support overlaps FormalLearningTheory. Source/provenance and prior-art evidence were considered separately from CI; these findings do not assert that every proof line was manually read. Earlier automated scores are advisory and are not approval of this failing head.

[Vilin97]

{
"reviewed_head": "c87e3908ee3f10ccfdcc51fabea2e88ee14a0eba",
"verdict": "approve",
"scope": "Resolution review against the complete retained project and prior source review. All 37 project files have identical executable Lean tokens to the full-CI-green module migration d21b681; the new patch changes documentation and the project card only.",
"faithfulness": {
"verdict": "pass",
"evidence": "The registered Kuratowski–Ryll-Nardzewski endpoint assumes nonempty closed values and weak measurability into a complete separable metric Borel space. The title/card now describes finite-horizon locally feasible coupling strategies. MultiPeriod.bellman_value_attained_multi explicitly requires Continuous kernels and LowerSemicontinuous nonnegative extended-real costs. The umbrella and competitor-form docstring disclose the missing path-law equivalence, and Proposition1 identifies IsBicausal₂ as a kernel-decomposition definition."
},
"novelty": {
"verdict": "pass",
"evidence": "The retained development adds substantial measurable-selection, kernel-section and coupling-strategy results. Its overlap with FormalLearningTheory analytic capacitability/universal measurability is explicitly disclosed, with the local Souslin construction retained for the parametrized kernel proof."
},
"significance": {
"verdict": "pass",
"evidence": "Kuratowski–Ryll-Nardzewski selection, Jankov–von Neumann uniformization and measurable finite-horizon strategy attainment form a substantial graduate-level probability/descriptive-set-theory development even within the corrected strategy scope."
},
"sources": {
"verdict": "pass",
"evidence": "Checked Bertsekas–Shreve, Stochastic Optimal Control: The Discrete-Time Case, printed pp.170 and177. Corollary7.43.1 is the related analytic probability-measure superlevel statement; Proposition7.46 is a universal-measurability integration theorem. The kernel-section docstring now cites the former as related and identifies its finite-kernel variant as proved here. Source: MIT book PDF. Pinned upstream source, authorship and declared AI provenance are retained."
},
"code_quality": {
"verdict": "pass",
"evidence": "No proof, declaration, gate or waiver changes. Four changed Lean modules elaborate warning-free; scoped style, static/proof-size, generated module index and project metadata/card/endpoint checks pass. The normal main merge preserves all 218 main project cards and all 219 registered entry imports."
},
"validation_limit": "Fresh final-head CI is required before merging. The incoming d21b681 full-pool build/linter/quality/axiom and documentation checks were green; no whole-pool rebuild was repeated locally.",
"github_review_state": "COMMENT: GitHub prevents this authenticated PR author from submitting APPROVE; approve above is the review recommendation, not a recorded GitHub approval."
}

[Vilin97]

Reviewed current integration head c2fb5cd349ca15a9fdb4c7ab6b283f0068c2c315. The project's complete Lean source is byte-identical to the previously reviewed c87e3908ee3f10ccfdcc51fabea2e88ee14a0eba; the existing mathematical assessment and scoped fixes carry forward. All 218 current-main project cards and this project's complete card retain their values and original text. The actual pinned mk_all --module --check command passes.

Recommendation: accept once fresh required CI passes. This is a lossless main update, not a new claim of a full local rebuild.

[Vilin97]

Approve this bounded shared-helper refactor at df93934dd1b962482863a1401478dfb7d408685c, subject to fresh compilation and all required CI. COMMENT is used because the authenticated account authored the PR.

The existing public ennreal_iSup_min_natCast moves unchanged into a small Mathlib-only ENNRealTruncation module. Both KernelIntegral and LintegralLsc publicly import it, and the latter uses it instead of its private duplicate. The existing public eps_optimal_element moves unchanged to JankovVonNeumann, replacing its identical private copy; UpperBound already publicly imports that module, so both the old public import route and the selection proof retain the same theorem. Public names, types, proof bodies, hypotheses and constructed data are preserved.

The three helpers described as copied in CouplingsCompact each already have a single implementation in the current project. Its changes remove stale draft-integration notes only; its executable tokens are unchanged. The entire named public declaration inventory is retained, the project card is unchanged, and the only root-index change is the new shared module.

Independent source review, the four unchanged scoped source checks, git diff --check, and the actual pinned mk_all --module --check pass. The complete 38-module project import graph is acyclic and every module is directly indexed. No compiler or new compiler waiter was started for this patch; fresh CI remains the elaboration and remaining-gate authority. No check, configuration, waiver, or main refresh changed.

[Vilin97]

Daily disposition: needs maintainer — protected merge operation

Reviewed exact head fe2c41c586e6b4f40126462456a08a78f8ce84ca. The measurable-selection and finite-horizon local-strategy Bellman results are independently significant. The card explicitly disclaims equivalence with bicausal path-law optimization. Shared ENNReal truncation and epsilon-selection lemmas replace duplicates. The complete source/dependency review and recovered repairs were reconciled through the lossless main integration; fresh protected CI remains the integration authority.

Build project: pending/not yet reported, Content / non-content separation: SUCCESS, Documentation preflight: SUCCESS. These are observed check states, not an assertion that unfinished checks passed.

The remaining authority boundary is operational: this repository has allow_auto_merge=false, and GitHub rejected enablePullRequestAutoMerge with “Auto merge is not allowed for this repository.” The maintainer must make protected queuing available through an authorized repository-setting decision, or remove this label and perform a normal squash merge after the required checks and current-base integration pass. This cycle does not change repository settings or bypass protection. No unresolved substantive author-actionable finding justifies another change request or closure; the label is not for draft status, missing profiling, or an old advisory score.