English
The symmetric definition of convolution with a bilinear operator equal to multiplication: (f ⋆ g)(x) = ∫ f(x−t) g(t) dt.
Русский
Симметричное определение свёртки, когда билинейный оператор равен умножению: (f ⋆ g)(x) = ∫ f(x−t) g(t) dt.
LaTeX
$$$(f ⋆ g)(x) = \int_G f(x-t) \cdot g(t) \, d\mu(t).$$$
Lean4
/-- The convolution is continuous if one function is integrable and the other is bounded and
continuous. -/
theorem _root_.BddAbove.continuous_convolution_right_of_integrable [FirstCountableTopology G]
[SecondCountableTopologyEither G E'] (hbg : BddAbove (range fun x => ‖g x‖)) (hf : Integrable f μ)
(hg : Continuous g) : Continuous (f ⋆[L, μ] g) :=
by
refine continuous_iff_continuousAt.mpr fun x₀ => ?_
have : ∀ᶠ x in 𝓝 x₀, ∀ᵐ t : G ∂μ, ‖L (f t) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖ :=
by
filter_upwards with x; filter_upwards with t
apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl, le_ciSup hbg (x - t)]
refine continuousAt_of_dominated ?_ this ?_ ?_
· exact Eventually.of_forall fun x => hf.aestronglyMeasurable.convolution_integrand_snd' L hg.aestronglyMeasurable
· exact (hf.norm.const_mul _).mul_const _
·
exact
Eventually.of_forall fun t =>
(L.continuous₂.comp₂ continuous_const <| hg.comp <| continuous_id.sub continuous_const).continuousAt
