Pooled polling: the Austin route, unit 1 (R4 converse, #107, #197) #
Route A (Austin) only. Nothing from the Kallenberg spine appears here, and nothing in this module asserts that the two routes' outputs agree — they prove the same statement by different means and will not produce canonically equal representations.
What is Austin's here, and what is not #
The construction follows Austin (arXiv:0801.1698): a spare vertex reservoir, mixed clusters —
those not wholly original, all-spare included — and an enriched law that carries the polling data
forward. PoolVertex S s is
Vinfinite S s ⊕ Vinfinite S s, with originalVertex = Sum.inl and poolVertex = Sum.inr, so the
two halves are disjoint definitionally, and a PooledRankExtension is invariant under the full
pooled permutation family.
The conditional-independence engine is not Austin's, and this module does not reprove his
Proposition 3.12. RankRepresentation.screening is a field — an inductive hypothesis assumed at
rank n — and its remainder already contains every other rank-≤ n block together with the whole
pooled latent array. Weak union converts that directly into the mutual statement, so the
tail-polling argument is not needed at this inductive stage and no tail machinery appears here.
Stating otherwise would credit this file with a theorem it does not contain.
The geometry, and a trap it sets #
The observed blocks are confined to the original half: originalBlock A reads the block at
supportImage (originalVertex S) A, every vertex of which is a Sum.inl. The poll is confined to
supports containing at least one Sum.inr. The two families are therefore disjoint by
construction, which is the whole point — a block that could itself lie in the poll would make the
conditional independence say nothing.
Reading the blocks instead through the canonical identification pooledJointEquiv is tempting,
because it makes the transport to C.P an exact identification. It is wrong here:
poolVertexEquiv is a bijection PoolVertex ≃ Vinfinite, so blocks read through it range across
both summands rather than being confined to the original half, while the poll reads the spare
half — the two would overlap.
The seam is an enriched law, not C.P #
Austin's polling data must survive into the next law; forgetting it into a bare C.P statement
would discard exactly what the successor construction consumes. That data is the family of
mixed clusters — pooled rank-n blocks that are not wholly original — and not merely the
induced structure on the spare half. "Mixed" is the negation of "wholly original", so an all-spare
support qualifies, its original part being empty and therefore proper.
pollingClusters— the mixed cluster observation, indexed byMixedClusterIndex: pooled rank-nsupports containing at least one spare vertex, all-spare supports included. Each such support has a proper original part, since at least one of itsnvertices is spare; for an all-spare support that part is empty, which is proper as well.enrichedPollingLaw— the pushforward ofQ.lawretaining the original structure and old latents together with the auxiliary polling data: the whole pooled rank-nlatent array and the clusters.enrichedPollingLaw_map_fst— the first marginal isC.Pexactly, proved throughQ.map_restrict_embedding (originalVertex S). The gate theorem is a compiled dependency here, not a citation.
The conditioning is pinned by pollingCond: the whole pooled rank-n latent array together with
the clusters. It is a definition rather than a witness field, because an existential conditioning
factor could be taken to be the whole joint object and would make the conclusion vacuous. Every index of
RankLatentIndex S n has cardinality < n, so the latent half of the conditioning is
proper-subset data carrying no rank-n block.
Scope #
- Only the ambient
Countableassumptions are needed. Because the conditional independence comes from the assumed screening contract rather than from a polling argument, theFintype S.Srthypothesis that the fixing-algebra stack carries is not required here. - Rank zero is not this module's business. The successor at
n = 0is supplied bynonempty_rankRepresentation_onetogether withtruncation_zero, which is also what respectsstepKernel's deliberate lack of anA = ∅realization theorem.
The conditioning σ-algebra may be replaced by an equal one, for a family. The
CondIndepFun form is shared glue in ForMathlib/CondIndepSup.lean; this is its iCondIndepFun
counterpart, route-local while its consumers are internal to this development. Needed because the
conditioning algebra occurs in a dependent position — the ≤ proof mentions it — so rw cannot
reach it.
Weak union for conditional independence #
The graphoid axiom this development turns on, and which neither Mathlib nor this repository has:
if X is conditionally independent of (Y, Z) given W, and W is contained in Z, then X
is conditionally independent of Y given Z alone. The containment W ≤ Z is what lets the
conclusion condition on exactly Z rather than on an unsimplified W ⊔ Z.
Kept private under the standing promotion rule: private at one consumer, extracted to
ForMathlib/ once a second independent consumer exists.
The proof is the standard one. The key step is that enlarging the conditioning from W to any
algebra between W and Y ⊔ Z does not change the conditional probability of an X-event —
proved by conditional-expectation uniqueness, with the product identity supplying the set
integrals. Applying that at Y ⊔ Z and at Z, and then peeling with the tower property, gives the
result.
Blocks on the original half #
The rank-n block family on the original half. Every vertex of
supportImage (originalVertex S) A is a Sum.inl, so this family is disjoint from the poll below
by construction.
Equations
Instances For
The mixed clusters #
Mixed cluster indices: pooled rank-n supports that are not wholly original, i.e.
containing at least one spare vertex. All-spare supports are included — "mixed" is the negation of
"wholly original", not a demand that both halves be met. The original part of such a support is a
proper subset of it, since at least one of its n vertices is spare, and for an all-spare
support that part is empty; this is the sense in which the clusters are indexed by proper original
subsets.
Equations
Instances For
The cluster observation space.
Equations
Instances For
The mixed cluster observation — the poll. Each coordinate is a pooled rank-n block that
is not wholly original; no coordinate is an original-half block, since every index carries a spare
vertex.
Equations
Instances For
The enriched law #
The enriched observation space: the original structure and old latents, together with the
auxiliary polling data — the whole pooled rank-n latent array and the clusters.
The pooled latent array is carried alongside the original marginal rather than replacing it, so
the first component is untouched and enrichedPollingLaw_map_fst stays literally what it was. The pooled array is the right lower-rank factor because Q.screening's remainder
restObservationOver n A already contains it in full, and weak union conditions on exactly that
factor. Every pooled latent index has cardinality < n, so the latent component reveals no
rank-n block; the clusters, by contrast, are rank-n blocks at supports that are not wholly
original, and carrying them is the point of the poll.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The enriched polling map: restrict to the original half, and retain the poll.
Equations
Instances For
The enriched polling law. Austin's polling data survives here: the whole pooled rank-n
latent array and the clusters are retained alongside the original structure and old latents, rather
than being forgotten into a bare C.P statement.
Equations
Instances For
The enriched law refines the representation: forgetting the clusters returns C.P exactly.
Proved through Q.map_restrict_embedding at the original-vertex embedding, so the pooled gate
theorem is a compiled dependency of everything downstream.
The conditioning #
The polling conditioning, pinned concretely: the whole pooled rank-n latent array
together with the mixed clusters — that is, the auxiliary component. Not a witness field: an
existential factor could be taken to be the whole joint object and would make the conclusion
vacuous.
The array read is the pooled one because Q.screening's remainder contains it in full and weak
union conditions on exactly that lower-rank factor. Every index has cardinality < n, so the
latent half carries no rank-n block.
Equations
Instances For
The source-level conditioning #
Steps 1–4 of the construction run under Q.law, on the pooled space, and only the final descent
moves to the enriched law. sourcePollingCond is the conditioning read there, and it is the
same observation: pollingCond ∘ enrichedPollingMap is definitionally sourcePollingCond, so
no transport is needed to relate the two statements.
The polling conditioning read directly on the pooled space.
Equations
Instances For
The two conditionings agree, definitionally: conditioning on the enriched law and conditioning on the pooled law are the same observation composed with the enriching map.
Check 1: the local conditioning at any pooled support is measurable from the source polling
conditioning — it is a coordinate projection of the pooled latent component. This is the W ≤ Z
hypothesis of weak union, discharged concretely rather than assumed.
What the screening remainder supplies #
Q.screening gives conditional independence of the block at a pooled support A from
restObservationOver n A — the other rank-≤ n blocks together with the whole pooled latent
array. Weak union needs that remainder to dominate both the accumulated F-blocks and the whole
polling conditioning. restToPollingData exhibits that as a single measurable factorization rather
than as a bare algebra inequality, so it records exactly which information the remainder supplies
and lets CondIndepFun.comp consume the screening statement directly.
A support in the image of the original half carries no spare vertex.
Separation, original against original: distinct rank-n supports have distinct images,
since supportImage is injective.
Separation, cluster against original: a mixed cluster carries a spare vertex, while the image of an original support is wholly original.
The accumulated block observation space, indexed by a finite family of rank-n supports.
Equations
Instances For
The screening remainder computes both sides of the weak-union hypothesis: the accumulated
F-blocks and the entire polling conditioning are read off restObservationOver n A alone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The exact factorization. Both the accumulated blocks and the polling conditioning are functions of the screening remainder, on the nose.
The conditioning algebra is the fixed one #
Named rather than left to simp: the forward descent at the end of the construction has to be
visibly exact, and that requires an explicit identity between the algebra the source statement
conditions on and the pullback of pollingCond.
Check 3: the source conditioning algebra is the pullback of the enriched conditioning.
The insertion identity #
The peel step, assembled from the pieces above: Q.screening at the original image of e, its
remainder pushed through restToPollingData, comap_prodMk to split the resulting algebra into
the accumulated blocks joined with the polling conditioning, and weak union to drop back to the
polling conditioning alone. Stated as a direct conditional-expectation identity so that it feeds
Finset.induction_on with Finset.set_biInter_insert and Finset.prod_insert, without any
dependent tuple reindexing inside the induction.
The source-level mutual theorem #
Named rather than inlined into the witness: it is the load-bearing consumer of
polling_condExp_insert and the direct input to the forward descent, so keeping it separate makes
it independently reviewable and leaves the final constructor carrying no probability argument of
its own.
Mutual conditional independence of the whole rank-n block family under Q.law, given the
polling conditioning. The peel is structurally the singleton peel: the empty stage is a constant,
and each insertion is discharged by polling_condExp_insert against the induction hypothesis, with
the conditioning algebra fixed throughout.
Transport to the enriched law #
Two obligations, both discharged by named identities so that nothing is coerced ad hoc inside the
witness constructor: the conditioning algebra (check 3) and the block codomains. The source
family lands in BlockSpaceOver (PoolVertex S) (supportImage (originalVertex S) A), whereas the
witness reads blockMap A on the restricted original structure; blockSpaceCongr is the
measurable equivalence between them and blockMapOver_restrict is the naturality that relates the
two readings exactly.
The block codomains agree, exactly. Reading a block of the restricted original structure is
reading the pooled block at the image support and transporting along blockSpaceCongr.
Forward transport of mutual conditional independence along a measurable map. Route-local:
public within the Austin development, which has more than one consumer for it, but not promoted to
ForMathlib/ — that awaits a consumer independent of this route. No injectivity is needed, which
is why neither direction of the existing transport API applies: the maps that build the enriched
objects forget the spare half of the structure.
The witness #
The polling conclusion: mutual conditional independence of the entire rank-n block
family of the original structure, given the pooled latents and the mixed clusters, under the
enriched law.
iCondIndepFun over the whole family is the shape Austin's Proposition 3.12 delivers, but here it
is obtained from the assumed rank-n screening contract by weak union rather than by a tail-polling
argument. Pairwise independence, or one block against the rest, would be strictly weaker, and the
adversarial battery of #196 exists to keep that distinction honest.
- mutualCondIndep : ProbabilityTheory.iCondIndepFun (MeasurableSpace.comap (pollingCond S n) inferInstance) ⋯ (fun (A : S.RankSupport n) => blockMap ↑A ∘ Prod.fst ∘ Prod.fst) (enrichedPollingLaw Q)
Mutual conditional independence of the whole rank-
nblock family.
Instances For
The polling witness exists, for every pooled rank extension. Pure transport: the
probability content is iCondIndepFun_originalBlock_sourcePollingCond, and this constructor only
moves it along enrichedPollingMap, matching the block codomains by blockSpaceCongr and the
conditioning algebra by the named identity.