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‖ₑ) : LocallyIntegrable g μ

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 : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ (a : X) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) : LocallyIntegrable f μ ↔ LocallyIntegrable g μ

theorem MeasureTheory.LocallyIntegrable.congr {X : Type u_1} {ε : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {μ : Measure X} {f g : X → ε} (hf : LocallyIntegrable f μ) (h : f =ᶠ[ae μ] g) : LocallyIntegrable g μ

theorem MeasureTheory.locallyIntegrable_congr {X : Type u_1} {ε : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {μ : Measure X} {f g : X → ε} (h : f =ᶠ[ae μ] g) : LocallyIntegrable f μ ↔ LocallyIntegrable g μ