ae_of_compProd — Mathlib

English

If f is integrable with respect to the product kernel (κ ⊗ η) a, then f(x,·) is integrable w.r.t. η(a,x) for κ-a.e. x.

Русский

Если f интегрируема по произведённому ядру (κ ⊗ η) a, то для почти всех x по κ a функция y ↦ f(x,y) интегрируема по η(a,x).

LaTeX

$$MeasureTheory.Integrable.ae_of_compProd (hf) : ∀ᵐ x ∂κ a, Integrable (fun y => f (x, y)) (η (a, x))$$

Lean4

theorem _root_.MeasureTheory.Integrable.ae_of_compProd ⦃f : β × γ → E⦄ (hf : Integrable f ((κ ⊗ₖ η) a)) :
    ∀ᵐ x ∂κ a, Integrable (fun y => f (x, y)) (η (a, x)) :=
  ((integrable_compProd_iff hf.aestronglyMeasurable).mp hf).1

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