convolution_integrand_bound_right

English

For HasCompactSupport g and continuous g, and appropriate s,u with x in s and subset condition, the same right-bound inequality holds for all x,t with indicator over the subset.

Русский

Для HasCompactSupport g и непрерывной g, и подходящих s,u с x∈s и условия подмножества, выполняется аналогичное неравенство справа для всех x,t.

LaTeX

$$$HasCompactSupport\ g \ Land \ Continuous g \Rightarrow \|L(f(t), g(x-t))\| ≤ (-tsupport g + s).indicator(\dots)\ t$$$

Lean4

theorem _root_.HasCompactSupport.convolution_integrand_bound_right (hcg : HasCompactSupport g) (hg : Continuous g)
    {x t : G} {s : Set G} (hx : x ∈ s) :
    ‖L (f t) (g (x - t))‖ ≤ (-tsupport g + s).indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖) t :=
  hcg.convolution_integrand_bound_right_of_subset L hg hx Subset.rfl

Похожие утверждения