English
If HasCompactSupport g and g is continuous, then for any x,t and any s, the bound on ‖L(f t) (g (x−t))‖ is controlled by the indicator of −tsupport g + s and the product of ‖L‖, ‖f t‖, and sup‖g i‖ over i.
Русский
Если g имеет компактную опору и непрерывна, граница на ‖L(f(t), g(x−t))‖ управляется через индикацию −tsupport g + s и произведение ‖L‖, ‖f(t)‖ и sup‖g i‖.
LaTeX
$$$\|L(f(t), g(x-t))\| ≤ (-tsupport g + s).indicator (\lambda t. ‖L‖ \cdot ‖f(t)‖ \cdot ⨆ i, ‖g(i)‖) \, t$$$
Lean4
theorem _root_.HasCompactSupport.convolution_integrand_bound_right_of_subset (hcg : HasCompactSupport g)
(hg : Continuous g) {x t : G} {s u : Set G} (hx : x ∈ s) (hu : -tsupport g + s ⊆ u) :
‖L (f t) (g (x - t))‖ ≤ u.indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖) t :=
by
refine convolution_integrand_bound_right_of_le_of_subset _ (fun i => ?_) hx hu
exact le_ciSup (hg.norm.bddAbove_range_of_hasCompactSupport hcg.norm) _
