continuousOn_smul — Mathlib

English

If f ∈ LocallyIntegrableOn on s and g ∈ ContinuousOn on K with A ⊆ K, then the smul product f•g is LocallyIntegrableOn on A.

Русский

Если f локально интегрируем на s и g непрерывна на K, A ⊆ K, то f·g локально интегрируемо на A.

LaTeX

$$$\text{LocallyIntegrableOn}(f\cdot g, A, μ)$$$

Lean4

theorem continuousOn_smul [LocallyCompactSpace X] [T2Space X] {𝕜 : Type*} [NormedRing 𝕜]
    [SecondCountableTopologyEither X 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] {f : X → E} {g : X → 𝕜} {s : Set X}
    (hs : IsLocallyClosed s) (hf : LocallyIntegrableOn f s μ) (hg : ContinuousOn g s) :
    LocallyIntegrableOn (fun x => g x • f x) s μ :=
  by
  rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢
  exact fun k hk_sub hk_c => (hf k hk_sub hk_c).continuousOn_smul (hg.mono hk_sub) hk_c

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