Kernel lifting utilities

This file provides helper functions for lifting and unlifting kernel expressions: type extraction, construction of measurable equivalences, and explicit constructors for kernel operations and Kernel.lift. The constructors build the applications directly (mkAppN with explicit universe levels and instances) instead of going through mkAppM, whose unification is the main cost of the transformations.

Main declarations

• Carrier: a measurable space X : Type u, given by the expression X and the level u.
• getTypesFromKernel: extracts carrier types and universe levels from kernel expressions.
• constructMeasurableEquiv: recursively builds measurable equivalences.
• getOriginalType: retrieves the original type from a lifted type.
• mkKernelComp, mkKernelParallelComp, ..., mkKernelLift: explicit constructors.

structure Carrier : Type

A measurable space: the carrier type and its universe level.

• type : Lean.Expr

  The carrier type.

• lvl : Lean.Level

  The universe level of the carrier type.

def Carrier.inst (c : Carrier) : Lean.MetaM Lean.Expr

The MeasurableSpace instance of a carrier (cached).

Equations

• c.inst = synthInstanceCached (Lean.mkApp (Lean.mkConst `MeasurableSpace [c.lvl]) c.type)

def getTypesFromKernel (κ : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr × Lean.Level × Lean.Level)

Extract (X, Y, u, v) from an expression of type Kernel X Y.

Equations

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

def getCarriersFromKernel (κ : Lean.Expr) : Lean.MetaM (Carrier × Carrier)

Extract the source and target carriers of a kernel.

Equations

• getCarriersFromKernel κ = do let __x ← getTypesFromKernel κ match __x with | (X, Y, xLvl, yLvl) => pure ({ type := X, lvl := xLvl }, { type := Y, lvl := yLvl })

partial def constructMeasurableEquiv (e : Lean.Expr) (eLevel maxLvl : Lean.Level) : Lean.MetaM (Lean.Expr × Lean.Expr)

Build the measurable equivalence X' ≃ᵐ X between the lift X' of e to the universe maxLvl and e itself, recursively on products. Returns the equivalence and X'.

def Carrier.lift (c : Carrier) (maxLvl : Lean.Level) : Lean.MetaM (Lean.Expr × Carrier)

Same as constructMeasurableEquiv, for a carrier.

Equations

• c.lift maxLvl = do let __x ← constructMeasurableEquiv c.type c.lvl maxLvl match __x with | (equiv, c') => pure (equiv, { type := c', lvl := maxLvl })

partial def getOriginalType (t : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Level)

Get the original type from a lifted type.

Explicit constructors

def mkKernelComp (X Y Z : Carrier) (η κ : Lean.Expr) : Lean.MetaM Lean.Expr

η ∘ₖ κ with κ : Kernel X Y and η : Kernel Y Z.

Equations

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

def mkKernelParallelComp (X Y Z T : Carrier) (κ η : Lean.Expr) : Lean.MetaM Lean.Expr

κ ∥ₖ η with κ : Kernel X Y and η : Kernel Z T.

Equations

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

def mkKernelProd (X Y Z : Carrier) (κ η : Lean.Expr) : Lean.MetaM Lean.Expr

κ ×ₖ η with κ : Kernel X Y and η : Kernel X Z.

Equations

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

def mkKernelCompProd (X Y Z : Carrier) (κ η : Lean.Expr) : Lean.MetaM Lean.Expr

κ ⊗ₖ η with κ : Kernel X Y and η : Kernel (X × Y) Z.

Equations

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

def mkKernelId (X : Carrier) : Lean.MetaM Lean.Expr

Kernel.id : Kernel X X.

Equations

• mkKernelId X = do let __do_lift ← X.inst pure (Lean.mkAppN (Lean.mkConst `ProbabilityTheory.Kernel.id [X.lvl]) #[X.type, __do_lift])

def mkKernelCopy (X : Carrier) : Lean.MetaM Lean.Expr

Kernel.copy X.

Equations

• mkKernelCopy X = do let __do_lift ← X.inst pure (Lean.mkAppN (Lean.mkConst `ProbabilityTheory.Kernel.copy [X.lvl]) #[X.type, __do_lift])

def mkKernelDiscard (X : Carrier) (punitLvl : Lean.Level) : Lean.MetaM Lean.Expr

Kernel.discard X : Kernel X PUnit.{punitLvl + 1}.

Equations

• mkKernelDiscard X punitLvl = do let __do_lift ← X.inst pure (Lean.mkAppN (Lean.mkConst `ProbabilityTheory.Kernel.discard [X.lvl, punitLvl]) #[X.type, __do_lift])

def mkKernelSwap (X Y : Carrier) : Lean.MetaM Lean.Expr

Kernel.swap X Y.

Equations

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

def mkKernelLift (X Y X' Y' : Carrier) (ex ey κ : Lean.Expr) : Lean.MetaM Lean.Expr

κ.lift (ex := ex) (ey := ey) : Kernel X' Y' with κ : Kernel X Y.

Equations

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