mathlib3 documentation

measure_theory.integral.lebesgue_normed_space

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) μ