memL1_smul_of_L1_withDensity — Mathlib

English

If f≥0 is measurable, then f • u belongs to L1 with density μ when u is in L1 with density μ.withDensity f.

Русский

Если f≥0 измерима, то f • u принадлежит L1 по мере μ, когда u в L1 по μ.withDensity f.

LaTeX

$$MemLp (fun x => f x • u x) 1 μ$$

Lean4

theorem memL1_smul_of_L1_withDensity {f : α → ℝ≥0} (f_meas : Measurable f) (u : Lp E 1 (μ.withDensity fun x => f x)) :
    MemLp (fun x => f x • u x) 1 μ :=
  memLp_one_iff_integrable.2 <|
    (integrable_withDensity_iff_integrable_smul f_meas).1 <| memLp_one_iff_integrable.1 (Lp.memLp u)

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