theorem
MeasureTheory.IntegrableAtFilter.congr'_enorm
{α : Type u_1}
{ε : Type u_3}
{ε' : Type u_4}
[MeasurableSpace α]
{μ : Measure α}
[TopologicalSpace ε]
[TopologicalSpace ε']
[ContinuousENorm ε]
[ContinuousENorm ε']
{l : Filter α}
{f : α → ε}
{g : α → ε'}
(hf : IntegrableAtFilter f l μ)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ)
:
IntegrableAtFilter g l μ
theorem
MeasureTheory.IntegrableAtFilter.congr
{α : Type u_1}
{ε : Type u_3}
[MeasurableSpace α]
{μ : Measure α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{l : Filter α}
{f g : α → ε}
(hf : IntegrableAtFilter f l μ)
(h : f =ᶠ[ae μ] g)
:
IntegrableAtFilter g l μ
theorem
integrableOn_of_integrableOn_inter_support
{α : Type u_1}
{ε' : Type u_4}
[MeasurableSpace α]
{s : Set α}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε']
[ENormedAddMonoid ε']
[TopologicalSpace.PseudoMetrizableSpace ε']
{f : α → ε'}
(hs : MeasurableSet s)
(hf : MeasureTheory.IntegrableOn f (s ∩ Function.support f) μ)
: