ForMathlib: upstream candidates tracker

[cameronfreer]

Tracker for declarations kept under Graphon/ForMathlib/: statements that are signature-free, depend only on Mathlib, and are plausible upstream contributions. Nothing here is being upstreamed yet. This issue records candidacy and the promotion bar; the actual PR to Mathlib is a separate decision, taken per declaration and not before the bar below is met.

Promotion bar

A candidate is marked Hardened only once it has been consumed independently by at least two real call sites — for the current batch, I(1) and a later rank transition. Two independent consumers are what distinguish a tested orientation of the API from a speculative one; a single consumer tells us only that the statement was convenient for the theorem it was extracted from. Until then a candidate stays Provisional and its signature may change freely.

Current candidates

From #159 (Graphon/ForMathlib/RelativeFactorCoupling.lean):

• ProbabilityTheory.map_condDistrib_id — Provisional. Fibre concentration: (condDistrib id q μ).map q =ᵐ[μ.map q] Kernel.id. Belongs beside condDistrib_comp and condDistrib_self in Mathlib/Probability/Kernel/CondDistrib.lean; it is the missing "conditioning on q pins down q" statement, and both supporting lemmas (condDistrib_id_apply_fibre, ae_ae_eq_condDistrib_id) are immediate from it.
  • Consumers so far: the relative joining in the same file. Needs one genuinely independent consumer.
