7.8. モナド則
補題.
x を \delta_x に送る写像 \delta : X \to \Measure(X) は可測である。
Lean code
theorem Measure.dirac_measurable : Measurable (Measure.dirac : X → Measure X) := X:Type u_1inst✝:MeasurableSpace X⊢ Measurable dirac
intro A X:Type u_1inst✝:MeasurableSpace XA:Set (Measure X)hA:MeasurableSet A⊢ MeasurableSet (dirac ⁻¹' A)
induction hA with
X:Type u_1inst✝:MeasurableSpace XA✝:Set (Measure X)A:Set (Measure X)hA:A ∈ MeasurableGen X⊢ MeasurableSet (dirac ⁻¹' A)
X:Type u_1inst✝:MeasurableSpace XA✝:Set (Measure X)A:Set XhA:MeasurableSet AB:Set ℝ≥0∞hB:MeasurableSet B⊢ MeasurableSet (dirac ⁻¹' {μ | μ A ∈ B})
X:Type u_1inst✝:MeasurableSpace XA✝:Set (Measure X)A:Set XhA:MeasurableSet AB:Set ℝ≥0∞hB:MeasurableSet Bthis:MeasurableSet ((A.indicator fun x => 1) ⁻¹' B) := Measurable.indicator measurable_const hA hB⊢ MeasurableSet (dirac ⁻¹' {μ | μ A ∈ B})
X:Type u_1inst✝:MeasurableSpace XA✝:Set (Measure X)A:Set XhA:MeasurableSet AB:Set ℝ≥0∞hB:MeasurableSet Bthis:MeasurableSet ((A.indicator fun x => 1) ⁻¹' B) := Measurable.indicator measurable_const hA hB⊢ (A.indicator fun x => 1) ⁻¹' B = dirac ⁻¹' {μ | μ A ∈ B}
X:Type u_1inst✝:MeasurableSpace XA✝:Set (Measure X)A:Set XhA:MeasurableSet AB:Set ℝ≥0∞hB:MeasurableSet Bthis:MeasurableSet ((A.indicator fun x => 1) ⁻¹' B) := Measurable.indicator measurable_const hA hB⊢ (A.indicator fun x => 1) ⁻¹' B = {a | A.indicator (fun x => 1) a ∈ B}
All goals completed! 🐙
X:Type u_1inst✝:MeasurableSpace XA:Set (Measure X)⊢ MeasurableSet (dirac ⁻¹' ∅) All goals completed! 🐙
X:Type u_1inst✝:MeasurableSpace XA✝:Set (Measure X)A:Set (Measure X)hA:MeasurableSpace.GenerateMeasurable (MeasurableGen X) Aih:MeasurableSet (dirac ⁻¹' A)⊢ MeasurableSet (dirac ⁻¹' Aᶜ)
X:Type u_1inst✝:MeasurableSpace XA✝:Set (Measure X)A:Set (Measure X)hA:MeasurableSpace.GenerateMeasurable (MeasurableGen X) Aih:MeasurableSet (dirac ⁻¹' A)⊢ MeasurableSet (dirac ⁻¹' A)ᶜ
All goals completed! 🐙
X:Type u_1inst✝:MeasurableSpace XA✝:Set (Measure X)A:ℕ → Set (Measure X)hA:∀ (n : ℕ), MeasurableSpace.GenerateMeasurable (MeasurableGen X) (A n)ih:∀ (n : ℕ), MeasurableSet (dirac ⁻¹' A n)⊢ MeasurableSet (dirac ⁻¹' ⋃ i, A i)
X:Type u_1inst✝:MeasurableSpace XA✝:Set (Measure X)A:ℕ → Set (Measure X)hA:∀ (n : ℕ), MeasurableSpace.GenerateMeasurable (MeasurableGen X) (A n)ih:∀ (n : ℕ), MeasurableSet (dirac ⁻¹' A n)⊢ MeasurableSet (⋃ i, dirac ⁻¹' A i)
All goals completed! 🐙
補題.
対応 \mu \mapsto \mathcal{K}_{\nu}(\mu) は
\Measure(X) \to \Measure(Y) として可測である。
Lean code
theorem Measure.bind_measurable (f : X → Measure Y) (hf : Measurable f) :
Measurable (Measure.bind f) := X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Measure Yhf:Measurable f⊢ Measurable (bind f)
X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Measure Yhf:Measurable fA:Set YhA:MeasurableSet A⊢ Measurable fun x => (bind f x) A
X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Measure Yhf:Measurable fA:Set YhA:MeasurableSet A⊢ Measurable fun x => ∫⁻ (x : X), (f x) A ∂x
X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Measure Yhf:Measurable fA:Set YhA:MeasurableSet A⊢ Measurable fun x => (f x) A
All goals completed! 🐙
定理.
\nu : X \to \Measure(Y) と \lambda : Y \to \Measure(Z) が可測ならば
\mathcal{K}_\lambda \circ \mathcal{K}_\nu =
\mathcal{K}_{\mathcal{K}_\lambda \circ \nu},
\qquad
\mathcal{K}_\nu \circ \delta = \nu,
\qquad
\mathcal{K}_{\delta}(\mu) = \mu.
が成り立つ。
この 3 つの等式はモナド則と呼ばれます。
Lean code
theorem Measure.bind_assoc
(ν : X → Measure Y) (hν : Measurable ν)
(ℓ : Y → Measure Z) (hℓ : Measurable ℓ) :
bind ℓ ∘ bind ν =
bind (bind ℓ ∘ ν) := X:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zν:X → Measure Yhν:Measurable νℓ:Y → Measure Zhℓ:Measurable ℓ⊢ bind ℓ ∘ bind ν = bind (bind ℓ ∘ ν)
X:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zν:X → Measure Yhν:Measurable νℓ:Y → Measure Zhℓ:Measurable ℓμ:Measure XA:Set ZhA:MeasurableSet A⊢ ((bind ℓ ∘ bind ν) μ) A = (bind (bind ℓ ∘ ν) μ) A
X:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zν:X → Measure Yhν:Measurable νℓ:Y → Measure Zhℓ:Measurable ℓμ:Measure XA:Set ZhA:MeasurableSet A⊢ (bind ℓ (bind ν μ)) A = (bind (bind ℓ ∘ ν) μ) A
X:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zν:X → Measure Yhν:Measurable νℓ:Y → Measure Zhℓ:Measurable ℓμ:Measure XA:Set ZhA:MeasurableSet A⊢ ∫⁻ (x : Y), (ℓ x) A ∂bind ν μ = (bind (bind ℓ ∘ ν) μ) A
X:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zν:X → Measure Yhν:Measurable νℓ:Y → Measure Zhℓ:Measurable ℓμ:Measure XA:Set ZhA:MeasurableSet A⊢ ∫⁻ (x : Y), (ℓ x) A ∂bind ν μ = ∫⁻ (x : X), ((bind ℓ ∘ ν) x) A ∂μ
X:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zν:X → Measure Yhν:Measurable νℓ:Y → Measure Zhℓ:Measurable ℓμ:Measure XA:Set ZhA:MeasurableSet A⊢ ∫⁻ (x : X), ∫⁻ (y : Y), (ℓ y) A ∂ν x ∂μ = ∫⁻ (x : X), ((bind ℓ ∘ ν) x) A ∂μX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zν:X → Measure Yhν:Measurable νℓ:Y → Measure Zhℓ:Measurable ℓμ:Measure XA:Set ZhA:MeasurableSet A⊢ Measurable fun x => (ℓ x) A
X:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zν:X → Measure Yhν:Measurable νℓ:Y → Measure Zhℓ:Measurable ℓμ:Measure XA:Set ZhA:MeasurableSet A⊢ ∫⁻ (x : X), ∫⁻ (y : Y), (ℓ y) A ∂ν x ∂μ = ∫⁻ (x : X), ((bind ℓ ∘ ν) x) A ∂μ All goals completed! 🐙
X:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zν:X → Measure Yhν:Measurable νℓ:Y → Measure Zhℓ:Measurable ℓμ:Measure XA:Set ZhA:MeasurableSet A⊢ Measurable fun x => (ℓ x) A All goals completed! 🐙theorem Measure.dirac_bind (f : X → Measure Y) (hf : Measurable f) :
bind f ∘ dirac = f := X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Measure Yhf:Measurable f⊢ bind f ∘ dirac = f
X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Measure Yhf:Measurable fx:XA:Set YhA:MeasurableSet A⊢ ((bind f ∘ dirac) x) A = (f x) A
X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Measure Yhf:Measurable fx:XA:Set YhA:MeasurableSet A⊢ ∫⁻ (x : X), (f x) A ∂dirac x = (f x) A
All goals completed! 🐙theorem Measure.bind_dirac (μ : Measure X) :
bind dirac μ = μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure X⊢ bind dirac μ = μ
X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet A⊢ (bind dirac μ) A = μ A
X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet A⊢ ∫⁻ (x : X), (dirac x) A ∂μ = μ A
X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet A⊢ ∫⁻ (x : X), A.indicator (fun x => 1) x ∂μ = μ A
X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet A⊢ ∫⁻ (a : X) in A, 1 ∂μ = μ A
All goals completed! 🐙