stieltjesOfMeasurableRat_ae_eq — Mathlib

English

For a finite κ and hf, for any a and q rational, the set-level (restricted) lower integral equals the corresponding real measure of the kernel.

Русский

Для конечного κ и hf, при любом a и рациональном q, выражение для ограниченного множества даёт равенство интеграла и меры ядра.

LaTeX

$$$\\int\\!\,\n b \\in s \\; \\text{stieltjesOfMeasurableRat}(f, hf.measurable,(a,b), q)\n dν(a) = κ(a)(s \\timesˢ Iic(q))$$$

Lean4

theorem stieltjesOfMeasurableRat_ae_eq (hf : IsRatCondKernelCDF f κ ν) (a : α) (q : ℚ) :
    (fun b ↦ stieltjesOfMeasurableRat f hf.measurable (a, b) q) =ᵐ[ν a] fun b ↦ f (a, b) q :=
  by
  filter_upwards [hf.isRatStieltjesPoint_ae a] with a ha
  rw [stieltjesOfMeasurableRat_eq, toRatCDF_of_isRatStieltjesPoint ha]

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