Block cylinders and their indicator products

For a process X : ℕ → Ω → α and a finite coordinate selection k : Fin m → ℕ:

• blockCylinder X k C = {ω | ∀ i, X (k i) ω ∈ C i} — the cylinder event on the selected coordinates (matching the blockLaw selection vocabulary; the first-r prefix is the case k = fun i => i.val);
• blockIndicatorProd X k C ω = ∏ i, 𝟙_{C i}(X (k i) ω) — its (ℝ-valued) indicator product.

These events and integrands describe finite-dimensional rectangles for arbitrary measurable sequences, without any symmetry assumption. They are used in finite-block factorization arguments. blockCylinder_eq_preimage_univ_pi and blockLaw_blockCylinder bridge the cylinder to the existing rectangle/blockLaw interface, while blockCylinder_eq_iInter gives the intersection form, which is what a proof meeting the cylinder with another event wants. blockIndicatorProd_eq_indicator identifies the product with the cylinder indicator, and integrable_blockIndicatorProd records integrability under a finite measure.

Adapted from cameronfreer/exchangeability (PathSpace/CylinderHelpers.lean, DeFinetti/ViaMartingale/IndicatorAlgebra.lean, pin e0532e59ceff23edab44dda9ab0655debbc9cc22).

def TauCeti.Probability.blockCylinder {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) {m : ℕ} (k : Fin m → ℕ) (C : Fin m → Set α) : Set Ω

The block cylinder event on the selected coordinates: {ω | ∀ i, X (k i) ω ∈ C i}.

Equations

• TauCeti.Probability.blockCylinder X k C = {ω : Ω | ∀ (i : Fin m), X (k i) ω ∈ C i}

@[simp]

theorem TauCeti.Probability.mem_blockCylinder {Ω : Type u_1} {α : Type u_2} {X : ℕ → Ω → α} {m : ℕ} {k : Fin m → ℕ} {C : Fin m → Set α} {ω : Ω} : ω ∈ blockCylinder X k C ↔ ∀ (i : Fin m), X (k i) ω ∈ C i

Membership in the block cylinder: ω lies in blockCylinder X k C iff every selected coordinate X (k i) ω lies in its set C i.

theorem TauCeti.Probability.blockCylinder_eq_preimage_univ_pi {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) {m : ℕ} (k : Fin m → ℕ) (C : Fin m → Set α) : blockCylinder X k C = (fun (ω : Ω) (i : Fin m) => X (k i) ω) ⁻¹' Set.univ.pi C

The block cylinder is the preimage of the rectangle Set.univ.pi C under the selected-coordinate map ω ↦ (X (k ·) ω).

theorem TauCeti.Probability.blockCylinder_eq_iInter {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) {m : ℕ} (k : Fin m → ℕ) (C : Fin m → Set α) : blockCylinder X k C = ⋂ (i : Fin m), X (k i) ⁻¹' C i

The block cylinder is the intersection of the selected coordinates' preimages. This is the ⋂ counterpart of blockCylinder_eq_preimage_univ_pi: the rectangle form suits pushforwards and block laws, this one suits intersections with another event.

