Measurable equivalences

Measurable equivalences between product and pi types, used to manipulate histories of sequential learning algorithms (elements of Fin n → 𝓐 × 𝓨 or Iic n → 𝓐 × 𝓨).

• MeasurableEquiv.uniqueProd, MeasurableEquiv.prodUnique: drop a component that lives in a type with a unique element.
• MeasurableEquiv.IicSuccProd: (Π i : Iic (n + 1), X i) ≃ᵐ (Π i : Iic n, X i) × X (n + 1).
• MeasurableEquiv.finSuccPiIic: (Π i : Fin (n + 1), X i) ≃ᵐ (Π i : Iic n, X i).
• MeasurableEquiv.finSuccProd: (Fin (n + 1) → X) ≃ᵐ (Fin n → X) × X.

theorem measurableEmbedding_prodMk_left_of_measurableSet {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {x : α} (hx : MeasurableSet {x}) : MeasurableEmbedding (Prod.mk x)

Prod.mk x is a measurable embedding as soon as {x} is measurable. This generalises measurableEmbedding_prodMk_left, which assumes MeasurableSingletonClass.

theorem coe_default_Iic_zero : ↑default = 0

def MeasurableEquiv.uniqueProd (α : Type u_1) (β : Type u_2) [MeasurableSpace α] [MeasurableSpace β] [Unique α] : α × β ≃ᵐ β

The measurable equivalence α × β ≃ᵐ β when α has a unique element.

Equations

• MeasurableEquiv.uniqueProd α β = { toFun := Prod.snd, invFun := fun (b : β) => (default, b), left_inv := ⋯, right_inv := ⋯, measurable_toFun := ⋯, measurable_invFun := ⋯ }

@[simp]

theorem MeasurableEquiv.uniqueProd_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Unique α] (p : α × β) : (uniqueProd α β) p = p.2

@[simp]

theorem MeasurableEquiv.uniqueProd_symm_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Unique α] (b : β) : (uniqueProd α β).symm b = (default, b)

def MeasurableEquiv.prodUnique (α : Type u_1) (β : Type u_2) [MeasurableSpace α] [MeasurableSpace β] [Unique β] : α × β ≃ᵐ α

The measurable equivalence α × β ≃ᵐ α when β has a unique element.

Equations

• MeasurableEquiv.prodUnique α β = { toFun := Prod.fst, invFun := fun (a : α) => (a, default), left_inv := ⋯, right_inv := ⋯, measurable_toFun := ⋯, measurable_invFun := ⋯ }

@[simp]

theorem MeasurableEquiv.prodUnique_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Unique β] (p : α × β) : (prodUnique α β) p = p.1

@[simp]

theorem MeasurableEquiv.prodUnique_symm_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Unique β] (a : α) : (prodUnique α β).symm a = (a, default)

def MeasurableEquiv.IicSuccProd (X : ℕ → Type u_2) [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ) : ((i : ↥(Finset.Iic (n + 1))) → X ↑i) ≃ᵐ ((i : ↥(Finset.Iic n)) → X ↑i) × X (n + 1)

Measurable equivalence between a product up to n + 1 and the pair of the product up to n and the space at n + 1.

Equations

• MeasurableEquiv.IicSuccProd X n = (MeasurableEquiv.IicProdIoc ⋯).symm.trans ((MeasurableEquiv.refl ((i : ↥(Finset.Iic n)) → X ↑i)).prodCongr (MeasurableEquiv.piSingleton n).symm)

theorem MeasurableEquiv.symm_IicSuccProd {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ) : (IicSuccProd X n).symm = ((refl ((i : ↥(Finset.Iic n)) → X ↑i)).prodCongr (piSingleton n)).trans (IicProdIoc ⋯)

@[simp]

theorem MeasurableEquiv.IicSuccProd_apply {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ) (h : (i : ↥(Finset.Iic (n + 1))) → X ↑i) : (IicSuccProd X n) h = (fun (i : ↥(Finset.Iic n)) => h ⟨↑i, ⋯⟩, h ⟨n + 1, ⋯⟩)

theorem MeasurableEquiv.coe_prodCongr {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (e₁ : α ≃ᵐ β) (e₂ : γ ≃ᵐ δ) : ⇑(e₁.prodCongr e₂) = Prod.map ⇑e₁ ⇑e₂

theorem MeasurableEquiv.coe_refl {α : Type u_2} {mα : MeasurableSpace α} : ⇑(refl α) = id

def MeasurableEquiv.finSuccPiIic (X : ℕ → Type u_2) [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ) : ((i : Fin (n + 1)) → X ↑i) ≃ᵐ ((i : ↥(Finset.Iic n)) → X ↑i)

Measurable equivalence between Π i : Fin (n + 1), X i and Π i : Iic n, X i.

Equations

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

@[simp]

theorem MeasurableEquiv.finSuccPiIic_apply {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ) (h : (i : Fin (n + 1)) → X ↑i) (i : ↥(Finset.Iic n)) : (finSuccPiIic X n) h i = h ⟨↑i, ⋯⟩

@[simp]

theorem MeasurableEquiv.finSuccPiIic_symm_apply {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ) (h : (i : ↥(Finset.Iic n)) → X ↑i) (i : Fin (n + 1)) : (finSuccPiIic X n).symm h i = h ⟨↑i, ⋯⟩

theorem MeasurableEquiv.finSuccPiIic_symm_comp_frestrictLe {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ) : ⇑(finSuccPiIic X n).symm ∘ Preorder.frestrictLe n = fun (x : (i : ℕ) → X i) (i : Fin (n + 1)) => x ↑i

def MeasurableEquiv.finSuccProd (X : Type u_2) [MeasurableSpace X] (n : ℕ) : (Fin (n + 1) → X) ≃ᵐ (Fin n → X) × X

Measurable equivalence between Fin (n + 1) → X and (Fin n → X) × X.

Equations

• MeasurableEquiv.finSuccProd X n = (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) => X) (Fin.last n)).trans MeasurableEquiv.prodComm

@[simp]

theorem MeasurableEquiv.finSuccProd_apply {X : Type u_2} [MeasurableSpace X] (n : ℕ) (h : Fin (n + 1) → X) : (finSuccProd X n) h = (fun (i : Fin n) => h i.castSucc, h (Fin.last n))

@[simp]

theorem MeasurableEquiv.finSuccProd_symm_apply {X : Type u_2} [MeasurableSpace X] (n : ℕ) (p : (Fin n → X) × X) : (finSuccProd X n).symm p = Fin.snoc p.1 p.2