Auxiliary maps for Ionescu-Tulcea theorem

This file contains auxiliary maps which are used to prove the Ionescu-Tulcea theorem.

def IocProdIoc {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [DecidableLE ι] {X : ι → Type u_2} (a b c : ι) (x : ((i : { x : ι // x ∈ Finset.Ioc a b }) → X ↑i) × ((i : { x : ι // x ∈ Finset.Ioc b c }) → X ↑i)) (i : { x : ι // x ∈ Finset.Ioc a c }) : X ↑i

Gluing Ioc a b and Ioc b c into Ioc a c.

Equations

• IocProdIoc a b c x i = if h : ↑i ≤ b then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩

theorem measurable_IocProdIoc {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [DecidableLE ι] {X : ι → Type u_2} [(i : ι) → MeasurableSpace (X i)] {a b c : ι} : Measurable (IocProdIoc a b c)

def IicProdIoc {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [DecidableLE ι] {X : ι → Type u_2} [LocallyFiniteOrderBot ι] (a b : ι) (x : ((i : { x : ι // x ∈ Finset.Iic a }) → X ↑i) × ((i : { x : ι // x ∈ Finset.Ioc a b }) → X ↑i)) (i : { x : ι // x ∈ Finset.Iic b }) : X ↑i

Gluing Iic a and Ioc a b into Iic b. If b < a, this is just a projection on the first coordinate followed by a restriction, see IicProdIoc_le.

Equations

• IicProdIoc a b x i = if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩

theorem IicProdIoc_def {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [DecidableLE ι] {X : ι → Type u_2} [LocallyFiniteOrderBot ι] (a b : ι) : IicProdIoc a b = fun (x : ((i : { x : ι // x ∈ Finset.Iic a }) → X ↑i) × ((i : { x : ι // x ∈ Finset.Ioc a b }) → X ↑i)) (i : { x : ι // x ∈ Finset.Iic b }) => if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩

When IicProdIoc is only partially applied (i.e. IicProdIoc a b x but not IicProdIoc a b x i) simp [IicProdIoc] won't unfold the definition. This lemma allows to unfold it by writing simp [IicProdIoc_def].

theorem frestrictLe₂_comp_IicProdIoc {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [DecidableLE ι] {X : ι → Type u_2} [LocallyFiniteOrderBot ι] {a b : ι} (hab : a ≤ b) : Preorder.frestrictLe₂ hab ∘ IicProdIoc a b = Prod.fst

theorem restrict₂_comp_IicProdIoc {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [DecidableLE ι] {X : ι → Type u_2} [LocallyFiniteOrderBot ι] (a b : ι) : Finset.restrict₂ ⋯ ∘ IicProdIoc a b = Prod.snd

@[simp]

theorem IicProdIoc_self {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [DecidableLE ι] {X : ι → Type u_2} [LocallyFiniteOrderBot ι] (a : ι) : IicProdIoc a a = Prod.fst

theorem IicProdIoc_le {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [DecidableLE ι] {X : ι → Type u_2} [LocallyFiniteOrderBot ι] {a b : ι} (hba : b ≤ a) : IicProdIoc a b = Preorder.frestrictLe₂ hba ∘ Prod.fst

theorem IicProdIoc_comp_restrict₂ {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [DecidableLE ι] {X : ι → Type u_2} [LocallyFiniteOrderBot ι] {a b : ι} : Finset.restrict₂ ⋯ ∘ IicProdIoc a b = Prod.snd

theorem measurable_IicProdIoc {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [DecidableLE ι] {X : ι → Type u_2} [LocallyFiniteOrderBot ι] [(i : ι) → MeasurableSpace (X i)] {m n : ι} : Measurable (IicProdIoc m n)

def MeasurableEquiv.IicProdIoc {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [DecidableLE ι] {X : ι → Type u_2} [LocallyFiniteOrderBot ι] [(i : ι) → MeasurableSpace (X i)] {a b : ι} (hab : a ≤ b) : ((i : { x : ι // x ∈ Finset.Iic a }) → X ↑i) × ((i : { x : ι // x ∈ Finset.Ioc a b }) → X ↑i) ≃ᵐ ((i : { x : ι // x ∈ Finset.Iic b }) → X ↑i)

Gluing Iic a and Ioc a b into Iic b. This version requires a ≤ b to get a measurable equivalence.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasurableEquiv.coe_IicProdIoc {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [DecidableLE ι] {X : ι → Type u_2} [LocallyFiniteOrderBot ι] [(i : ι) → MeasurableSpace (X i)] {a b : ι} (hab : a ≤ b) : ⇑(IicProdIoc hab) = _root_.IicProdIoc a b

theorem MeasurableEquiv.coe_IicProdIoc_symm {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [DecidableLE ι] {X : ι → Type u_2} [LocallyFiniteOrderBot ι] [(i : ι) → MeasurableSpace (X i)] {a b : ι} (hab : a ≤ b) : ⇑(IicProdIoc hab).symm = fun (x : (i : { x : ι // x ∈ Finset.Iic b }) → X ↑i) => (Preorder.frestrictLe₂ hab x, Finset.restrict₂ ⋯ x)

def MeasurableEquiv.IicProdIoi {ι : Type u_1} [LinearOrder ι] [DecidableLE ι] {X : ι → Type u_2} [LocallyFiniteOrderBot ι] [(i : ι) → MeasurableSpace (X i)] (a : ι) : ((i : { x : ι // x ∈ Finset.Iic a }) → X ↑i) × ((i : ↑(Set.Ioi a)) → X ↑i) ≃ᵐ ((n : ι) → X n)

Gluing Iic a and Ioi a into ℕ, version as a measurable equivalence on dependent functions.

Equations

• One or more equations did not get rendered due to their size.

def MeasurableEquiv.piSingleton {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (a : ℕ) : X (a + 1) ≃ᵐ ((i : { x : ℕ // x ∈ Finset.Ioc a (a + 1) }) → X ↑i)

Identifying {a + 1} with Ioc a (a + 1), as a measurable equiv on dependent functions.

Equations

• One or more equations did not get rendered due to their size.

theorem IocProdIoc_preimage {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [DecidableLE ι] {X : ι → Type u_2} {a b c : ι} (hab : a ≤ b) (hbc : b ≤ c) (s : (i : { x : ι // x ∈ Finset.Ioc a c }) → Set (X ↑i)) : IocProdIoc a b c ⁻¹' Set.univ.pi s = Set.univ.pi (Finset.restrict₂ ⋯ s) ×ˢ Set.univ.pi (Finset.restrict₂ ⋯ s)

theorem IicProdIoc_preimage {ι : Type u_1} [LinearOrder ι] [LocallyFiniteOrder ι] [DecidableLE ι] {X : ι → Type u_2} [LocallyFiniteOrderBot ι] {a b : ι} (hab : a ≤ b) (s : (i : { x : ι // x ∈ Finset.Iic b }) → Set (X ↑i)) : IicProdIoc a b ⁻¹' Set.univ.pi s = Set.univ.pi (Preorder.frestrictLe₂ hab s) ×ˢ Set.univ.pi (Finset.restrict₂ ⋯ s)