[Merged by Bors] - feat(Probability/Kernel): Kernel.sectL and sectR

[LorenzoLuccioli]

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.

---

[github-actions]

PR summary 3c46787a4d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ _root_.ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR
+ comap_sectL
+ comap_sectR
+ instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (sectL κ b)] :
+ instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (sectR κ b)] :
+ instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((sectL κ b) a) := by
+ instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((sectR κ a) b) := by
+ instance (κ : Kernel (α × β) γ) (a : α) [IsFiniteKernel κ] : IsFiniteKernel (sectR κ a) := by
+ instance (κ : Kernel (α × β) γ) (a : α) [IsMarkovKernel κ] : IsMarkovKernel (sectR κ a) := by
+ instance (κ : Kernel (α × β) γ) (a : α) [IsSFiniteKernel κ] : IsSFiniteKernel (sectR κ a) := by
+ instance (κ : Kernel (α × β) γ) (a : α) [IsZeroOrMarkovKernel κ] :
+ instance (κ : Kernel (α × β) γ) (b : β) [IsFiniteKernel κ] : IsFiniteKernel (sectL κ b) := by
+ instance (κ : Kernel (α × β) γ) (b : β) [IsMarkovKernel κ] : IsMarkovKernel (sectL κ b) := by
+ instance (κ : Kernel (α × β) γ) (b : β) [IsSFiniteKernel κ] : IsSFiniteKernel (sectL κ b) := by
+ instance (κ : Kernel (α × β) γ) (b : β) [IsZeroOrMarkovKernel κ] :
+ sectL
+ sectL_apply
+ sectL_prodMkLeft
+ sectL_prodMkRight
+ sectL_swapRight
+ sectL_zero
+ sectR
+ sectR_apply
+ sectR_prodMkLeft
+ sectR_prodMkRight
+ sectR_swapRight
+ sectR_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[LorenzoLuccioli]

The names are Kernel.fst' and Kernel.snd', since Kernel.fst and Kernel.snd are already taken for the case where the codomain is a product space. Suggestions for a better name are welcome.

[urkud]

About names: there are Function.Embedding.sectl and MonoidHom.inl. Probably, the former is closer to this case. Also, please ask on Zulip for other suggestions.

[YaelDillies]

Can you please update the PR description?

[YaelDillies]

Thanks! 🚀

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[YaelDillies]

Looks like this is ready to be merged again?

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[RemyDegenne]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style