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.

@[instance_reducible]

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

Equations

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

@[reducible]

def MeasurableCoherence.TransEquiv {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] [mXY : MeasurableCoherence X Y] {X' : Type u_3} {Y' : Type u_4} [MeasurableSpace X'] [MeasurableSpace Y'] (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) : MeasurableCoherence X' Y'

Given measurable equivalences ex : X ≃ᵐ X' and ey : Y ≃ᵐ Y', we can transport the MeasurableCoherence instance from X and Y to X' and Y'.

Equations

• MeasurableCoherence.TransEquiv ex ey = { miso := ex.trans (MeasurableCoherence.miso.trans ey.symm) }

@[reducible]

noncomputable def MeasurableCoherence.monoidalCoherence {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] [mXY : MeasurableCoherence X Y] {SX SY : SFinKer} (ex : SX.carrier ≃ᵐ X) (ey : SY.carrier ≃ᵐ Y) : CategoryTheory.MonoidalCoherence SX SY

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 u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [MeasurableSpace W] [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] {SW SX SY SZ : SFinKer} (ew : SW.carrier ≃ᵐ W) (ex : SX.carrier ≃ᵐ X) (ey : SY.carrier ≃ᵐ Y) (ez : SZ.carrier ≃ᵐ 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. It uses arbitrary measurable equivalences to transport the kernels to the SFinKer category.

Equations

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

instance ProbabilityTheory.Kernel.monoComp'_sfinite {W : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [MeasurableSpace W] [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] {SW SX SY SZ : SFinKer} (ew : SW.carrier ≃ᵐ W) (ex : SX.carrier ≃ᵐ X) (ey : SY.carrier ≃ᵐ Y) (ez : SZ.carrier ≃ᵐ Z) [MeasurableCoherence X Y] (κ : Kernel W X) [IsSFiniteKernel κ] (η : Kernel Y Z) [IsSFiniteKernel η] : IsSFiniteKernel (monoComp₀ ew ex ey ez κ η)

@[reducible, inline]

noncomputable abbrev ProbabilityTheory.Kernel.monoComp {W : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [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 η = ProbabilityTheory.Kernel.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.