of_norm' — Mathlib

English

If the norm of f and g is controlled by a bound h and the convolution exists, then the resulting convolution with L exists.

Русский

Если норма f и g управляется границей и существует свёртка, то свёртка с L существует.

LaTeX

$$ConvolutionExistsAt f g x₀ L μ$$

Lean4

/-- If `‖f‖ *[μ] ‖g‖` exists, then `f *[L, μ] g` exists. -/
theorem of_norm' {x₀ : G} (h : ConvolutionExistsAt (fun x => ‖f x‖) (fun x => ‖g x‖) x₀ (mul ℝ ℝ) μ)
    (hmf : AEStronglyMeasurable f μ) (hmg : AEStronglyMeasurable g <| map (fun t => x₀ - t) μ) :
    ConvolutionExistsAt f g x₀ L μ :=
  by
  refine (h.const_mul ‖L‖).mono' (hmf.convolution_integrand_snd' L hmg) (Eventually.of_forall fun x => ?_)
  rw [mul_apply', ← mul_assoc]
  apply L.le_opNorm₂

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