A lemma about measurability with density under scalar multiplication in normed spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
ae_measurable_with_density_iff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_2}
[normed_add_comm_group E]
[normed_space ℝ E]
[topological_space.second_countable_topology E]
[measurable_space E]
[borel_space E]
{f : α → nnreal}
(hf : measurable f)
{g : α → E} :
ae_measurable g (μ.with_density (λ (x : α), ↑(f x))) ↔ ae_measurable (λ (x : α), ↑(f x) • g x) μ