Polling infrastructure for the relative-independence arguments (R4, #107)

The reusable engine behind the polling arguments: the L²-squeeze tail property, measure preservation of the sortwise action, and the upgrade of fixingAlgebra-invariance from finitely supported to arbitrary permutations. Extracted from Graphon.RelFixingCondIndep when the rankwise relative-independence argument became its second consumer.

Three declarations are public, and are the whole intended interface:

• condExp_ae_eq_condExp_of_comap_eq — the tail engine (Austin, arXiv:0801.1698, proof of Theorem 3.1, abstracted): a measure-preserving T that fixes f a.e. and pulls the conditioning algebra m₁ back to a sub-algebra m₂ ≤ m₁ forces μ[f|m₁] =ᵐ[μ] μ[f|m₂];
• InfiniteRelExchangeableLaw.measurePreserving_relabel — the sortwise action is measure preserving under any exchangeable law, for every permutation family, not merely finitely supported ones;
• InfiniteRelExchangeableLaw.relabel_preimage_ae_eq_of_fixingAlgebra — a fixingAlgebra A-event is invariant modulo the law under every sortwise permutation fixing A, which is what supplies the engine's f ∘ T =ᵐ f.

The L² squeeze and the conditional-expectation transport along MeasurableSpace.comap remain private: they are the proof of the tail engine, not part of its interface.

Generic conditional-expectation tools

theorem RelSignature.condExp_ae_eq_condExp_of_comap_eq {Ω : Type u_1} {m₁ m₂ mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {T : Ω → Ω} (hT : Measurable T) (hTμ : MeasureTheory.MeasurePreserving T μ μ) (hm : m₁ ≤ mΩ) (h2m : m₂ ≤ m₁) (hcomap : MeasurableSpace.comap T m₁ = m₂) {f : Ω → ℝ} (hf : MeasureTheory.MemLp f 2 μ) (hfT : f ∘ T =ᵐ[μ] f) : μ[f | m₁] =ᵐ[μ] μ[f | m₂]

The tail-property engine (Austin, proof of Theorem 3.1, p. 99, abstracted): if a measure-preserving T fixes f a.e. and pulls the conditioning algebra m₁ back to a sub-algebra m₂ ≤ m₁, the two conditional expectations agree a.e. — the energies agree by measure preservation, and the squeeze concludes.

Measure preservation under the exchangeable law

theorem RelSignature.InfiniteRelExchangeableLaw.measurePreserving_relabel {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) (σ : S.Srt → Equiv.Perm ℕ) : MeasureTheory.MeasurePreserving (RelStructure.relabel σ) ↑M.law ↑M.law

The relabeling action is measure preserving under any exchangeable law — for every sortwise permutation, not merely a finitely supported one, since the law is invariant under the full sortwise action by definition.

Arbitrary-permutation a.e. invariance of fixing-algebra events

theorem RelSignature.InfiniteRelExchangeableLaw.relabel_preimage_ae_eq_of_fixingAlgebra {S : RelSignature} [Fintype S.Srt] [Countable S.Rel] (M : S.InfiniteRelExchangeableLaw) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {E : Set (S.RelStructure S.Vinfinite)} (hE : MeasurableSet E) {σ : S.Srt → Equiv.Perm ℕ} (hσ : ∀ v ∈ A, (σ v.fst) v.snd = v.snd) : RelStructure.relabel σ ⁻¹' E =ᵐ[↑M.law] E

Arbitrary-permutation a.e. invariance of fixing-algebra events (the f ∘ T =ᵐ f input of the tail engine): a fixingAlgebra A-event E is invariant under every sortwise permutation fixing A pointwise — not merely finitely supported ones — modulo M.law. This bridges Austin's literally-window-measurable colours (arXiv:0801.1698, Prop 3.12) to the larger invariance-measurable fixingAlgebra A. Proof: approximate E in measure by an initial cylinder D (exists_initialAlgebra_measure_symmDiff_lt, R3); build a finitely supported π agreeing with σ on a window enlarged to contain both the cylinder block and all of A (exists_finSupp_perm_extend) — since σ fixes A and the window covers A, π fixes A, so relabel π ⁻¹' E = E exactly; then μ(σ⁻¹E ∆ E) ≤ μ(σ⁻¹(E ∆ D)) + μ(π⁻¹(D ∆ E)) = 2·μ(E ∆ D) using σ⁻¹D = π⁻¹D (window agreement) and measure preservation, and let the approximation error vanish.