Commit 2025-01-07 16:45 01e66383

View on Github →

feat(Probability/Kernel): Kernel.sectL and sectR (#15466) Define a Kernel α γ and a Kernel β γ from a Kernel (α × β) γ by taking the comap of fun a ↦ (a, b) and fun b ↦ (a, b) respectively.

  • Add definitions of Kernel.sectL and Kernel.sectR.
  • Add some API lemmas: sectL_apply, sectL_zero, comap_sectL, sectL_prodMkLeft, sectL_prodMkRight and the equivalent lemmas for sectR.
  • Add instances for IsMarkovKernel, IsFiniteKernel, IsSFiniteKernel and NeZero.
  • Add sectL_swapRight and sectR_swapRight.
  • Add compProd_apply_eq_compProd_sectR.

Estimated changes