• ProbabilityTheory.relativeFactorCoupling and its API — Provisional. The relatively independent joining over a common factor, with both marginals, the common-factor identity, and condIndepFun_fst_snd_relativeFactorCoupling. Mathlib has the disintegration and conditional-independence machinery but not this canonical joining.
  • Consumers so far: exists_relativeFactorCoupling_uniform01 (feat: relatively independent joinings over a common factor (#107) #159), which is a specialization rather than an independent use.

Not candidates

Recorded to keep the boundary explicit — these either have one consumer or already compose cleanly from Mathlib primitives, and abstracting them now would cost more than it saves:

• the rank-one finite-family peel (iCondIndepFun_exactMap_singleton);
• a general "kernel concentrated on fibres" predicate — the two a.e. statements above suffice at every site so far;
• the short projection calculations using Kernel.fst_prod / Kernel.snd_prod;
• a general conditional-distribution transport theorem (Incubate and upstream reusable measure/probability infrastructure (Mathlib / Tau Ceti) #24).

Related: #107, #140, #159.

[cameronfreer]

Two additions to Graphon/ForMathlib/RelativeFactorCoupling.lean from #161, both Provisional:

• ProbabilityTheory.map_prodMap_relativeFactorCoupling — a measure-preserving T with q ∘ T = q gives Prod.map T id preserving the joining. Consumer so far: map_prodMap_relabel_rankOneCoupling (I(1)).
• ProbabilityTheory.condIndepFun_comp_fst_snd_relativeFactorCoupling — the transfer clause, conditional independence passed to any measurable reading of the first coordinate. One line from Mathlib's CondIndepFun.comp; named because it is what consumers cite. Consumer so far: condIndepFun_comp_fst_snd_rankOne (I(1)).

Both were driven by I(1) rather than added speculatively, so they meet the "driven by a real consumer" bar — but each has exactly one consumer, and I(1) is the first of the two the promotion bar requires. The later rank transition is the second. Neither is Hardened.

Note for that transition: I(1) leans on the rank-one factor being relabeling invariant on the nose (lowerFactorMap_one_relabel), which holds only because LowerIndex 1 is anchored at ∅. At higher rank the factor map is merely equivariant, so the second consumer will exercise map_prodMap_relativeFactorCoupling in a genuinely different shape — the factor space has to move by lowerFactorSpaceEquiv on the other side. That is the right kind of second consumer for hardening: it will show whether the current signature (a symmetry T of a single space fixing the factor) is the useful orientation, or whether it wants a two-space form with a factor-space equivalence.

[cameronfreer]

Correction to the candidate list, from review of #161 (now merged).

ProbabilityTheory.condIndepFun_comp_fst_snd_relativeFactorCoupling is not an upstream candidate. It is a discoverability wrapper around Mathlib's CondIndepFun.comp — the composition lemma already exists upstream, and this adds only the specialization to relativeFactorCoupling, which would have no meaning in Mathlib unless the joining itself went up first. It stays local and is removed from the tracked list; the promotion bar does not apply to it. It is still worth keeping as a named statement here, because it is what downstream consumers cite rather than re-deriving.

That leaves the candidate list as:

• ProbabilityTheory.map_condDistrib_id — Provisional. Fibre concentration.
• ProbabilityTheory.relativeFactorCoupling and its core API — Provisional. The joining, both marginals, the common-factor identity, condIndepFun_fst_snd_relativeFactorCoupling.
• ProbabilityTheory.map_prodMap_relativeFactorCoupling — Provisional, and the more substantive of the two additions from feat: I(1), the rank-one transfer step (#107) #161: a symmetry of the first space fixing the factor is a symmetry of the joining. It says something about the construction that is not a specialization of an existing Mathlib lemma.

Scope notes recorded while they are fresh:

• The relabeling statement in RelRankOneTransfer is finitary (FinSuppPerm) and that is the exact boundary, not a limitation to fix — the coherent basis is closed under FinSuppPerm and the invariance of empty-anchor events is proved from exactly that closure. Any measure-level or full-permutation formulation should be driven by higher-rank use, not added speculatively.
• No unresolvedStructure object. The theorem quantified over every measurable g is strictly stronger and avoids committing to a particular residual object. A name is warranted only if the recursion introduces a canonical residual state that recurs.

[cameronfreer]

New Provisional candidate from #163: MeasureTheory.condExp_eq_condExp_of_ae_representable (with the iCondIndepFun transfer corollary ProbabilityTheory.iCondIndepFun_congr_of_ae_representable) in Graphon/ForMathlib/CondExpRepresentable.lean.

Conditioning is insensitive to replacing a σ-algebra by one that represents it modulo the measure. Mathlib does not have this, and it sits next to an acknowledged gap: MeasureTheory.EventuallyMeasurable notes that eventual measurability is strictly weaker than a.e. equality to a measurable function and leaves the equivalence as a TODO. This theorem sidesteps that TODO rather than closing it — the uniqueness argument is run with μ[f | m₂] as the candidate at m₁, so the hypothesis is only ever used on sets.

Ledger note, correcting an earlier assumption of mine: applying a parametrized theorem at every n is one consumer, not independent consumers. This will be used at every rank by a single proof path, which does not advance it toward Hardened. It stays Provisional until another proof path genuinely exercises the signature. Upstream value can be high without the label.

[cameronfreer]

Ledger update after #164 (merged, master audit 276).

Promoted to Hardened

• MeasureTheory.Measure.infinitePi_map_comp_equiv — HARDENED. Two genuinely independent consumers via different proof paths: evaluated-law exchangeability, and rank-latent source invariance under relabeling (R4: add rank-indexed latent sources #164). This is the first entry to clear the bar as stated — not one parametrized theorem applied repeatedly, but two separate arguments exercising the signature. Ready for the upstream queue.

New, Provisional

• MeasureTheory.Measure.infinitePi_map_sumPiEquivProdPi (R4: add rank-indexed latent sources #164) — the product decomposition over a sum of index types. Factored at the right boundary already; only the successor source identity consumes it. Not to be generalized to dependent fibres until another use requests that shape — speculative generalization is exactly what the Provisional label exists to prevent.

Local refactors identified, not blockers

Neither blocked #164; both are worth doing before the duplication spreads further:

• rankSublevelSuccEquiv (rank : α → ℕ) (n : ℕ) : {a // rank a < n + 1} ≃ {a // rank a < n} ⊕ {a // rank a = n} — replaces the duplicated successor partition at Graphon/RelRankSuccessor.lean:201 and Graphon/RelRankLatents.lean:199. Clearest immediate local refactor.
• piSplit (e : α ≃ β ⊕ γ) : (α → X) ≃ᵐ (β → X) × (γ → X) — Mathlib supplies piCongrLeft and sumPiEquivProdPi but not their composition. Replaces substantial duplicate constructions across the Bool-valued factor layer and the ℝ-valued latent layer.

Explicitly not abstracting yet

• The rank-preserving actions (basis-index, support, latent). Syntactically similar, meaningfully different data. RankCoding will reveal whether they share a useful interface; abstracting first would fix the wrong interface.
• No custom Finset transport helper — Mathlib already has Equiv.finsetCongr.

Next major extraction

Two-sided equivariance of relativeFactorCoupling: transformations on both source spaces together with an equivalence of factor spaces. The rank transition is now a real second design site, so it should determine the orientation and the a.e. measure, rather than another rank-specific transport theorem being added first. When it lands it replaces map_prodMap_relativeFactorCoupling — the degenerate e = id, U = id case — as the tracked candidate here.

[cameronfreer]

Ledger update after #168 (merged, master audit 280).

Promoted to Hardened

• MeasureTheory.Measure.map_prodMap_compProd_comap — HARDENED. Two independent consumers via distinct proof paths:

  • RelSignature.CoherentBasis.stepKernel_map_ae_eq_comap — step-kernel transport under a sortwise relabeling (refactor: extract compProd/comap change of variables (#107) #165, repointed from the private original it was extracted from);
  • ProbabilityTheory.condDistrib_id_map_comap — fibre transport for the relative factor coupling (feat: two-sided transport of the relative factor coupling (#107) #168).

  These are not one parametrized theorem applied twice: the first identifies two kernels on layer spaces of a coherent basis, the second identifies a disintegration kernel with its own pullback under a factor shift. They exercise the signature from different directions, which is what the bar asks for. Ready for the upstream queue alongside Measure.infinitePi_map_comp_equiv.

Still Provisional

• MeasureTheory.Measure.comp_comap — one consumer (the composition step of map_prodMap_relativeFactorCoupling_two_sided). Stays Provisional.
• ProbabilityTheory.condDistrib_id_map_comap and map_prodMap_relativeFactorCoupling_two_sided (feat: two-sided transport of the relative factor coupling (#107) #168) — new. The two-sided transport now supersedes map_prodMap_relativeFactorCoupling as the tracked candidate for coupling symmetry, its orientation and a.e. base measure having been settled by two design sites as intended. The one-sided form is retained in the library but is no longer the tracked candidate: it avoids hr, hqr and the second measure-preserving map, so it remains the better API where the factor is literally fixed, but it is the degenerate case and not what would go upstream.
• MeasureTheory.condExp_eq_condExp_of_ae_representable and its iCondIndepFun corollary — unchanged, one proof path.
• MeasureTheory.Measure.infinitePi_map_sumPiEquivProdPi — unchanged, one consumer; not to be generalized to dependent fibres until a use asks.

[cameronfreer]

Recording a prospective candidate arising from the i.i.d.-edge regression (#196), not yet under Graphon/ForMathlib/.

• condIndepFun_of_prod_right — Provisional, and currently private. Under μ.prod ν, a left-coordinate observation is conditionally independent of a right-coordinate observation given any conditioning σ-algebra m' ≤ comap Prod.snd — in particular given comap (h ∘ Prod.snd) for measurable h.

Why it is plausibly upstream. Neither Mathlib nor TauCeti has it. Mathlib's MeasureTheory.condExp_indep_eq (Probability/ConditionalExpectation.lean:42) gives the single-factor half — the conditional expectation of an m₁-measurable function given an independent m₂ is the constant mean — but not the intersection case E[1_{A∩B} ∣ m'] = μ(A) · E[1_B ∣ m'] that conditional independence needs. TauCeti's closest result (Probability/Independence/Conditional.lean:62) turns a conditional-expectation "drop the extra information" identity into conditional independence, which is a usable route, but the product-measure computation itself is unproved there too. So this is a genuine gap rather than overlooked API.

Consumers so far: one — rank-two screening in the i.i.d.-edge regression. Under this issue's promotion bar that keeps it Provisional, and it therefore stays private to the regression module rather than moving to ForMathlib/ now. The natural second consumer would be any later product-coupling screening argument; if one appears, the lemma moves to ForMathlib/ and becomes a candidate here in the ordinary way.

Stated generally over m' ≤ comap Prod.snd rather than only for comap (h ∘ Prod.snd), so the instantiation is a corollary and the abstraction is tested at the point of use.