English
If f is integrable on μ×ν, then the function y ↦ ∫ ‖f(x,y)‖ dμ is integrable with respect to ν.
Русский
Если f интегрируема на μ×ν, то y↦∫‖f(x,y)‖ dμ интегрируема по ν.
LaTeX
$$$\mathrm{Integrable}(f, μ×ν) \Rightarrow \mathrm{Integrable}(y \mapsto \int x \|f(x,y)\| dμ, ν)$$$
Lean4
theorem op_fst_snd {F G : Type*} [NormedAddCommGroup F] [NormedAddCommGroup G] {op : E → F → G}
(hop : Continuous op.uncurry) (hop_norm : ∃ C, ∀ x y, ‖op x y‖ ≤ C * ‖x‖ * ‖y‖) {f : α → E} {g : β → F}
(hf : Integrable f μ) (hg : Integrable g ν) : Integrable (fun z ↦ op (f z.1) (g z.2)) (μ.prod ν) :=
by
use hop.comp_aestronglyMeasurable₂ hf.1.comp_fst hg.1.comp_snd
rcases hop_norm with ⟨C, hC⟩
calc
∫⁻ z, ‖op (f z.1) (g z.2)‖ₑ ∂μ.prod ν ≤ ∫⁻ z, .ofReal C * ‖f z.1‖ₑ * ‖g z.2‖ₑ ∂μ.prod ν :=
by
gcongr with z
simp only [enorm_eq_nnnorm, ENNReal.ofReal, ← ENNReal.coe_mul, ENNReal.coe_le_coe, ← NNReal.coe_le_coe,
NNReal.coe_mul, coe_nnnorm]
refine (hC _ _).trans ?_
gcongr
apply le_coe_toNNReal
_ ≤ ∫⁻ x, ∫⁻ y, .ofReal C * ‖f x‖ₑ * ‖g y‖ₑ ∂ν ∂μ := (lintegral_prod_le _)
_ ≤ .ofReal C * (∫⁻ x, ‖f x‖ₑ ∂μ) * ∫⁻ y, ‖g y‖ₑ ∂ν := by
simp [lintegral_const_mul', lintegral_mul_const', hg.2.ne, mul_assoc]
_ < ∞ := by apply_rules [ENNReal.mul_lt_top, hf.2, hg.2, ENNReal.ofReal_lt_top]
