Measurable coherence

This file introduces the monoidal composition for s-finite kernels (noted ⊗≫ₖ).

Main declarations

• MeasurableCoherence: class witnessing measurable equivalences between types.
• monoComp: monoidal composition of kernels using measurable equivalences to transport to SFinKer.
• hom_monoComp: the SFinKer morphism of the kernelized monoidal composition is the monoidal composition of the morphisms in SFinKer.

class MeasurableCoherence (X : Type u_1) (Y : Type u_2) [MeasurableSpace X] [MeasurableSpace Y] : Type (max u_1 u_2)

A class witnessing the existence of a measurable equivalence between two measurable spaces.

• miso : X ≃ᵐ Y

  A measurable equivalence between X and Y.

@[implicit_reducible]

instance MeasurableCoherence.inst {X : Type x} [MeasurableSpace X] : MeasurableCoherence X X

Equations

• MeasurableCoherence.inst = { miso := MeasurableEquiv.refl X }

@[reducible]

noncomputable def MeasurableCoherence.monoidalCoherence {X : Type x} {Y : Type y} [MeasurableSpace X] [MeasurableSpace Y] [mXY : MeasurableCoherence X Y] {X' Y' : Type w} [MeasurableSpace X'] [MeasurableSpace Y'] (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) : CategoryTheory.MonoidalCoherence { carrier := X', str := inst✝ } { carrier := Y', str := inst✝¹ }

MeasurableCoherence gives an instance of MonoidalCoherence in the SFinKer category.

Equations

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

noncomputable def ProbabilityTheory.Kernel.monoComp₀ {W : Type w} {X : Type x} {Y : Type y} {Z : Type z} [MeasurableSpace W] [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] [MeasurableCoherence X Y] (κ : Kernel W X) [IsSFiniteKernel κ] (η : Kernel Y Z) [IsSFiniteKernel η] {W' X' Y' Z' : Type (max w x y z)} [MeasurableSpace W'] [MeasurableSpace X'] [MeasurableSpace Y'] [MeasurableSpace Z'] (ew : W' ≃ᵐ W) (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) (ez : Z' ≃ᵐ Z) : Kernel W Z

The kernelized version of the monoidal composition of kernels using the SFinKer category. It uses arbitrary measurable equivalences to transport the kernels to the SFinKer category.

Equations

• κ.monoComp₀ η ew ex ey ez = ProbabilityTheory.Kernel.fromHom (CategoryTheory.monoidalComp κ.hom η.hom)

instance ProbabilityTheory.Kernel.monoComp'_sfinite {W : Type w} {X : Type x} {Y : Type y} {Z : Type z} [MeasurableSpace W] [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] [MeasurableCoherence X Y] (κ : Kernel W X) [IsSFiniteKernel κ] (η : Kernel Y Z) [IsSFiniteKernel η] {W' X' Y' Z' : Type (max w x y z)} [MeasurableSpace W'] [MeasurableSpace X'] [MeasurableSpace Y'] [MeasurableSpace Z'] (ew : W' ≃ᵐ W) (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) (ez : Z' ≃ᵐ Z) : IsSFiniteKernel (κ.monoComp₀ η ew ex ey ez)

@[reducible, inline]

noncomputable abbrev ProbabilityTheory.Kernel.monoComp {W : Type w} {X : Type x} {Y : Type y} {Z : Type z} [MeasurableSpace W] [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] [MeasurableCoherence X Y] (κ : Kernel W X) [IsSFiniteKernel κ] (η : Kernel Y Z) [IsSFiniteKernel η] : Kernel W Z

The kernelized version of the monoidal composition of kernels using the SFinKer category.

Equations

• κ.monoComp η = κ.monoComp₀ η MeasurableEquiv.ulift MeasurableEquiv.ulift MeasurableEquiv.ulift MeasurableEquiv.ulift

def ProbabilityTheory.«term_⊗≫ₖ_» : Lean.TrailingParserDescr

The kernelized version of the monoidal composition of kernels using the SFinKer category.

Equations

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

instance ProbabilityTheory.Kernel.monoComp_sfinite {W : Type w} {X : Type x} {Y : Type y} {Z : Type z} [MeasurableSpace W] [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] [MeasurableCoherence X Y] (κ : Kernel W X) [IsSFiniteKernel κ] (η : Kernel Y Z) [IsSFiniteKernel η] : IsSFiniteKernel (κ.monoComp η)

theorem ProbabilityTheory.Kernel.hom_monoComp {W : Type w} {X : Type x} {Y : Type y} {Z : Type z} [MeasurableSpace W] [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] [MeasurableCoherence X Y] (κ : Kernel W X) [IsSFiniteKernel κ] (η : Kernel Y Z) [IsSFiniteKernel η] {W'' X'' Y'' Z'' : Type (max v w x y z)} [MeasurableSpace W''] [MeasurableSpace X''] [MeasurableSpace Y''] [MeasurableSpace Z''] (ew' : W'' ≃ᵐ W) (ex' : X'' ≃ᵐ X) (ey' : Y'' ≃ᵐ Y) (ez' : Z'' ≃ᵐ Z) : CategoryTheory.monoidalComp κ.hom η.hom = (κ.monoComp η).hom