setIntegral_stieltjesOfMeasurableRat_rat

English

If for all a, IsMarkovKernel(κCond a), then condKernelCountable κCond h_atom is a Markov kernel.

Русский

Если для каждого a, κCond a является марковским ядром, то condKernelCountable κCond h_atom является марковским ядром.

LaTeX

$$$[\\forall a, IsMarkovKernel(κCond a)] \\Rightarrow IsMarkovKernel( condKernelCountable κCond h_{atom} ).$$$

Lean4

theorem setIntegral_stieltjesOfMeasurableRat_rat (hf : IsRatCondKernelCDF f κ ν) (a : α) (q : ℚ) {s : Set β}
    (hs : MeasurableSet s) :
    ∫ b in s, stieltjesOfMeasurableRat f hf.measurable (a, b) q ∂(ν a) = (κ a).real (s ×ˢ Iic (q : ℝ)) :=
  by
  rw [setIntegral_congr_ae hs (g := fun b ↦ f (a, b) q) ?_, hf.setIntegral a hs]
  filter_upwards [stieltjesOfMeasurableRat_ae_eq hf a q] with b hb using fun _ ↦ hb

Похожие утверждения