theorem TauCeti.Probability.measurableSet_blockCylinder {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {X : ℕ → Ω → α} {m : ℕ} {k : Fin m → ℕ} {C : Fin m → Set α} (hX : ∀ (i : Fin m), Measurable (X (k i))) (hC : ∀ (i : Fin m), MeasurableSet (C i)) : MeasurableSet (blockCylinder X k C)

The block cylinder of a process with measurable selected coordinates on measurable sets is measurable.

theorem TauCeti.Probability.blockLaw_blockCylinder {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} (X : ℕ → Ω → α) {m : ℕ} {k : Fin m → ℕ} {C : Fin m → Set α} (hX : ∀ (i : Fin m), AEMeasurable (X (k i)) μ) (hC : ∀ (i : Fin m), MeasurableSet (C i)) : (blockLaw μ X k) (Set.univ.pi C) = μ (blockCylinder X k C)

The block law evaluated on a measurable rectangle is the measure of the block cylinder: blockLaw μ X k (Set.univ.pi C) = μ (blockCylinder X k C). A blockCylinder-named restatement of blockLaw_apply_rectangle.

theorem TauCeti.Probability.blockCylinder_comp_perm {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) {m : ℕ} (k : Fin m → ℕ) (C : Fin m → Set α) (e : Equiv.Perm (Fin m)) : blockCylinder X k C = blockCylinder X (k ∘ ⇑e) fun (i : Fin m) => C (e i)

A block cylinder is invariant under permuting the selection. Reordering the coordinates of a block, and the sets along with them, describes the same event: membership is a conjunction over the index set, which a permutation does not change.

This is what lets a proof supply only strictly monotone selections: Tuple.sort permutes an arbitrary injective k into increasing order, and this lemma says the event is unaffected.

theorem TauCeti.Probability.exists_perm_strictMono_comp_blockCylinder_eq_and_prod_eq {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) {m : ℕ} {k : Fin m → ℕ} (hk : Function.Injective k) (B : Fin m → Set α) : ∃ (e : Equiv.Perm (Fin m)), StrictMono (k ∘ ⇑e) ∧ (blockCylinder X k B = blockCylinder X (k ∘ ⇑e) fun (i : Fin m) => B (e i)) ∧ ∀ {M : Type u_3} [inst : CommMonoid M] (g : Set α → M), ∏ i : Fin m, g (B (e i)) = ∏ i : Fin m, g (B i)

Sorting an injective block selection. Any injective k can be permuted into strictly increasing order without changing the block event or any product over the selected sets.

This packages the whole reduction that lets a proof handle only the monotone case, and the name records all three parts: Tuple.sort supplies the permutation, blockCylinder_comp_perm says the block event is unchanged (_blockCylinder_eq), and the final clause says a product over the selected sets is unchanged (_and_prod_eq), for any commutative monoid. Callers that establish an identity for strictly monotone selections get the injective case by obtaining this and rewriting.

noncomputable def TauCeti.Probability.blockIndicatorProd {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) {m : ℕ} (k : Fin m → ℕ) (C : Fin m → Set α) : Ω → ℝ

The product of the selected coordinate indicators, ∏ i, 𝟙_{C i}(X (k i) ω).

Equations

• TauCeti.Probability.blockIndicatorProd X k C ω = ∏ i : Fin m, (C i).indicator (fun (x : α) => 1) (X (k i) ω)

@[simp]

theorem TauCeti.Probability.blockIndicatorProd_apply {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) {m : ℕ} (k : Fin m → ℕ) (C : Fin m → Set α) (ω : Ω) : blockIndicatorProd X k C ω = ∏ i : Fin m, (C i).indicator (fun (x : α) => 1) (X (k i) ω)

Pointwise value of the indicator product: the product of the selected coordinate indicators.

theorem TauCeti.Probability.blockIndicatorProd_eq_indicator {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) {m : ℕ} (k : Fin m → ℕ) (C : Fin m → Set α) : blockIndicatorProd X k C = (blockCylinder X k C).indicator fun (x : Ω) => 1

The indicator product is the indicator of the block cylinder.

@[simp]

theorem TauCeti.Probability.blockIndicatorProd_empty {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (k : Fin 0 → ℕ) (C : Fin 0 → Set α) : blockIndicatorProd X k C = fun (x : Ω) => 1

The empty (zero-coordinate) indicator product is the constant-one function.

theorem TauCeti.Probability.blockIndicatorProd_succ_eq_indicator_inter {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) {r : ℕ} (k : Fin (r + 1) → ℕ) (C : Fin (r + 1) → Set α) : blockIndicatorProd X k C = ((blockCylinder X (fun (i : Fin r) => k i.castSucc) fun (j : Fin r) => C j.castSucc) ∩ X (k (Fin.last r)) ⁻¹' C (Fin.last r)).indicator fun (x : Ω) => 1

Successor split of the indicator product. Splitting off the last selected coordinate, the length-r+1 indicator product equals the indicator of the length-r prefix cylinder intersected with the last coordinate's preimage. The Fin 0 companion is blockIndicatorProd_empty.

theorem TauCeti.Probability.nullMeasurableSet_blockCylinder {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {m : ℕ} {k : Fin m → ℕ} {C : Fin m → Set α} (hX : ∀ (i : Fin m), AEMeasurable (X (k i)) μ) (hC : ∀ (i : Fin m), MeasurableSet (C i)) : MeasureTheory.NullMeasurableSet (blockCylinder X k C) μ

The block cylinder is null-measurable when the selected coordinates are a.e. measurable.

theorem TauCeti.Probability.integrable_blockIndicatorProd {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} {m : ℕ} {k : Fin m → ℕ} {C : Fin m → Set α} (hX : ∀ (i : Fin m), AEMeasurable (X (k i)) μ) (hC : ∀ (i : Fin m), MeasurableSet (C i)) : MeasureTheory.Integrable (blockIndicatorProd X k C) μ

The indicator product is integrable under a finite measure (a.e.-measurable coordinates).

theorem TauCeti.Probability.lintegral_blockCylinder_indicator {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {m : ℕ} {k : Fin m → ℕ} {C : Fin m → Set α} (hX : ∀ (i : Fin m), AEMeasurable (X (k i)) μ) (hC : ∀ (i : Fin m), MeasurableSet (C i)) : ∫⁻ (ω : Ω), (blockCylinder X k C).indicator (fun (x : Ω) => 1) ω ∂μ = (blockLaw μ X k) (Set.univ.pi C)

The block law of a rectangle is the lintegral of the block-cylinder indicator. For a.e.-measurable selected coordinates, ∫⁻ ω, 𝟙_{blockCylinder X k C}(ω) ∂μ = blockLaw μ X k (∏ᵢ C i). Being an ℝ≥0∞ lintegral, this is the honest identity for an arbitrary measure (no finiteness needed).

theorem TauCeti.Probability.integral_blockIndicatorProd {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {m : ℕ} {k : Fin m → ℕ} {C : Fin m → Set α} (hX : ∀ (i : Fin m), AEMeasurable (X (k i)) μ) (hC : ∀ (i : Fin m), MeasurableSet (C i)) : ∫ (ω : Ω), blockIndicatorProd X k C ω ∂μ = ((blockLaw μ X k) (Set.univ.pi C)).toReal

The real (Bochner) integral of the indicator product is the block law of the rectangle: ∫ ω, ∏ i, 𝟙_{C i}(X (k i) ω) ∂μ = (blockLaw μ X k (∏ᵢ C i)).toReal — the real (toReal) form of the ℝ≥0∞ identity lintegral_blockCylinder_indicator (integrability under a finite measure is integrable_blockIndicatorProd).