@[simp]
theorem
MeasureTheory.Integrable.fun_mul_of_top_right
{α : Type u_1}
{𝕜 : Type u_3}
{mα : MeasurableSpace α}
{μ : Measure α}
[NormedField 𝕜]
{f φ : α → 𝕜}
(hf : Integrable f μ)
(hφ : MemLp φ ⊤ μ)
:
Integrable (fun (x : α) => φ x * f x) μ
@[simp]
theorem
MeasureTheory.Integrable.fun_mul_of_top_left
{α : Type u_1}
{𝕜 : Type u_3}
{mα : MeasurableSpace α}
{μ : Measure α}
[NormedField 𝕜]
{f φ : α → 𝕜}
(hφ : Integrable φ μ)
(hf : MemLp f ⊤ μ)
:
Integrable (fun (x : α) => φ x * f x) μ
theorem
MeasureTheory.Integrable.measurable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[ContinuousENorm β]
[μ.IsComplete]
{f : α → β}
[BorelSpace β]
(hf : Integrable f μ)
: