Kernel Lift

This file defines the lift operation on kernels, which allows to cast kernels to different types in the same universe level, as long as there are measurable equivalences between the types.

Main declarations

• Kernel.lift: the main definition of the lift operation.
• Kernel.isSFinite_lift: a kernel is s-finite if and only if its lift is s-finite.
• Kernel.lift_congr: two kernels are equal if and only if their lifts are equal.
• Kernel.lift_comp: the lift of a composition is the composition of the lifts.
• Kernel.parallelComp_lift: the lift of a parallel composition is the parallel composition of the lifts.
• Kernel.prod_lift: the lift of a product is the product of the lifts.

noncomputable def ProbabilityTheory.Kernel.lift {X : Type x} [MeasurableSpace X] {Y : Type y} [MeasurableSpace Y] {X' : Type w} [MeasurableSpace X'] {Y' : Type w} [MeasurableSpace Y'] {ex : X' ≃ᵐ X} {ey : Y' ≃ᵐ Y} (κ : Kernel X Y) : Kernel X' Y'

Cast a kernel to different types in the same universe level, using measurable equivalences.

Equations

• κ.lift = (κ.map ⇑ey.symm).comap ⇑ex ⋯

theorem ProbabilityTheory.Kernel.lift_apply {X : Type x} [MeasurableSpace X] {Y : Type y} [MeasurableSpace Y] {X' : Type w} [MeasurableSpace X'] {Y' : Type w} [MeasurableSpace Y'] (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) (κ : Kernel X Y) (a : X') : κ.lift a = (κ.map ⇑ey.symm) (ex a)

theorem ProbabilityTheory.Kernel.lift_apply' {X : Type x} [MeasurableSpace X] {Y : Type y} [MeasurableSpace Y] {X' : Type w} [MeasurableSpace X'] {Y' : Type w} [MeasurableSpace Y'] (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) (κ : Kernel X Y) (a : X') {s : Set Y'} (hs : MeasurableSet s) : (κ.lift a) s = (κ (ex a)) (⇑ey '' s)

theorem ProbabilityTheory.Kernel.isSFinite_lift {X : Type x} [MeasurableSpace X] {Y : Type y} [MeasurableSpace Y] {X' : Type w} [MeasurableSpace X'] {Y' : Type w} [MeasurableSpace Y'] (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) (κ : Kernel X Y) : IsSFiniteKernel κ ↔ IsSFiniteKernel κ.lift

instance ProbabilityTheory.Kernel.instIsSFiniteKernelLift {X : Type x} [MeasurableSpace X] {Y : Type y} [MeasurableSpace Y] {X' : Type w} [MeasurableSpace X'] {Y' : Type w} [MeasurableSpace Y'] (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) (κ : Kernel X Y) [IsSFiniteKernel κ] : IsSFiniteKernel κ.lift

instance ProbabilityTheory.Kernel.instIsMarkovKernelLift {X : Type x} [MeasurableSpace X] {Y : Type y} [MeasurableSpace Y] {X' : Type w} [MeasurableSpace X'] {Y' : Type w} [MeasurableSpace Y'] (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) (κ : Kernel X Y) [IsMarkovKernel κ] : IsMarkovKernel κ.lift

theorem ProbabilityTheory.Kernel.lift_congr {X : Type x} [MeasurableSpace X] {Y : Type y} [MeasurableSpace Y] {X' : Type w} [MeasurableSpace X'] {Y' : Type w} [MeasurableSpace Y'] (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) (κ η : Kernel X Y) : κ = η ↔ κ.lift = η.lift

theorem ProbabilityTheory.Kernel.comp_lift {X : Type x} [MeasurableSpace X] {Y : Type y} [MeasurableSpace Y] {X' : Type w} [MeasurableSpace X'] {Y' : Type w} [MeasurableSpace Y'] (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) {Z : Type z} [MeasurableSpace Z] {Z' : Type w} [MeasurableSpace Z'] (ez : Z' ≃ᵐ Z) (η : Kernel X Y) (κ : Kernel Z X) : η.lift.comp κ.lift = (η.comp κ).lift

theorem ProbabilityTheory.Kernel.parallelComp_lift {X : Type x} [MeasurableSpace X] {Y : Type y} [MeasurableSpace Y] {X' : Type w} [MeasurableSpace X'] {Y' : Type w} [MeasurableSpace Y'] (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) {Z : Type z} [MeasurableSpace Z] {T : Type t} [MeasurableSpace T] {Z' : Type w} [MeasurableSpace Z'] {T' : Type w} [MeasurableSpace T'] (ez : Z' ≃ᵐ Z) (et : T' ≃ᵐ T) (κ : Kernel X Y) (η : Kernel Z T) : κ.lift.parallelComp η.lift = (κ.parallelComp η).lift

theorem ProbabilityTheory.Kernel.id_lift {X : Type x} [MeasurableSpace X] {X' : Type w} [MeasurableSpace X'] (ex : X' ≃ᵐ X) : Kernel.id = Kernel.id.lift

theorem ProbabilityTheory.Kernel.discard_lift {X : Type x} [MeasurableSpace X] {X' : Type w} [MeasurableSpace X'] (ex : X' ≃ᵐ X) : discard X' = (discard X).lift

theorem ProbabilityTheory.Kernel.copy_lift {X : Type x} [MeasurableSpace X] {X' : Type w} [MeasurableSpace X'] (ex : X' ≃ᵐ X) : copy X' = (copy X).lift

theorem ProbabilityTheory.Kernel.swap_lift {X : Type x} [MeasurableSpace X] {Y : Type y} [MeasurableSpace Y] {X' : Type w} [MeasurableSpace X'] {Y' : Type w} [MeasurableSpace Y'] (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) : swap X' Y' = (swap X Y).lift

theorem ProbabilityTheory.Kernel.prod_lift {X : Type x} [MeasurableSpace X] {Y : Type y} [MeasurableSpace Y] {X' : Type w} [MeasurableSpace X'] {Y' : Type w} [MeasurableSpace Y'] (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) {Z : Type z} [MeasurableSpace Z] {Z' : Type w} [MeasurableSpace Z'] (ez : Z' ≃ᵐ Z) (κ : Kernel X Y) (η : Kernel X Z) : κ.lift.prod η.lift = (κ.prod η).lift

theorem ProbabilityTheory.Kernel.compProd_lift {X : Type x} [MeasurableSpace X] {Y : Type y} [MeasurableSpace Y] {X' : Type w} [MeasurableSpace X'] {Y' : Type w} [MeasurableSpace Y'] (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) {Z : Type z} [MeasurableSpace Z] {Z' : Type w} [MeasurableSpace Z'] (ez : Z' ≃ᵐ Z) (κ : Kernel X Y) (η : Kernel (X × Y) Z) : κ.lift.compProd η.lift = (κ.compProd η).lift

instance ProbabilityTheory.Kernel.instIsDeterministicLift {X : Type x} [MeasurableSpace X] {Y : Type y} [MeasurableSpace Y] {X' : Type w} [MeasurableSpace X'] {Y' : Type w} [MeasurableSpace Y'] (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y) {κ : Kernel X Y} [IsDeterministic κ] : IsDeterministic κ.lift