sFinite — Mathlib

English

For kernels κ and η, and a measurable f, HasFiniteIntegral of f under κ ⊗ η is equivalent to a pair of conditions: almost everywhere finiteness of f(a,·) under η(a,·), and finiteness of the integral of its norm against η.

Русский

Для ядер κ и η и измеримой функции f выполнение условий: почти нигде конечность интеграла f(a,·) по η(a,·) и конечность интеграла нормы f по η(a,·) эквивалентно HasFiniteIntegral.

LaTeX

$$HasFiniteIntegral f ((κ ⊗ η) a) ↔ (∀ᵐ a ∂κ a, HasFiniteIntegral (λ y, f(a,y)) (η(a,a))) ∧ HasFiniteIntegral (λ a, ∫ y, ||f(a,y)|| dη(a,y)) (κ a)$$

Lean4

instance _root_.ProbabilityTheory.IsSFiniteKernel.sFinite [IsSFiniteKernel κ] (a : α) : SFinite (κ a) :=
  ⟨⟨fun n ↦ seq κ n a, inferInstance, (measure_sum_seq κ a).symm⟩⟩

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