convolution_integrand_bound_left — Mathlib

English

If f and g are measurable, then the function t ↦ L(f(x−t), g(t)) is measurable with respect to the product measure μ×ν.

Русский

Если f и g измеримы, то t ↦ L(f(x−t), g(t)) измерима по произведённой мере μ×ν.

LaTeX

$$AEStronglyMeasurable (λ t, L (f (x−t)) (g t)) μ$$

Lean4

theorem _root_.HasCompactSupport.convolution_integrand_bound_left (hcf : HasCompactSupport f) (hf : Continuous f)
    {x t : G} {s : Set G} (hx : x ∈ s) :
    ‖L (f (x - t)) (g t)‖ ≤ (-tsupport f + s).indicator (fun t => (‖L‖ * ⨆ i, ‖f i‖) * ‖g t‖) t :=
  by
  convert hcf.convolution_integrand_bound_right L.flip hf hx using 1
  simp_rw [L.opNorm_flip, mul_right_comm]

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