integral — Mathlib

English

Auxiliary statement expressing a similar a.e. Tendsto to 1 along t→∞ for fixed a.

Русский

Дополнительное утверждение, аналогичное сходу к 1 по t→∞ для фиксированного a.

LaTeX

$$$\forall a,\; \text{ae}_{t\sim ν(a)}(\text{Tendsto}(f(a,t),\, atTop,\, 1)).$$$

Lean4

theorem integral {f : α × β → StieltjesFunction} (hf : IsCondKernelCDF f κ ν) (a : α) (x : ℝ) :
    ∫ b, f (a, b) x ∂(ν a) = (κ a).real (univ ×ˢ Iic x) := by
  rw [← hf.setIntegral _ MeasurableSet.univ, Measure.restrict_univ]

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