|
| 1 | +/- |
| 2 | +Copyright (c) 2024 Rémy Degenne. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Rémy Degenne, Lorenzo Luccioli |
| 5 | +-/ |
| 6 | +import Mathlib.Probability.Kernel.Composition.Basic |
| 7 | + |
| 8 | +/-! |
| 9 | +
|
| 10 | +# Parallel composition of kernels |
| 11 | +
|
| 12 | +Two kernels `κ : Kernel α β` and `η : Kernel γ δ` can be applied in parallel to give a kernel |
| 13 | +`κ ∥ₖ η` from `α × γ` to `β × δ`: `(κ ∥ₖ η) (a, c) = (κ a).prod (η c)`. |
| 14 | +
|
| 15 | +## Main definitions |
| 16 | +
|
| 17 | +* `parallelComp (κ : Kernel α β) (η : Kernel γ δ) : Kernel (α × γ) (β × δ)`: parallel composition |
| 18 | + of two s-finite kernels. We define a notation `κ ∥ₖ η = parallelComp κ η`. |
| 19 | + `∫⁻ bd, g bd ∂(κ ∥ₖ η) ac = ∫⁻ b, ∫⁻ d, g (b, d) ∂η ac.2 ∂κ ac.1` |
| 20 | +
|
| 21 | +## Main statements |
| 22 | +
|
| 23 | +* `parallelComp_comp_copy`: `(κ ∥ₖ η) ∘ₖ (copy α) = κ ×ₖ η` |
| 24 | +* `deterministic_comp_copy`: for a deterministic kernel, copying then applying the kernel to |
| 25 | + the two copies is the same as first applying the kernel then copying. That is, if `κ` is |
| 26 | + a deterministic kernel, `(κ ∥ₖ κ) ∘ₖ copy α = copy β ∘ₖ κ`. |
| 27 | +
|
| 28 | +## Notations |
| 29 | +
|
| 30 | +* `κ ∥ₖ η = ProbabilityTheory.Kernel.parallelComp κ η` |
| 31 | +
|
| 32 | +## Implementation notes |
| 33 | +
|
| 34 | +Our formalization of kernels is centered around the composition-product: the product and then the |
| 35 | +parallel composition are defined as special cases of the composition-product. |
| 36 | +We could have alternatively used the building blocks of kernels seen as a Markov category: |
| 37 | +composition, parallel composition (or tensor product) and the deterministic kernels `id`, `copy`, |
| 38 | +`swap` and `discard`. The product and composition-product could then be built from these. |
| 39 | +
|
| 40 | +-/ |
| 41 | + |
| 42 | +open MeasureTheory |
| 43 | + |
| 44 | +open scoped ENNReal |
| 45 | + |
| 46 | +namespace ProbabilityTheory.Kernel |
| 47 | + |
| 48 | +variable {α β γ δ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} |
| 49 | + {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} |
| 50 | + |
| 51 | +section ParallelComp |
| 52 | + |
| 53 | +/-- Parallel product of two kernels. -/ |
| 54 | +noncomputable |
| 55 | +def parallelComp (κ : Kernel α β) (η : Kernel γ δ) : Kernel (α × γ) (β × δ) := |
| 56 | + (prodMkRight γ κ) ×ₖ (prodMkLeft α η) |
| 57 | + |
| 58 | +@[inherit_doc] |
| 59 | +scoped[ProbabilityTheory] infixl:100 " ∥ₖ " => ProbabilityTheory.Kernel.parallelComp |
| 60 | + |
| 61 | +lemma parallelComp_apply (κ : Kernel α β) [IsSFiniteKernel κ] |
| 62 | + (η : Kernel γ δ) [IsSFiniteKernel η] (x : α × γ) : |
| 63 | + (κ ∥ₖ η) x = (κ x.1).prod (η x.2) := by |
| 64 | + rw [parallelComp, prod_apply, prodMkRight_apply, prodMkLeft_apply] |
| 65 | + |
| 66 | +lemma lintegral_parallelComp (κ : Kernel α β) [IsSFiniteKernel κ] |
| 67 | + (η : Kernel γ δ) [IsSFiniteKernel η] |
| 68 | + (ac : α × γ) {g : β × δ → ℝ≥0∞} (hg : Measurable g) : |
| 69 | + ∫⁻ bd, g bd ∂(κ ∥ₖ η) ac = ∫⁻ b, ∫⁻ d, g (b, d) ∂η ac.2 ∂κ ac.1 := by |
| 70 | + rw [parallelComp, lintegral_prod _ _ _ hg] |
| 71 | + simp |
| 72 | + |
| 73 | +instance (κ : Kernel α β) (η : Kernel γ δ) : IsSFiniteKernel (κ ∥ₖ η) := by |
| 74 | + rw [parallelComp]; infer_instance |
| 75 | + |
| 76 | +instance (κ : Kernel α β) [IsFiniteKernel κ] (η : Kernel γ δ) [IsFiniteKernel η] : |
| 77 | + IsFiniteKernel (κ ∥ₖ η) := by |
| 78 | + rw [parallelComp]; infer_instance |
| 79 | + |
| 80 | +instance (κ : Kernel α β) [IsMarkovKernel κ] (η : Kernel γ δ) [IsMarkovKernel η] : |
| 81 | + IsMarkovKernel (κ ∥ₖ η) := by |
| 82 | + rw [parallelComp]; infer_instance |
| 83 | + |
| 84 | +instance (κ : Kernel α β) [IsZeroOrMarkovKernel κ] (η : Kernel γ δ) [IsZeroOrMarkovKernel η] : |
| 85 | + IsZeroOrMarkovKernel (κ ∥ₖ η) := by |
| 86 | + rw [parallelComp]; infer_instance |
| 87 | + |
| 88 | +lemma parallelComp_comp_copy (κ : Kernel α β) [IsSFiniteKernel κ] |
| 89 | + (η : Kernel α γ) [IsSFiniteKernel η] : |
| 90 | + (κ ∥ₖ η) ∘ₖ (copy α) = κ ×ₖ η := by |
| 91 | + ext a s hs |
| 92 | + simp_rw [prod_apply, comp_apply, copy_apply, Measure.bind_apply hs (Kernel.measurable _)] |
| 93 | + rw [lintegral_dirac'] |
| 94 | + swap; · exact Kernel.measurable_coe _ hs |
| 95 | + rw [parallelComp_apply] |
| 96 | + |
| 97 | +lemma swap_parallelComp {κ : Kernel α β} [IsSFiniteKernel κ] |
| 98 | + {η : Kernel γ δ} [IsSFiniteKernel η] : |
| 99 | + (swap β δ) ∘ₖ (κ ∥ₖ η) = (η ∥ₖ κ) ∘ₖ (swap α γ) := by |
| 100 | + rw [parallelComp, swap_prod, parallelComp] |
| 101 | + ext ac s hs |
| 102 | + rw [comp_apply, swap_apply, Measure.bind_apply hs (Kernel.measurable _), |
| 103 | + lintegral_dirac' _ (Kernel.measurable_coe _ hs), prod_apply, prod_apply, prodMkLeft_apply, |
| 104 | + prodMkLeft_apply, prodMkRight_apply, prodMkRight_apply] |
| 105 | + rfl |
| 106 | + |
| 107 | +/-- For a deterministic kernel, copying then applying the kernel to the two copies is the same |
| 108 | +as first applying the kernel then copying. -/ |
| 109 | +lemma deterministic_comp_copy {f : α → β} (hf : Measurable f) : |
| 110 | + (Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) ∘ₖ Kernel.copy α |
| 111 | + = Kernel.copy β ∘ₖ Kernel.deterministic f hf := by |
| 112 | + rw [Kernel.parallelComp_comp_copy, Kernel.deterministic_prod_deterministic, |
| 113 | + Kernel.copy, Kernel.deterministic_comp_deterministic] |
| 114 | + rfl |
| 115 | + |
| 116 | +end ParallelComp |
| 117 | + |
| 118 | +end ProbabilityTheory.Kernel |
0 commit comments