comp_fst — Mathlib

English

If a bounded bilinear map op is given with a bound ‖op(x,y)‖ ≤ C‖x‖‖y‖, and f,g are integrable, then the bilinear composition z ↦ op(f(z1), g(z2)) is integrable on the product measure.

Русский

Если задано ограниченное билинейное отображение op с пределом ‖op(x,y)‖ ≤ C‖x‖‖y‖, и f,g интегрируемы, то z ↦ op(f(z1), g(z2)) интегрируема по произведению мер.

LaTeX

$$$\exists C>0\,\forall x,y,\|op(x,y)\| ≤ C\|x\|\|y\| \Rightarrow \mathrm{Integrable}(z \mapsto op(f(z_1), g(z_2)), μ×ν)$$$

Lean4

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

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