English
For a proper kernel π and B ⊆ X measurable with respect to 𝓑, the L^1/L^∞ integral of A under π restricted to B equals the product integral under π ∘ μ restricted to A ∩ B, reflecting Bayes-type consistency of restriction.
Русский
При правильном ядре π и измеримом B выполняется равенство интегралов при ограничении, т.е. согласованность Байеса для ограничений.
LaTeX
$$$$ \int_B π(a,A)\, dμ(a) = (π\circ_m μ)(A\cap B). $$$$
Lean4
theorem setLIntegral_eq_comp (hπ : IsProper π) (h𝓑𝓧 : 𝓑 ≤ 𝓧) {μ : Measure[𝓧] X} (hA : MeasurableSet[𝓧] A)
(hB : MeasurableSet[𝓑] B) : ∫⁻ a in B, π a A ∂μ = (π ∘ₘ μ) (A ∩ B) :=
by
rw [Measure.bind_apply (by measurability) (π.measurable.mono h𝓑𝓧 le_rfl).aemeasurable]
simp only [hπ.inter_eq_indicator_mul h𝓑𝓧 hA hB, ← indicator_mul_const, Pi.one_apply, one_mul]
rw [← lintegral_indicator (h𝓑𝓧 _ hB)]
rfl
