English
Auxiliary construction: for a countable index set and a family κCond, define a conditional kernel on α × β by κCondCountable.
Русский
Вспомогательное определение: для счетного множества индексов и семейства κCond задаём условное ядро κCondCountable на α × β.
LaTeX
$$Definition: condKernelCountable (h_atom) : Kernel (α × β) Ω$$
Lean4
/-- A conditional kernel is almost everywhere a probability measure. -/
theorem isProbabilityMeasure_ae [IsFiniteKernel κ.fst] [κ.IsCondKernel κCond] (a : α) :
∀ᵐ b ∂(κ.fst a), IsProbabilityMeasure (κCond (a, b)) :=
by
have h := disintegrate κ κCond
by_cases h_sfin : IsSFiniteKernel κCond
swap; · rw [Kernel.compProd_of_not_isSFiniteKernel_right _ _ h_sfin] at h; simp [h.symm]
suffices ∀ᵐ b ∂(κ.fst a), κCond (a, b) Set.univ = 1
by
convert this with b
exact ⟨fun _ ↦ measure_univ, fun h ↦ ⟨h⟩⟩
suffices (∀ᵐ b ∂(κ.fst a), κCond (a, b) Set.univ ≤ 1) ∧ (∀ᵐ b ∂(κ.fst a), 1 ≤ κCond (a, b) Set.univ) by
filter_upwards [this.1, this.2] with b h1 h2 using le_antisymm h1 h2
have h_eq s (hs : MeasurableSet s) : ∫⁻ b, s.indicator (fun b ↦ κCond (a, b) Set.univ) b ∂κ.fst a = κ.fst a s :=
by
conv_rhs => rw [← h]
rw [fst_compProd_apply _ _ _ hs]
have h_meas : Measurable fun b ↦ κCond (a, b) Set.univ :=
(κCond.measurable_coe MeasurableSet.univ).comp measurable_prodMk_left
constructor
· rw [ae_le_const_iff_forall_gt_measure_zero]
intro r hr
let s := {b | r ≤ κCond (a, b) Set.univ}
have hs : MeasurableSet s := h_meas measurableSet_Ici
have h_2_le : s.indicator (fun _ ↦ r) ≤ s.indicator (fun b ↦ (κCond (a, b)) Set.univ) :=
by
intro b
by_cases hbs : b ∈ s
· simpa [hbs]
· simp [hbs]
have : ∫⁻ b, s.indicator (fun _ ↦ r) b ∂(κ.fst a) ≤ κ.fst a s := (lintegral_mono h_2_le).trans_eq (h_eq s hs)
rw [lintegral_indicator_const hs] at this
contrapose! this with h_ne_zero
conv_lhs => rw [← one_mul (κ.fst a s)]
exact ENNReal.mul_lt_mul_right' h_ne_zero (measure_ne_top _ _) hr
· rw [ae_const_le_iff_forall_lt_measure_zero]
intro r hr
let s := {b | κCond (a, b) Set.univ ≤ r}
have hs : MeasurableSet s := h_meas measurableSet_Iic
have h_2_le : s.indicator (fun b ↦ (κCond (a, b)) Set.univ) ≤ s.indicator (fun _ ↦ r) :=
by
intro b
by_cases hbs : b ∈ s
· simpa [hbs]
· simp [hbs]
have : κ.fst a s ≤ ∫⁻ b, s.indicator (fun _ ↦ r) b ∂(κ.fst a) := (h_eq s hs).symm.trans_le (lintegral_mono h_2_le)
rw [lintegral_indicator_const hs] at this
contrapose! this with h_ne_zero
conv_rhs => rw [← one_mul (κ.fst a s)]
exact ENNReal.mul_lt_mul_right' h_ne_zero (measure_ne_top _ _) hr
