ae_of_comp — Mathlib

English

From integrability of a function on the product kernel, deduce almost-everywhere integrability on slices.

Русский

Из интегрируемости на произведённом ядре выводим почти всюду интегрируемость на срезах.

LaTeX

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

Lean4

theorem _root_.MeasureTheory.Integrable.ae_of_comp ⦃f : γ → E⦄ (hf : Integrable f ((η ∘ₖ κ) a)) :
    ∀ᵐ x ∂κ a, Integrable f (η x) :=
  ((integrable_comp_iff hf.1).1 hf).1

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