English
If f is integrable with respect to ν and g is integrable with respect to μ, then the convolution integrand given by L(f p.2) (g (p.1 − p.2)) is integrable with respect to μ×ν.
Русский
Если f интегрируема по ν и g интегрируема по μ, то конволюционная интегрантная функция интегрируема по μ×ν.
LaTeX
$$Integrable f ν → Integrable g μ → Integrable (λ p: G×G, L (f p.2) (g (p.1 - p.2))) (μ.prod ν)$$
Lean4
theorem convolution_integrand (hf : Integrable f ν) (hg : Integrable g μ) :
Integrable (fun p : G × G => L (f p.2) (g (p.1 - p.2))) (μ.prod ν) :=
by
have h_meas : AEStronglyMeasurable (fun p : G × G => L (f p.2) (g (p.1 - p.2))) (μ.prod ν) :=
hf.aestronglyMeasurable.convolution_integrand L hg.aestronglyMeasurable
have h2_meas : AEStronglyMeasurable (fun y : G => ∫ x : G, ‖L (f y) (g (x - y))‖ ∂μ) ν :=
h_meas.prod_swap.norm.integral_prod_right'
simp_rw [integrable_prod_iff' h_meas]
refine ⟨Eventually.of_forall fun t => (L (f t)).integrable_comp (hg.comp_sub_right t), ?_⟩
refine Integrable.mono' ?_ h2_meas (Eventually.of_forall fun t => (?_ : _ ≤ ‖L‖ * ‖f t‖ * ∫ x, ‖g (x - t)‖ ∂μ))
· simp only [integral_sub_right_eq_self (‖g ·‖)]
exact (hf.norm.const_mul _).mul_const _
· simp_rw [← integral_const_mul]
rw [Real.norm_of_nonneg (by positivity)]
exact
integral_mono_of_nonneg (Eventually.of_forall fun t => norm_nonneg _) ((hg.comp_sub_right t).norm.const_mul _)
(Eventually.of_forall fun t => L.le_opNorm₂ _ _)
