withDensitySMulLI_apply — Mathlib

English

A real-valued smul structure transfers integrability across densities.

Русский

Передача интегрируемости через умножение на скаляр сохраняется при плотности.

LaTeX

$$Integrable g (μ.withDensity f) ↔ Integrable (f.toReal • g) μ$$

Lean4

@[simp]
theorem withDensitySMulLI_apply {f : α → ℝ≥0} (f_meas : Measurable f) (u : Lp E 1 (μ.withDensity fun x => f x)) :
    withDensitySMulLI μ (E := E) f_meas u = (memL1_smul_of_L1_withDensity f_meas u).toLp fun x => f x • u x :=
  rfl

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