Repository navigation
Expand file tree
/
Copy pathExamples.lean
More file actions
85 lines (63 loc) · 3.38 KB
/
Copy pathExamples.lean
File metadata and controls
85 lines (63 loc) · 3.38 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
/-
Copyright (c) 2026 Gaëtan Serré. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gaëtan Serré
-/
module
public import KernelHom
/-!
# Structural lemmas of Mathlib
Lemmas of `Mathlib.Probability.Kernel.Composition` that are equalities of kernels built only from
composition, parallel composition, product, identity, copy and swap, and that are not used to build
the category `SFinKer`. The other lemmas of this kind, such as `Kernel.comp_assoc` or
`Kernel.swap_parallelComp`, are used to prove the axioms of `SFinKer`, so their proofs with
Kernel-Hom could not replace the ones of Mathlib. Each lemma has the name of its Mathlib
counterpart, suffixed by `₀`.
The file also contains `parallelComp_self_comp_copy₀`, from
`Mathlib.Probability.Kernel.Deterministic`, which shows that the properties of deterministic kernels
are available after translation.
They are all proved by a single call to `kernel_monoidal` or `kernel_disch`, which also handles the
exchange law (`parallelComp_comm₀`) and the coassociativity of copy (`prodAssoc_prod₀`).
`Kernel.map` is not translated, so `map_prod_swap₀` and `prodAssoc_prod₀` are first rewritten with
`swap_comp_eq_map` and `deterministic_comp_eq_map`. As in Mathlib, `parallelComp_comm₀` holds for
any kernels, and the case of a non s-finite kernel is closed by `simp`.
-/
@[expose] public section
open MeasureTheory ProbabilityTheory CategoryTheory MonoidalCategory
open scoped KernelHom
show_panel_widgets [local KernelDiagram]
variable {X Y Z T Y' Z' : Type*} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z]
[MeasurableSpace T] [MeasurableSpace Y'] [MeasurableSpace Z']
namespace ProbabilityTheory.Kernel
/-! ### `Mathlib.Probability.Kernel.Composition.Prod` -/
lemma map_prod_swap₀ (κ : Kernel X Y) (η : Kernel X Z) [IsSFiniteKernel κ] [IsSFiniteKernel η] :
map (κ ×ₖ η) Prod.swap = η ×ₖ κ := by
rw [← swap_comp_eq_map]
kernel_disch
lemma swap_prod₀ {κ : Kernel X Y} [IsSFiniteKernel κ] {η : Kernel X Z} [IsSFiniteKernel η] :
swap Y Z ∘ₖ (κ ×ₖ η) = η ×ₖ κ := by
kernel_disch
lemma prodAssoc_prod₀ (κ : Kernel X Y) [IsSFiniteKernel κ] (η : Kernel X Z) [IsSFiniteKernel η]
(ξ : Kernel X T) [IsSFiniteKernel ξ] :
((κ ×ₖ ξ) ×ₖ η).map MeasurableEquiv.prodAssoc = κ ×ₖ (ξ ×ₖ η) := by
rw [← deterministic_comp_eq_map (MeasurableEquiv.measurable _)]
kernel_disch
/-! ### `Mathlib.Probability.Kernel.Composition.KernelLemmas` -/
lemma parallelComp_comp_prod₀ {κ : Kernel X Y} [IsSFiniteKernel κ] {η : Kernel Y Z}
[IsSFiniteKernel η] {κ' : Kernel X Y'} [IsSFiniteKernel κ'] {η' : Kernel Y' Z'}
[IsSFiniteKernel η'] :
(η ∥ₖ η') ∘ₖ (κ ×ₖ κ') = (η ∘ₖ κ) ×ₖ (η' ∘ₖ κ') := by
kernel_monoidal
lemma parallelComp_comm₀ {κ : Kernel X Y} {η : Kernel Z T} :
(Kernel.id ∥ₖ κ) ∘ₖ (η ∥ₖ Kernel.id) = (η ∥ₖ Kernel.id) ∘ₖ (Kernel.id ∥ₖ κ) := by
by_cases hκ : IsSFiniteKernel κ
swap; · simp [hκ]
by_cases hη : IsSFiniteKernel η
swap; · simp [hη]
kernel_disch
/-! ### `Mathlib.Probability.Kernel.Deterministic` -/
lemma parallelComp_self_comp_copy₀ (κ : Kernel (X × Y) Z) [IsMarkovKernel κ]
[IsDeterministic κ] :
(κ ∥ₖ κ) ∘ₖ copy (X × Y) = copy Z ∘ₖ κ := by
kernel_disch
end ProbabilityTheory.Kernel