smul_continuousOn — Mathlib

English

If f ∈ LocallyIntegrableOn on A and g ∈ ContinuousOn on K with A ⊆ K, then f was scaled by g remains LocallyIntegrableOn on A.

Русский

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

LaTeX

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

Lean4

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

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