case refine'_1
α : Type u_1
E : Type ?u.644803
F : Type ?u.644806
𝕜 : Type ?u.644809
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : { x // x ∈ Lp ℝ 1 }
⊢ Continuous fun x => integral x

case refine'_2
α : Type u_1
E : Type ?u.644803
F : Type ?u.644806
𝕜 : Type ?u.644809
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : { x // x ∈ Lp ℝ 1 }
⊢ Continuous fun x => ‖Lp.posPart x‖ - ‖Lp.negPart x‖

case refine'_3
α : Type u_1
E : Type ?u.644803
F : Type ?u.644806
𝕜 : Type ?u.644809
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : { x // x ∈ Lp ℝ 1 }
⊢ ∀ (a : { x // x ∈ ↑(simpleFunc ℝ 1 μ) }), (fun f => integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖) ↑a
α : Type u_1
E : Type ?u.644803
F : Type ?u.644806
𝕜 : Type ?u.644809
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : { x // x ∈ Lp ℝ 1 }
⊢ integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖
refine' @isClosed_property _ _ _ ((↑) : (α →₁ₛ[μ] ℝ) → α →₁[μ] ℝ)
    (fun f : α →₁[μ] ℝ => integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖)
    (simpleFunc.denseRange one_ne_top) (isClosed_eq _ _) _ f
case refine'_1
α : Type u_1
E : Type ?u.644803
F : Type ?u.644806
𝕜 : Type ?u.644809
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : { x // x ∈ Lp ℝ 1 }
⊢ Continuous fun x => ↑integralCLM x
case refine'_1
α : Type u_1
E : Type ?u.644803
F : Type ?u.644806
𝕜 : Type ?u.644809
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : { x // x ∈ Lp ℝ 1 }
⊢ Continuous fun x => integral x
simp only [integral]
no goals
case refine'_1
α : Type u_1
E : Type ?u.644803
F : Type ?u.644806
𝕜 : Type ?u.644809
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : { x // x ∈ Lp ℝ 1 }
⊢ Continuous fun x => ↑integralCLM x
exact cont _
no goals
case refine'_2
α : Type u_1
E : Type ?u.644803
F : Type ?u.644806
𝕜 : Type ?u.644809
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : { x // x ∈ Lp ℝ 1 }
⊢ Continuous fun x => ‖Lp.posPart x‖ - ‖Lp.negPart x‖
refine' Continuous.sub (continuous_norm.comp Lp.continuous_posPart)
  (continuous_norm.comp Lp.continuous_negPart)
case refine'_3
α : Type u_1
E : Type ?u.644803
F : Type ?u.644806
𝕜 : Type ?u.644809
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : { x // x ∈ Lp ℝ 1 }
s : { x // x ∈ ↑(simpleFunc ℝ 1 μ) }
⊢ integral ↑s = ‖Lp.posPart ↑s‖ - ‖Lp.negPart ↑s‖
case refine'_3
α : Type u_1
E : Type ?u.644803
F : Type ?u.644806
𝕜 : Type ?u.644809
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : { x // x ∈ Lp ℝ 1 }
⊢ ∀ (a : { x // x ∈ ↑(simpleFunc ℝ 1 μ) }), (fun f => integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖) ↑a
intro s
case refine'_3
α : Type u_1
E : Type ?u.644803
F : Type ?u.644806
𝕜 : Type ?u.644809
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : { x // x ∈ Lp ℝ 1 }
s : { x // x ∈ ↑(simpleFunc ℝ 1 μ) }
⊢ SimpleFunc.integral s = ‖SimpleFunc.posPart s‖ - ‖SimpleFunc.negPart s‖
case refine'_3
α : Type u_1
E : Type ?u.644803
F : Type ?u.644806
𝕜 : Type ?u.644809
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : { x // x ∈ Lp ℝ 1 }
s : { x // x ∈ ↑(simpleFunc ℝ 1 μ) }
⊢ integral ↑s = ‖Lp.posPart ↑s‖ - ‖Lp.negPart ↑s‖
norm_cast
no goals
case refine'_3
α : Type u_1
E : Type ?u.644803
F : Type ?u.644806
𝕜 : Type ?u.644809
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : { x // x ∈ Lp ℝ 1 }
s : { x // x ∈ ↑(simpleFunc ℝ 1 μ) }
⊢ SimpleFunc.integral s = ‖SimpleFunc.posPart s‖ - ‖SimpleFunc.negPart s‖
exact SimpleFunc.integral_eq_norm_posPart_sub _