English
If g has compact support and is bounded by C, then for any x,t and sets s,u with x ∈ s and -(tsupport g) + s ⊆ u, the norm of L(f t, g(x−t)) is bounded by u.indicator(t) times ‖L‖·‖f t‖·C.
Русский
Если g имеет компактную опору и ограничена на ней величиной C, то при любых x,t и множествах s,u с x ∈ s и −tsupport g + s ⊆ u, нормa L(f(t), g(x−t)) ограничена через индикацию u.
LaTeX
$$$hC\!:\forall i, ‖g(i)‖≤C \\Rightarrow \forall {x,t}\, {s u},\ x\in s\, \text{and}\ -(tsupport g)+s\subseteq u:\
‖L(f t, g(x-t))‖ ≤ u.indicator (\lambda t. ‖L‖⋅‖f t‖⋅C)\ t$$
Lean4
theorem convolution_integrand_bound_right_of_le_of_subset {C : ℝ} (hC : ∀ i, ‖g i‖ ≤ C) {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‖ * C) t := by
-- Porting note: had to add `f := _`
refine le_indicator (f := fun t ↦ ‖L (f t) (g (x - t))‖) (fun t _ => ?_) (fun t ht => ?_) t
· apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl]
· have : x - t ∉ support g := by
refine mt (fun hxt => hu ?_) ht
refine ⟨_, Set.neg_mem_neg.mpr (subset_closure hxt), _, hx, ?_⟩
simp only [neg_sub, sub_add_cancel]
simp only [notMem_support.mp this, (L _).map_zero, norm_zero, le_rfl]
