Moving a block through a reindexing, over an invariant event

Over a shift-invariant event, a law-preserving reindexing that is eventually a translation changes no set-integral; so for a contractable law, where strict monotonicity supplies that preservation, a strictly increasing finite selection may be displaced onto the prefix 0, 1, …, m - 1.

Measure preservation cannot be dropped: without it the first claim fails outright — take ρ a point mass at an alternating path, A = univ and φ = (· + 1). Eventual translation is a sufficient condition for the reindexing to fix every invariant event, not a necessary one for the integral identity, which needs only T ⁻¹' A = A.

Main results

• measurePreserving_restrict_reindex_of_measurableSet_invariants_of_eventually_add — the primitive: such a reindexing preserves the restricted law, so Koopman-side consumers get a MeasurePreserving, not only an integral identity;

• ContractableLaw.map_restrict_prefixProj_of_strictMono_of_measurableSet_invariants — the finite-selection form as a measure equality on the restricted law: reading a strictly increasing block and reading the prefix push ρ.restrict A to the same measure, so Bochner and Lᵖ statements follow as well. The unrestricted counterpart is the existing ContractableLaw.map_prefixProj_of_strictMono.

• integral_mul_block_eq_prefixProj_of_strictMono_of_measurable_invariants and its set-integral form setIntegral_mul_block_eq_prefixProj_of_strictMono_of_measurable_invariants (both in the ContractableLaw namespace) — the same displacement against an invariant weight, which is unchanged by the reindexing (comp_reindex_apply_eq_of_measurable_invariants_of_eventually_add) and so rides through the change of variables. An invariant event is a special invariant weight, so the second follows from the first by applying it to A.indicator w. This is the form an induction peeling one coordinate at a time needs, since the factors already peeled accumulate as such a weight.

• ContractableLaw.measure_inter_blockCylinder_eq_prefix_of_strictMono_of_measurableSet_invariants — the block-cylinder corollary: over an invariant event, the mass of a block cylinder does not depend on which strictly increasing selection cuts it, and may be read at the prefix.

The one ℝ≥0∞ statement here is the block-cylinder mass corollary above, an equality of measure values. The transport results themselves are not restated in ℝ≥0∞: a consumer wanting that applies .lintegral_comp to the MeasurePreserving above, or rewrites with lintegral_map through the measure equality. A weighted ℝ≥0∞ form is available both ways: via .lintegral_comp together with comp_reindex_apply_eq_of_measurable_invariants_of_eventually_add, or as a measure equality on ρ.withDensity w, which the reindexing preserves because it preserves ρ and fixes w. It is the signed real weight that cannot ride in an equality of positive measures, which is why the ℝ-valued statements above are integral identities.

The endomorphism-level facts are Mathlib's: MeasurePreserving.restrict_preimage gives the restricted measure preservation once the invariant event is rewritten by preimage_reindex_eq_of_measurableSet_invariants_of_eventually_add, and MeasurePreserving.lintegral_comp gives the integral identity. This module supplies only the reindexing-and-invariant-event instance, and restates no Mathlib API.

Nothing here is specific to a de Finetti route. The statements mention a contractable path law, a shift-invariant event and a finite selection, and no Koopman operator; the Koopman route is the motivating consumer: ViaKoopman/CylinderMass.lean imports this for the block-cylinder corollary.

Invariance, not tail-measurability

⚠ These results rest on invariance: shift ⁻¹' A = A, in the MeasurableSpace.invariants-measurable form. A tail event need not satisfy it, and invariants_shift_lt_pathTail shows the inclusion is strict already over Bool. This is the substantive difference from the L² route, whose block comparison is distributional — an equality of conditional laws given the tail — rather than an actual invariance of the test event.

The general statement asks only that the reindexing preserve the law. Contractability and strict monotonicity are one way to obtain that, not requirements: a merely shift-invariant law with φ = (· + C) qualifies.

Source

No material is adapted from cameronfreer/exchangeability. That development carries its own block-reindexing and factorization material for the Koopman argument; the statements here were assembled from Tau Ceti's own pieces — the eventual-translation extension StrictMono.exists_strictMono_nat_extending_fin_eventually_add, the invariant-event preimage identity preimage_reindex_eq_of_measurableSet_invariants_of_eventually_add, contractable reindexing ContractableLaw.measurePreserving_reindex, and Mathlib's MeasurePreserving.restrict_preimage.

theorem TauCeti.Probability.measurePreserving_restrict_reindex_of_measurableSet_invariants_of_eventually_add {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} {φ : ℕ → ℕ} {m C : ℕ} (hmp : MeasureTheory.MeasurePreserving (fun (x : ℕ → α) (k : ℕ) => x (φ k)) ρ ρ) (hφ_add : ∀ (n : ℕ), m ≤ n → φ n = n + C) {A : Set (ℕ → α)} (hA : MeasurableSet A) : MeasureTheory.MeasurePreserving (fun (x : ℕ → α) (k : ℕ) => x (φ k)) (ρ.restrict A) (ρ.restrict A)

