English
Associativity of mlconvolution for ENNReal-valued functions with AEMeasurability assumptions.
Русский
Ассоциативность mlconvolution для функций в ENNReal с предпосылками AEMеасurable.
LaTeX
$$$f,g,k : G \\to \\mathbb{R}_{\\ge 0}^{\\infty},\\ hf hg hk \\Rightarrow f \\star (g \\star k) = (f \\star g) \\star k$$$
Lean4
@[to_additive]
theorem mlconvolution_assoc₀ {f g k : G → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
(hk : AEMeasurable k μ) : f ⋆ₘₗ[μ] g ⋆ₘₗ[μ] k = (f ⋆ₘₗ[μ] g) ⋆ₘₗ[μ] k :=
by
ext x
simp only [mlconvolution_def]
conv in f _ * (∫⁻ _, _ ∂μ) => rw [← lintegral_const_mul'' _ (by fun_prop), ← lintegral_mul_left_eq_self _ y⁻¹]
conv in (∫⁻ _, _ ∂μ) * k _ => rw [← lintegral_mul_const'' _ (by fun_prop)]
rw [lintegral_lintegral_swap]
· simp [mul_assoc]
simpa [mul_assoc] using by
fun_prop
/- Convolution is associative. -/
