of_comp_snd — Mathlib

English

If f is integrable with respect to μ×ν after composing with the second projection, then f is integrable with respect to ν provided μ ≠ 0.

Русский

Если f интегрируема по мере μ×ν после композиции с второй проекцией, то f интегрируема по ν при условии μ ≠ 0.

LaTeX

$$$\mathrm{Integrable}(f, μ×ν) \Rightarrow \mathrm{Integrable}(f, ν)$ under appropriate hypotheses on μ$$

Lean4

theorem of_comp_snd {f : β → E} (hf : Integrable (f ·.2) (μ.prod ν)) (hμ : μ ≠ 0) : Integrable f ν :=
  by
  rcases hf with ⟨hf_meas, hf_fin⟩
  use hf_meas.of_comp_snd hμ
  have := hf_meas.enorm
  aesop (add simp [HasFiniteIntegral, lintegral_prod, ENNReal.mul_lt_top_iff])

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