Such a reindexing preserves the restricted law. The primitive form: consumers needing the Koopman operator on Lp (ρ.restrict A), or a Bochner integral, get a MeasurePreserving rather than only an ℝ≥0∞ identity.

Only measure preservation by this reindexing is used; contractability and strict monotonicity are one way to obtain it, not requirements. In particular a merely shift-invariant law with φ = (· + C) qualifies.

theorem TauCeti.Probability.ContractableLaw.map_restrict_prefixProj_of_strictMono_of_measurableSet_invariants {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ContractableLaw ρ) {m : ℕ} {k : Fin m → ℕ} (hk : StrictMono k) {A : Set (ℕ → α)} (hA : MeasurableSet A) : MeasureTheory.Measure.map (fun (x : ℕ → α) (i : Fin m) => x (k i)) (ρ.restrict A) = MeasureTheory.Measure.map (prefixProj α m) (ρ.restrict A)

The primitive measure equality. Over an invariant event, reading a strictly increasing block and reading the prefix push the restricted law to the same measure on Fin m → α.

This is the form that gives Bochner integrals and Lᵖ statements as well; an ℝ≥0∞ identity follows by rewriting with lintegral_map, and is not restated here.

theorem TauCeti.Probability.ContractableLaw.integral_mul_block_eq_prefixProj_of_strictMono_of_measurable_invariants {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ContractableLaw ρ) {m : ℕ} {k : Fin m → ℕ} (hk : StrictMono k) {w : (ℕ → α) → ℝ} (hw : Measurable w) {f : (Fin m → α) → ℝ} (hf : Measurable f) : ∫ (x : ℕ → α), w x * f fun (i : Fin m) => x (k i) ∂ρ = ∫ (x : ℕ → α), w x * f (prefixProj α m x) ∂ρ

An invariants-measurable weight rides through the block-to-prefix change of variables.

The unweighted statement is an equality of positive measures, so a signed real weight cannot ride in it; that is why this is an integral identity. (A nonnegative weight can: the reindexing preserves ρ.withDensity w, since it preserves ρ and fixes w. That is the route to an ℝ≥0∞ weighted statement, and is not restated here.)

The weight is unchanged by the reindexing, by comp_reindex_apply_eq_of_measurable_invariants_of_eventually_add, so it passes through the measure-preserving change of variables alongside the block observable.

theorem TauCeti.Probability.ContractableLaw.setIntegral_mul_block_eq_prefixProj_of_strictMono_of_measurable_invariants {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ContractableLaw ρ) {m : ℕ} {k : Fin m → ℕ} (hk : StrictMono k) {A : Set (ℕ → α)} (hA : MeasurableSet A) {w : (ℕ → α) → ℝ} (hw : Measurable w) {f : (Fin m → α) → ℝ} (hf : Measurable f) : ∫ (x : ℕ → α) in A, w x * f fun (i : Fin m) => x (k i) ∂ρ = ∫ (x : ℕ → α) in A, w x * f (prefixProj α m x) ∂ρ

The set-integral form over an invariant event. An invariant event is just a special invariant weight: apply the unrestricted statement to A.indicator w.

theorem TauCeti.Probability.ContractableLaw.measure_inter_blockCylinder_eq_prefix_of_strictMono_of_measurableSet_invariants {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ContractableLaw ρ) {r : ℕ} {k : Fin r → ℕ} (hk : StrictMono k) {B : Fin r → Set α} (hB : ∀ (i : Fin r), MeasurableSet (B i)) {A : Set (ℕ → α)} (hA : MeasurableSet A) : ρ (A ∩ blockCylinder (fun (j : ℕ) (x : ℕ → α) => x j) k B) = ρ (A ∩ blockCylinder (fun (j : ℕ) (x : ℕ → α) => x j) (fun (i : Fin r) => ↑i) B)

The mass of a block cylinder met with an invariant event may be read at the prefix.

For a contractable law, a shift-invariant event, measurable coordinate sets and a strictly increasing selection, the mass of the intersection equals that of the intersection with the prefix cylinder.

theorem TauCeti.Probability.ContractableLaw.setIntegral_comp_coord_eq_comp_zero_of_measurableSet_invariants {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ContractableLaw ρ) (r : ℕ) {A : Set (ℕ → α)} (hA : MeasurableSet A) {f : α → ℝ} (hf : Measurable f) : ∫ (x : ℕ → α) in A, f (x r) ∂ρ = ∫ (x : ℕ → α) in A, f (x 0) ∂ρ

Every coordinate has the same set-integral over an invariant event. The single-coordinate instance of the block transport: reading coordinate r and reading coordinate 0 give the same integral of any measurable real observable, over any invariant event.