continuous_convolution_left_of_integrable

English

If the support of f is contained in a ball and g is constant on a ball around x0, then (f ⋆ L g)(x0) equals the integral of L(f t) g(x0) over μ.

Русский

Если опорa f лежит в шаре и g константа на шаре вокруг x0, то (f ⋆ g)(x0) равно интегралу L(f t) g(x0) по μ.

LaTeX

$$(hf : support f ⊆ ball 0 R) ∧ (hg : ∀ x ∈ ball x0 R, g x = g x0) → (f ⋆[L, μ] g) x0 = ∫ t, L (f t) (g x0) ∂μ$$

Lean4

theorem _root_.BddAbove.continuous_convolution_left_of_integrable [FirstCountableTopology G]
    [SecondCountableTopologyEither G E] (hbf : BddAbove (range fun x => ‖f x‖)) (hf : Continuous f)
    (hg : Integrable g μ) : Continuous (f ⋆[L, μ] g) :=
  by
  rw [← convolution_flip]
  exact hbf.continuous_convolution_right_of_integrable L.flip hg hf

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