theorem
MeasureTheory.LocallyIntegrable.norm
{X : Type u_1}
{E : Type u_2}
[MeasurableSpace X]
[TopologicalSpace X]
[NormedAddCommGroup E]
{f : X → E}
{μ : Measure X}
(hf : LocallyIntegrable f μ)
:
LocallyIntegrable (fun (x : X) => ‖f x‖) μ
theorem
MeasureTheory.LocallyIntegrable.congr'_enorm
{X : Type u_1}
{ε : Type u_2}
{ε' : Type u_3}
[MeasurableSpace X]
[TopologicalSpace X]
[TopologicalSpace ε]
[ContinuousENorm ε]
[TopologicalSpace ε']
[ContinuousENorm ε']
{μ : Measure X}
{f : X → ε}
{g : X → ε'}
(hf : LocallyIntegrable f μ)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (a : X) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ)
: