English
If f,g are measurable, μ.withDensity f ∗ μ.withDensity g = μ.withDensity (mlconvolution f g μ).
Русский
Если f,g измеримы, то μ_{f} ∗ μ_{g} = μ_{mlconvolution(f,g,μ)}.
LaTeX
$$$ μ^{f} *_{μ} μ^{g} = μ^{(mlconvolution(f,g,μ))} $$$
Lean4
@[to_additive]
theorem mconv_withDensity_eq_mlconvolution₀ {f g : G → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
μ.withDensity f ∗ₘ μ.withDensity g = μ.withDensity (f ⋆ₘₗ[μ] g) :=
by
refine ext_of_lintegral _ fun φ hφ ↦ ?_
rw [lintegral_mconv_eq_lintegral_prod hφ, prod_withDensity₀ hf hg, lintegral_withDensity_eq_lintegral_mul₀,
lintegral_withDensity_eq_lintegral_mul₀, lintegral_prod,
lintegral_congr (fun x ↦ by apply (lintegral_mul_left_eq_self _ x⁻¹).symm), lintegral_lintegral_swap]
· simp only [Pi.mul_apply, mul_inv_cancel_left, mlconvolution_def]
conv in (∫⁻ _, _ ∂μ) * φ _ => rw [(lintegral_mul_const'' _ (by fun_prop)).symm]
all_goals
first
| fun_prop
| dsimp; fun_prop
