α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf_Lp : Memℒp f 1
⊢ f =ᵐ[μ] 0
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
⊢ f =ᵐ[μ] 0
have hf_Lp : Memℒp f 1 μ := memℒp_one_iff_integrable.mpr hf
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf_Lp : Memℒp f 1
f_Lp : { x // x ∈ Lp E 1 } := Memℒp.toLp f hf_Lp
⊢ f =ᵐ[μ] 0
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf_Lp : Memℒp f 1
⊢ f =ᵐ[μ] 0
let f_Lp := hf_Lp.toLp f
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf_Lp : Memℒp f 1
f_Lp : { x // x ∈ Lp E 1 } := Memℒp.toLp f hf_Lp
hf_f_Lp : f =ᵐ[μ] ↑↑f_Lp
⊢ f =ᵐ[μ] 0
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf_Lp : Memℒp f 1
f_Lp : { x // x ∈ Lp E 1 } := Memℒp.toLp f hf_Lp
⊢ f =ᵐ[μ] 0
have hf_f_Lp : f =ᵐ[μ] f_Lp := (Memℒp.coeFn_toLp hf_Lp).symm
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf_Lp : Memℒp f 1
f_Lp : { x // x ∈ Lp E 1 } := Memℒp.toLp f hf_Lp
hf_f_Lp : f =ᵐ[μ] ↑↑f_Lp
⊢ ↑↑f_Lp =ᵐ[μ] 0
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf_Lp : Memℒp f 1
f_Lp : { x // x ∈ Lp E 1 } := Memℒp.toLp f hf_Lp
hf_f_Lp : f =ᵐ[μ] ↑↑f_Lp
⊢ f =ᵐ[μ] 0
refine' hf_f_Lp.trans _
case refine'_1
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf_Lp : Memℒp f 1
f_Lp : { x // x ∈ Lp E 1 } := Memℒp.toLp f hf_Lp
hf_f_Lp : f =ᵐ[μ] ↑↑f_Lp
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f_Lp) s

case refine'_2
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf_Lp : Memℒp f 1
f_Lp : { x // x ∈ Lp E 1 } := Memℒp.toLp f hf_Lp
hf_f_Lp : f =ᵐ[μ] ↑↑f_Lp
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, ↑↑f_Lp x ∂μ) = 0
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf_Lp : Memℒp f 1
f_Lp : { x // x ∈ Lp E 1 } := Memℒp.toLp f hf_Lp
hf_f_Lp : f =ᵐ[μ] ↑↑f_Lp
⊢ ↑↑f_Lp =ᵐ[μ] 0
refine' Lp.ae_eq_zero_of_forall_set_integral_eq_zero f_Lp one_ne_zero ENNReal.coe_ne_top _ _
no goals
case refine'_1
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf_Lp : Memℒp f 1
f_Lp : { x // x ∈ Lp E 1 } := Memℒp.toLp f hf_Lp
hf_f_Lp : f =ᵐ[μ] ↑↑f_Lp
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f_Lp) s
exact fun s _ _ => Integrable.integrableOn (L1.integrable_coeFn _)
case refine'_2
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf_Lp : Memℒp f 1
f_Lp : { x // x ∈ Lp E 1 } := Memℒp.toLp f hf_Lp
hf_f_Lp : f =ᵐ[μ] ↑↑f_Lp
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ (∫ (x : α) in s, ↑↑f_Lp x ∂μ) = 0
case refine'_2
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf_Lp : Memℒp f 1
f_Lp : { x // x ∈ Lp E 1 } := Memℒp.toLp f hf_Lp
hf_f_Lp : f =ᵐ[μ] ↑↑f_Lp
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, ↑↑f_Lp x ∂μ) = 0
intro s hs hμs
case refine'_2
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf_Lp : Memℒp f 1
f_Lp : { x // x ∈ Lp E 1 } := Memℒp.toLp f hf_Lp
hf_f_Lp : f =ᵐ[μ] ↑↑f_Lp
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ (∫ (a : α) in s, f a ∂μ) = 0
case refine'_2
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf_Lp : Memℒp f 1
f_Lp : { x // x ∈ Lp E 1 } := Memℒp.toLp f hf_Lp
hf_f_Lp : f =ᵐ[μ] ↑↑f_Lp
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ (∫ (x : α) in s, ↑↑f_Lp x ∂μ) = 0
rw [integral_congr_ae (ae_restrict_of_ae hf_f_Lp.symm)]
no goals
case refine'_2
α : Type u_2
E : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → E
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
hf_Lp : Memℒp f 1
f_Lp : { x // x ∈ Lp E 1 } := Memℒp.toLp f hf_Lp
hf_f_Lp : f =ᵐ[μ] ↑↑f_Lp
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ (∫ (a : α) in s, f a ∂μ) = 0
exact hf_zero s hs hμs