smul_prod — Mathlib

English

If f is IntegrableOn on s×t with respect to μ.prod ν, then the swapped function is IntegrableOn on t×s with respect to ν.prod μ.

Русский

Если f интегрируемо на s×t относительно μ.prod ν, то переставленная функция интегрируема на t×s относительно ν.prod μ.

LaTeX

$$$\mathrm{IntegrableOn}(f, s×t, μ×ν) \Rightarrow \mathrm{IntegrableOn}(f\circ\mathrm{Prod.swap}, t×s, ν×μ)$$$

Lean4

theorem smul_prod {R : Type*} [NormedRing R] [Module R E] [IsBoundedSMul R E] {f : α → R} {g : β → E}
    (hf : Integrable f μ) (hg : Integrable g ν) : Integrable (fun z : α × β => f z.1 • g z.2) (μ.prod ν) :=
  hf.op_fst_snd continuous_smul ⟨1, by simpa using norm_smul_le⟩ hg

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