English
If κ is a kernel with almost everywhere probability measures and μ ≠ 0, there exists η such that κ =ᵐ[μ] η and η is Markov.
Русский
Если κ — ядро с почти всюду вероятностными мерами и μ ≠ 0, существует η такое, что κ =ae μ η и η — марковское ядро.
LaTeX
$$$\\exists \\eta, (κ =^{\\ae}_{\\mu} \\eta) \\land \\text{IsMarkovKernel}(\\eta)$$$
Lean4
theorem exists_ae_eq_isMarkovKernel {μ : Measure α} (h : ∀ᵐ a ∂μ, IsProbabilityMeasure (κ a)) (h' : μ ≠ 0) :
∃ (η : Kernel α β), (κ =ᵐ[μ] η) ∧ IsMarkovKernel η := by
classical
obtain ⟨s, s_meas, μs, hs⟩ : ∃ s, MeasurableSet s ∧ μ s = 0 ∧ ∀ a ∉ s, IsProbabilityMeasure (κ a) :=
by
refine
⟨toMeasurable μ {a | ¬IsProbabilityMeasure (κ a)}, measurableSet_toMeasurable _ _, by
simpa [measure_toMeasurable] using h, ?_⟩
intro a ha
contrapose! ha
exact subset_toMeasurable _ _ ha
obtain ⟨a, ha⟩ : sᶜ.Nonempty := by contrapose! h'; simpa [μs, h'] using measure_univ_le_add_compl s (μ := μ)
refine ⟨Kernel.piecewise s_meas (Kernel.const _ (κ a)) κ, ?_, ?_⟩
· filter_upwards [measure_eq_zero_iff_ae_notMem.1 μs] with b hb
simp [hb, piecewise]
· refine ⟨fun b ↦ ?_⟩
by_cases hb : b ∈ s
· simpa [hb, piecewise] using hs _ ha
· simpa [hb, piecewise] using hs _ hb
