English
Under the usual assumptions, the iterated convolution (f ⋆ g) ⋆ k equals f ⋆ (g ⋆ k) at each point.
Русский
При обычных предположениях итеративная свёртка (f ⋆ g) ⋆ k равна f ⋆ (g ⋆ k) в каждой точке.
LaTeX
$$$$((f \\star[ L,\\nu] g) \\star[ L_2, \\mu] k)_{x_0} = (f \\star[ L_3, \\nu] g \\star[ L_4, \\mu] k)_{x_0}.$$$$
Lean4
/-- Convolution is associative. This requires that
* all maps are a.e. strongly measurable w.r.t. one of the measures
* `f ⋆[L, ν] g` exists almost everywhere
* `‖g‖ ⋆[μ] ‖k‖` exists almost everywhere
* `‖f‖ ⋆[ν] (‖g‖ ⋆[μ] ‖k‖)` exists at `x₀` -/
theorem convolution_assoc (hL : ∀ (x : E) (y : E') (z : E''), L₂ (L x y) z = L₃ x (L₄ y z)) {x₀ : G}
(hf : AEStronglyMeasurable f ν) (hg : AEStronglyMeasurable g μ) (hk : AEStronglyMeasurable k μ)
(hfg : ∀ᵐ y ∂μ, ConvolutionExistsAt f g y L ν)
(hgk : ∀ᵐ x ∂ν, ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) x (mul ℝ ℝ) μ)
(hfgk : ConvolutionExistsAt (fun x => ‖f x‖) ((fun x => ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x => ‖k x‖) x₀ (mul ℝ ℝ) ν) :
((f ⋆[L, ν] g) ⋆[L₂, μ] k) x₀ = (f ⋆[L₃, ν] g ⋆[L₄, μ] k) x₀ :=
by
refine
convolution_assoc' L L₂ L₃ L₄ hL hfg (hgk.mono fun x hx => hx.of_norm L₄ hg hk)
?_
-- the following is similar to `Integrable.convolution_integrand`
have h_meas : AEStronglyMeasurable (uncurry fun x y => L₃ (f y) (L₄ (g x) (k (x₀ - y - x)))) (μ.prod ν) :=
by
refine L₃.aestronglyMeasurable_comp₂ hf.comp_snd ?_
refine L₄.aestronglyMeasurable_comp₂ hg.comp_fst ?_
refine (hk.mono_ac ?_).comp_measurable ((measurable_const.sub measurable_snd).sub measurable_fst)
refine QuasiMeasurePreserving.absolutelyContinuous ?_
refine
QuasiMeasurePreserving.prod_of_left ((measurable_const.sub measurable_snd).sub measurable_fst)
(Eventually.of_forall fun y => ?_)
dsimp only
exact quasiMeasurePreserving_sub_left_of_right_invariant μ _
have h2_meas : AEStronglyMeasurable (fun y => ∫ x, ‖L₃ (f y) (L₄ (g x) (k (x₀ - y - x)))‖ ∂μ) ν :=
h_meas.prod_swap.norm.integral_prod_right'
have h3 : map (fun z : G × G => (z.1 - z.2, z.2)) (μ.prod ν) = μ.prod ν := (measurePreserving_sub_prod μ ν).map_eq
suffices Integrable (uncurry fun x y => L₃ (f y) (L₄ (g x) (k (x₀ - y - x)))) (μ.prod ν)
by
rw [← h3] at this
convert this.comp_measurable (measurable_sub.prodMk measurable_snd)
ext ⟨x, y⟩
simp +unfoldPartialApp only [uncurry, Function.comp_apply, sub_sub_sub_cancel_right]
simp_rw [integrable_prod_iff' h_meas]
refine
⟨((quasiMeasurePreserving_sub_left_of_right_invariant ν x₀).ae hgk).mono fun t ht =>
(L₃ (f t)).integrable_comp <| ht.of_norm L₄ hg hk,
?_⟩
refine
(hfgk.const_mul (‖L₃‖ * ‖L₄‖)).mono' h2_meas
(((quasiMeasurePreserving_sub_left_of_right_invariant ν x₀).ae hgk).mono fun t ht => ?_)
simp_rw [convolution_def, mul_apply', mul_mul_mul_comm ‖L₃‖ ‖L₄‖, ← integral_const_mul]
rw [Real.norm_of_nonneg (by positivity)]
refine
integral_mono_of_nonneg (Eventually.of_forall fun t => norm_nonneg _) ((ht.const_mul _).const_mul _)
(Eventually.of_forall fun s => ?_)
simp only [← mul_assoc ‖L₄‖]
apply_rules [ContinuousLinearMap.le_of_opNorm₂_le_of_le, le_rfl]
