of_norm — Mathlib

English

If f is AEStronglyMeasurable and g is AEStronglyMeasurable, then the function t ↦ L(f(x−t), g(t)) is AEStronglyMeasurable.

Русский

Если f и g — AES-измеримы, то t ↦ L(f(x−t), g(t)) — AES-измеримая функция.

LaTeX

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

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 μ) : ConvolutionExistsAt f g x₀ L μ :=
  h.of_norm' L hmf <| hmg.mono_ac (quasiMeasurePreserving_sub_left_of_right_invariant μ x₀).absolutelyContinuous

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