comp_snd — Mathlib

English

If f: α→R and g: β→E are integrable and there is a scalar action, then the product f(z1) • g(z2) is integrable on α×β.

Русский

Если f: α→R и g: β→E интегрируемы и существует скалярное действие, то произведение f(z1)•g(z2) интегрируемо на α×β.

LaTeX

$$$\mathrm{Integrable}(f, μ) \land \mathrm{Integrable}(g, ν) \Rightarrow \mathrm{Integrable}(z \mapsto f(z_1) \cdot g(z_2), μ×ν)$$$

Lean4

theorem comp_snd {f : β → E} (hf : Integrable f ν) (μ : Measure α) [IsFiniteMeasure μ] :
    Integrable (fun x ↦ f x.2) (μ.prod ν) :=
  by
  rw [← memLp_one_iff_integrable] at hf ⊢
  exact hf.comp_snd μ

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