no goals
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
⊢ (∫ (x : α), ‖f x‖ ∂μ) = (∫ (x : α) in {x | 0 ≤ f x}, ‖f x‖ ∂μ) + ∫ (x : α) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ
rw [← integral_add_compl₀ h_meas hfi.norm]
case e_a
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
⊢ (∫ (x : α) in {x | 0 ≤ f x}, ‖f x‖ ∂μ) = ∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
⊢ ((∫ (x : α) in {x | 0 ≤ f x}, ‖f x‖ ∂μ) + ∫ (x : α) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) =
    (∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ) + ∫ (x : α) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ
congr 1
case e_a
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
x : α
hx : x ∈ {x | 0 ≤ f x}
⊢ ‖f x‖ = f x
case e_a
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
⊢ (∫ (x : α) in {x | 0 ≤ f x}, ‖f x‖ ∂μ) = ∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ
refine' set_integral_congr₀ h_meas fun x hx => _
case e_a
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
x : α
hx : x ∈ {x | 0 ≤ f x}
⊢ ‖f x‖ = f x
case e_a
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
x : α
hx : x ∈ {x | 0 ≤ f x}
⊢ ‖f x‖ = f x
dsimp only
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
x : α
hx : x ∈ {x | 0 ≤ f x}
⊢ 0 ≤ f x
case e_a
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
x : α
hx : x ∈ {x | 0 ≤ f x}
⊢ ‖f x‖ = f x
rw [Real.norm_eq_abs, abs_eq_self.mpr _]
no goals
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
x : α
hx : x ∈ {x | 0 ≤ f x}
⊢ 0 ≤ f x
exact hx
case e_a
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
⊢ (∫ (x : α) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) = -∫ (x : α) in {x | 0 ≤ f x}ᶜ, f x ∂μ
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
⊢ ((∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ) + ∫ (x : α) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) =
    (∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ) - ∫ (x : α) in {x | 0 ≤ f x}ᶜ, f x ∂μ
congr 1
case e_a
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
⊢ (∫ (x : α) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) = ∫ (a : α) in {x | 0 ≤ f x}ᶜ, -f a ∂μ
case e_a
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
⊢ (∫ (x : α) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) = -∫ (x : α) in {x | 0 ≤ f x}ᶜ, f x ∂μ
rw [← integral_neg]
case e_a
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
x : α
hx : x ∈ {x | 0 ≤ f x}ᶜ
⊢ ‖f x‖ = -f x
case e_a
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
⊢ (∫ (x : α) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) = ∫ (a : α) in {x | 0 ≤ f x}ᶜ, -f a ∂μ
refine' set_integral_congr₀ h_meas.compl fun x hx => _
case e_a
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
x : α
hx : x ∈ {x | 0 ≤ f x}ᶜ
⊢ ‖f x‖ = -f x
case e_a
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
x : α
hx : x ∈ {x | 0 ≤ f x}ᶜ
⊢ ‖f x‖ = -f x
dsimp only
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
x : α
hx : x ∈ {x | 0 ≤ f x}ᶜ
⊢ f x ≤ 0
case e_a
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
x : α
hx : x ∈ {x | 0 ≤ f x}ᶜ
⊢ ‖f x‖ = -f x
rw [Real.norm_eq_abs, abs_eq_neg_self.mpr _]
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
x : α
hx : ¬0 ≤ f x
⊢ f x ≤ 0
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
x : α
hx : x ∈ {x | 0 ≤ f x}ᶜ
⊢ f x ≤ 0
rw [Set.mem_compl_iff, Set.nmem_setOf_iff] at hx
no goals
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
x : α
hx : ¬0 ≤ f x
⊢ f x ≤ 0
linarith
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
⊢ ((∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ) - ∫ (x : α) in {x | 0 ≤ f x}ᶜ, f x ∂μ) =
    (∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ) - ∫ (x : α) in {x | f x < 0}, f x ∂μ
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
⊢ ((∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ) - ∫ (x : α) in {x | 0 ≤ f x}ᶜ, f x ∂μ) =
    (∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ) - ∫ (x : α) in {x | f x ≤ 0}, f x ∂μ
rw [← set_integral_neg_eq_set_integral_nonpos hfi.1]
case e_a.e_μ.e_s
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
⊢ {x | 0 ≤ f x}ᶜ = {x | f x < 0}
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
⊢ ((∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ) - ∫ (x : α) in {x | 0 ≤ f x}ᶜ, f x ∂μ) =
    (∫ (x : α) in {x | 0 ≤ f x}, f x ∂μ) - ∫ (x : α) in {x | f x < 0}, f x ∂μ
congr
case e_a.e_μ.e_s.h
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
x : α
⊢ x ∈ {x | 0 ≤ f x}ᶜ ↔ x ∈ {x | f x < 0}
case e_a.e_μ.e_s
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
⊢ {x | 0 ≤ f x}ᶜ = {x | f x < 0}
ext1 x
no goals
case e_a.e_μ.e_s.h
α : Type u_1
β : Type ?u.110031
E : Type ?u.110034
F : Type ?u.110037
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hfi : Integrable f
h_meas : NullMeasurableSet {x | 0 ≤ f x}
x : α
⊢ x ∈ {x | 0 ≤ f x}ᶜ ↔ x ∈ {x | f x < 0}
simp