LeanMachineLearning

4.3. Tactic.EqLift.Kernel.Lift🔗

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.

Module LeanMachineLearning.Tactic.EqLift.Kernel.Lift contains 16 exposed declarations.