α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
⊢ integral f = ‖posPart f‖ - ‖negPart f‖
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
⊢ integral f = ‖posPart f‖ - ‖negPart f‖
have ae_eq₁ : (toSimpleFunc f).posPart =ᵐ[μ] (toSimpleFunc (posPart f)).map norm := by
  filter_upwards [posPart_toSimpleFunc f]with _ h
  rw [SimpleFunc.map_apply, h]
  conv_lhs => rw [← SimpleFunc.posPart_map_norm, SimpleFunc.map_apply]
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ integral f = ‖posPart f‖ - ‖negPart f‖
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
⊢ integral f = ‖posPart f‖ - ‖negPart f‖
have ae_eq₂ : (toSimpleFunc f).negPart =ᵐ[μ] (toSimpleFunc (negPart f)).map norm := by
  filter_upwards [negPart_toSimpleFunc f]with _ h
  rw [SimpleFunc.map_apply, h]
  conv_lhs => rw [← SimpleFunc.negPart_map_norm, SimpleFunc.map_apply]
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) =
    MeasureTheory.SimpleFunc.integral μ
      (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))

case hf
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ Integrable ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))

case hg
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ Integrable ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ integral f = ‖posPart f‖ - ‖negPart f‖
rw [integral, norm_eq_integral, norm_eq_integral, ← SimpleFunc.integral_sub]
case h
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
a✝ : α
h : ↑(toSimpleFunc (posPart f)) a✝ = ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝
⊢ ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
⊢ ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
filter_upwards [posPart_toSimpleFunc f]with _ h
case h
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
a✝ : α
h : ↑(toSimpleFunc (posPart f)) a✝ = ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝
⊢ ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝ = ‖↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝‖
case h
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
a✝ : α
h : ↑(toSimpleFunc (posPart f)) a✝ = ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝
⊢ ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝
rw [SimpleFunc.map_apply, h]
no goals
case h
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
a✝ : α
h : ↑(toSimpleFunc (posPart f)) a✝ = ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝
⊢ ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝ = ‖↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝‖
conv_lhs => rw [← SimpleFunc.posPart_map_norm, SimpleFunc.map_apply]
case h
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
a✝ : α
h : ↑(toSimpleFunc (negPart f)) a✝ = ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝
⊢ ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
⊢ ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
filter_upwards [negPart_toSimpleFunc f]with _ h
case h
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
a✝ : α
h : ↑(toSimpleFunc (negPart f)) a✝ = ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝
⊢ ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝ = ‖↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝‖
case h
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
a✝ : α
h : ↑(toSimpleFunc (negPart f)) a✝ = ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝
⊢ ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
rw [SimpleFunc.map_apply, h]
no goals
case h
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
a✝ : α
h : ↑(toSimpleFunc (negPart f)) a✝ = ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝
⊢ ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝ = ‖↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝‖
conv_lhs => rw [← SimpleFunc.negPart_map_norm, SimpleFunc.map_apply]
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) =
    MeasureTheory.SimpleFunc.integral μ
      (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) =
    MeasureTheory.SimpleFunc.integral μ
      (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))
show (toSimpleFunc f).integral μ =
  ((toSimpleFunc (posPart f)).map norm - (toSimpleFunc (negPart f)).map norm).integral μ
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ ↑(toSimpleFunc f) =ᵐ[μ]
    ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) =
    MeasureTheory.SimpleFunc.integral μ
      (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))
apply MeasureTheory.SimpleFunc.integral_congr (SimpleFunc.integrable f)
case h
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
a✝ : α
h₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝
h₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
⊢ ↑(toSimpleFunc f) a✝ =
    ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ ↑(toSimpleFunc f) =ᵐ[μ]
    ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))
filter_upwards [ae_eq₁, ae_eq₂]with _ h₁ h₂
case h
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
a✝ : α
h₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝
h₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
⊢ ↑(toSimpleFunc f) a✝ =
    ↑(SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝ - ↑(SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
case h
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
a✝ : α
h₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝
h₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
⊢ ↑(toSimpleFunc f) a✝ =
    ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
show _ = _ - _
case h
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
a✝ : α
h₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝
h₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
⊢ ↑(toSimpleFunc f) a✝ =
    ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝ - ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝
case h
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
a✝ : α
h₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝
h₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
⊢ ↑(toSimpleFunc f) a✝ =
    ↑(SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝ - ↑(SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
rw [← h₁, ← h₂]
case h
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
a✝ : α
h₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝
h₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
this :
  MeasureTheory.SimpleFunc.posPart (toSimpleFunc f) - MeasureTheory.SimpleFunc.negPart (toSimpleFunc f) = toSimpleFunc f
⊢ ↑(toSimpleFunc f) a✝ =
    ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝ - ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝
case h
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
a✝ : α
h₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝
h₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
⊢ ↑(toSimpleFunc f) a✝ =
    ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝ - ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝
have := (toSimpleFunc f).posPart_sub_negPart
no goals
case h
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
a✝ : α
h₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝
h₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝ = ↑(SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
this :
  MeasureTheory.SimpleFunc.posPart (toSimpleFunc f) - MeasureTheory.SimpleFunc.negPart (toSimpleFunc f) = toSimpleFunc f
⊢ ↑(toSimpleFunc f) a✝ =
    ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a✝ - ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) a✝
conv_lhs => rw [← this]
no goals
case hf
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ Integrable ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
exact (SimpleFunc.integrable f).pos_part.congr ae_eq₁
no goals
case hg
α : Type u_1
E : Type ?u.361821
F : Type ?u.361824
𝕜 : Type ?u.361827
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.364202
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.364298
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
ae_eq₁ : ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f)) =ᵐ[μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ Integrable ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
exact (SimpleFunc.integrable f).neg_part.congr ae_eq₂