α : Type u_2
β : Type ?u.102789
E : Type u_1
F : Type ?u.102795
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearOrder E
f : α → E
hf : AEStronglyMeasurable f μ
h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}
⊢ (∫ (x : α) in {x | f x < 0}, f x ∂μ) = ∫ (x : α) in {x | f x ≤ 0}, f x ∂μ
α : Type u_2
β : Type ?u.102789
E : Type u_1
F : Type ?u.102795
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearOrder E
f : α → E
hf : AEStronglyMeasurable f μ
⊢ (∫ (x : α) in {x | f x < 0}, f x ∂μ) = ∫ (x : α) in {x | f x ≤ 0}, f x ∂μ
have h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0} := by
  ext; simp_rw [Set.mem_union, Set.mem_setOf_eq]; exact le_iff_lt_or_eq
α : Type u_2
β : Type ?u.102789
E : Type u_1
F : Type ?u.102795
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearOrder E
f : α → E
hf : AEStronglyMeasurable f μ
h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}
⊢ (∫ (x : α) in {x | f x < 0}, f x ∂μ) = ∫ (x : α) in {x | f x < 0} ∪ {x | f x = 0}, f x ∂μ
α : Type u_2
β : Type ?u.102789
E : Type u_1
F : Type ?u.102795
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearOrder E
f : α → E
hf : AEStronglyMeasurable f μ
h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}
⊢ (∫ (x : α) in {x | f x < 0}, f x ∂μ) = ∫ (x : α) in {x | f x ≤ 0}, f x ∂μ
rw [h_union]
α : Type u_2
β : Type ?u.102789
E : Type u_1
F : Type ?u.102795
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearOrder E
f : α → E
hf : AEStronglyMeasurable f μ
h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}
B : NullMeasurableSet {x | f x = 0}
⊢ (∫ (x : α) in {x | f x < 0}, f x ∂μ) = ∫ (x : α) in {x | f x < 0} ∪ {x | f x = 0}, f x ∂μ
α : Type u_2
β : Type ?u.102789
E : Type u_1
F : Type ?u.102795
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearOrder E
f : α → E
hf : AEStronglyMeasurable f μ
h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}
⊢ (∫ (x : α) in {x | f x < 0}, f x ∂μ) = ∫ (x : α) in {x | f x < 0} ∪ {x | f x = 0}, f x ∂μ
have B : NullMeasurableSet {x | f x = 0} μ :=
  hf.nullMeasurableSet_eq_fun aestronglyMeasurable_zero
α : Type u_2
β : Type ?u.102789
E : Type u_1
F : Type ?u.102795
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearOrder E
f : α → E
hf : AEStronglyMeasurable f μ
h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}
B : NullMeasurableSet {x | f x = 0}
⊢ (∫ (x : α) in {x | f x < 0} ∪ {x | f x = 0}, f x ∂μ) = ∫ (x : α) in {x | f x < 0}, f x ∂μ
α : Type u_2
β : Type ?u.102789
E : Type u_1
F : Type ?u.102795
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearOrder E
f : α → E
hf : AEStronglyMeasurable f μ
h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}
B : NullMeasurableSet {x | f x = 0}
⊢ (∫ (x : α) in {x | f x < 0}, f x ∂μ) = ∫ (x : α) in {x | f x < 0} ∪ {x | f x = 0}, f x ∂μ
symm
α : Type u_2
β : Type ?u.102789
E : Type u_1
F : Type ?u.102795
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearOrder E
f : α → E
hf : AEStronglyMeasurable f μ
h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}
B : NullMeasurableSet {x | f x = 0}
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | f x = 0}, f x = 0
α : Type u_2
β : Type ?u.102789
E : Type u_1
F : Type ?u.102795
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearOrder E
f : α → E
hf : AEStronglyMeasurable f μ
h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}
B : NullMeasurableSet {x | f x = 0}
⊢ (∫ (x : α) in {x | f x < 0} ∪ {x | f x = 0}, f x ∂μ) = ∫ (x : α) in {x | f x < 0}, f x ∂μ
refine' integral_union_eq_left_of_ae _
no goals
α : Type u_2
β : Type ?u.102789
E : Type u_1
F : Type ?u.102795
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearOrder E
f : α → E
hf : AEStronglyMeasurable f μ
h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}
B : NullMeasurableSet {x | f x = 0}
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | f x = 0}, f x = 0
filter_upwards [ae_restrict_mem₀ B] with x hx using hx
case h
α : Type u_2
β : Type ?u.102789
E : Type u_1
F : Type ?u.102795
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearOrder E
f : α → E
hf : AEStronglyMeasurable f μ
x✝ : α
⊢ x✝ ∈ {x | f x ≤ 0} ↔ x✝ ∈ {x | f x < 0} ∪ {x | f x = 0}
α : Type u_2
β : Type ?u.102789
E : Type u_1
F : Type ?u.102795
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearOrder E
f : α → E
hf : AEStronglyMeasurable f μ
⊢ {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}
ext
case h
α : Type u_2
β : Type ?u.102789
E : Type u_1
F : Type ?u.102795
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearOrder E
f : α → E
hf : AEStronglyMeasurable f μ
x✝ : α
⊢ f x✝ ≤ 0 ↔ f x✝ < 0 ∨ f x✝ = 0
case h
α : Type u_2
β : Type ?u.102789
E : Type u_1
F : Type ?u.102795
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearOrder E
f : α → E
hf : AEStronglyMeasurable f μ
x✝ : α
⊢ x✝ ∈ {x | f x ≤ 0} ↔ x✝ ∈ {x | f x < 0} ∪ {x | f x = 0}
simp_rw [Set.mem_union, Set.mem_setOf_eq]
no goals
case h
α : Type u_2
β : Type ?u.102789
E : Type u_1
F : Type ?u.102795
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearOrder E
f : α → E
hf : AEStronglyMeasurable f μ
x✝ : α
⊢ f x✝ ≤ 0 ↔ f x✝ < 0 ∨ f x✝ = 0
exact le_iff_lt_or_eq