α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
⊢ (∫ (a : α), f a ∂μ) =
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) - ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ)
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
⊢ (∫ (a : α), f a ∂μ) =
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) - ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ)
let f₁ := hf.toL1 f
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
⊢ (∫ (a : α), f a ∂μ) =
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) - ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ)
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
⊢ (∫ (a : α), f a ∂μ) =
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) - ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ)
have eq₁ : ENNReal.toReal (∫⁻ a, ENNReal.ofReal <| f a ∂μ) = ‖Lp.posPart f₁‖ := by
  rw [L1.norm_def]
  congr 1
  apply lintegral_congr_ae
  filter_upwards [Lp.coeFn_posPart f₁, hf.coeFn_toL1]with _ h₁ h₂
  rw [h₁, h₂, ENNReal.ofReal]
  congr 1
  apply NNReal.eq
  rw [Real.nnnorm_of_nonneg (le_max_right _ _)]
  rw [Real.coe_toNNReal', NNReal.coe_mk]
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
eq₂ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ) = ‖Lp.negPart f₁‖
⊢ (∫ (a : α), f a ∂μ) =
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) - ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ)
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
⊢ (∫ (a : α), f a ∂μ) =
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) - ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ)
have eq₂ : ENNReal.toReal (∫⁻ a, ENNReal.ofReal <| -f a ∂μ) = ‖Lp.negPart f₁‖ := by
  rw [L1.norm_def]
  congr 1
  apply lintegral_congr_ae
  filter_upwards [Lp.coeFn_negPart f₁, hf.coeFn_toL1]with _ h₁ h₂
  rw [h₁, h₂, ENNReal.ofReal]
  congr 1
  apply NNReal.eq
  simp only [Real.coe_toNNReal', coe_nnnorm, nnnorm_neg]
  rw [Real.norm_of_nonpos (min_le_right _ _), ← max_neg_neg, neg_zero]
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
eq₂ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ) = ‖Lp.negPart f₁‖
⊢ L1.integral (Integrable.toL1 (fun a => f a) ?hc) = ‖Lp.posPart f₁‖ - ‖Lp.negPart f₁‖

case hc
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
eq₂ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ) = ‖Lp.negPart f₁‖
⊢ Integrable fun a => f a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
eq₂ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ) = ‖Lp.negPart f₁‖
⊢ (∫ (a : α), f a ∂μ) =
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) - ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ)
rw [eq₁, eq₂, integral, dif_pos]
no goals
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
eq₂ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ) = ‖Lp.negPart f₁‖
⊢ L1.integral (Integrable.toL1 (fun a => f a) ?hc) = ‖Lp.posPart f₁‖ - ‖Lp.negPart f₁‖

case hc
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
eq₂ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ) = ‖Lp.negPart f₁‖
⊢ Integrable fun a => f a
exact L1.integral_eq_norm_posPart_sub _
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑(Lp.posPart f₁) a‖₊ ∂μ)
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
rw [L1.norm_def]
case e_a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ∫⁻ (a : α), ↑‖↑↑(Lp.posPart f₁) a‖₊ ∂μ
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑(Lp.posPart f₁) a‖₊ ∂μ)
congr 1
case e_a.h
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
⊢ (fun a => ENNReal.ofReal (f a)) =ᵐ[μ] fun a => ↑‖↑↑(Lp.posPart f₁) a‖₊
case e_a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ∫⁻ (a : α), ↑‖↑↑(Lp.posPart f₁) a‖₊ ∂μ
apply lintegral_congr_ae
case h
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart (Integrable.toL1 f hf)) a✝ = max (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ENNReal.ofReal (f a✝) = ↑‖↑↑(Lp.posPart (Integrable.toL1 f hf)) a✝‖₊
case e_a.h
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
⊢ (fun a => ENNReal.ofReal (f a)) =ᵐ[μ] fun a => ↑‖↑↑(Lp.posPart f₁) a‖₊
filter_upwards [Lp.coeFn_posPart f₁, hf.coeFn_toL1]with _ h₁ h₂
case h
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart (Integrable.toL1 f hf)) a✝ = max (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(Real.toNNReal (f a✝)) = ↑‖max (f a✝) 0‖₊
case h
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart (Integrable.toL1 f hf)) a✝ = max (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ENNReal.ofReal (f a✝) = ↑‖↑↑(Lp.posPart (Integrable.toL1 f hf)) a✝‖₊
rw [h₁, h₂, ENNReal.ofReal]
case h.e_a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart (Integrable.toL1 f hf)) a✝ = max (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ Real.toNNReal (f a✝) = ‖max (f a✝) 0‖₊
case h
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart (Integrable.toL1 f hf)) a✝ = max (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(Real.toNNReal (f a✝)) = ↑‖max (f a✝) 0‖₊
congr 1
case h.e_a.a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart (Integrable.toL1 f hf)) a✝ = max (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(Real.toNNReal (f a✝)) = ↑‖max (f a✝) 0‖₊
case h.e_a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart (Integrable.toL1 f hf)) a✝ = max (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ Real.toNNReal (f a✝) = ‖max (f a✝) 0‖₊
apply NNReal.eq
case h.e_a.a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart (Integrable.toL1 f hf)) a✝ = max (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(Real.toNNReal (f a✝)) = ↑{ val := max (f a✝) 0, property := (_ : 0 ≤ max (f a✝) 0) }
case h.e_a.a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart (Integrable.toL1 f hf)) a✝ = max (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(Real.toNNReal (f a✝)) = ↑‖max (f a✝) 0‖₊
rw [Real.nnnorm_of_nonneg (le_max_right _ _)]
no goals
case h.e_a.a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart (Integrable.toL1 f hf)) a✝ = max (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(Real.toNNReal (f a✝)) = ↑{ val := max (f a✝) 0, property := (_ : 0 ≤ max (f a✝) 0) }
rw [Real.coe_toNNReal', NNReal.coe_mk]
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ) = ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑(Lp.negPart f₁) a‖₊ ∂μ)
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ) = ‖Lp.negPart f₁‖
rw [L1.norm_def]
case e_a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
⊢ (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ) = ∫⁻ (a : α), ↑‖↑↑(Lp.negPart f₁) a‖₊ ∂μ
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ) = ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑(Lp.negPart f₁) a‖₊ ∂μ)
congr 1
case e_a.h
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
⊢ (fun a => ENNReal.ofReal (-f a)) =ᵐ[μ] fun a => ↑‖↑↑(Lp.negPart f₁) a‖₊
case e_a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
⊢ (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ) = ∫⁻ (a : α), ↑‖↑↑(Lp.negPart f₁) a‖₊ ∂μ
apply lintegral_congr_ae
case h
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart (Integrable.toL1 f hf)) a✝ = -min (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ENNReal.ofReal (-f a✝) = ↑‖↑↑(Lp.negPart (Integrable.toL1 f hf)) a✝‖₊
case e_a.h
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
⊢ (fun a => ENNReal.ofReal (-f a)) =ᵐ[μ] fun a => ↑‖↑↑(Lp.negPart f₁) a‖₊
filter_upwards [Lp.coeFn_negPart f₁, hf.coeFn_toL1]with _ h₁ h₂
case h
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart (Integrable.toL1 f hf)) a✝ = -min (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(Real.toNNReal (-f a✝)) = ↑‖-min (f a✝) 0‖₊
case h
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart (Integrable.toL1 f hf)) a✝ = -min (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ENNReal.ofReal (-f a✝) = ↑‖↑↑(Lp.negPart (Integrable.toL1 f hf)) a✝‖₊
rw [h₁, h₂, ENNReal.ofReal]
case h.e_a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart (Integrable.toL1 f hf)) a✝ = -min (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ Real.toNNReal (-f a✝) = ‖-min (f a✝) 0‖₊
case h
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart (Integrable.toL1 f hf)) a✝ = -min (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(Real.toNNReal (-f a✝)) = ↑‖-min (f a✝) 0‖₊
congr 1
case h.e_a.a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart (Integrable.toL1 f hf)) a✝ = -min (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(Real.toNNReal (-f a✝)) = ↑‖-min (f a✝) 0‖₊
case h.e_a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart (Integrable.toL1 f hf)) a✝ = -min (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ Real.toNNReal (-f a✝) = ‖-min (f a✝) 0‖₊
apply NNReal.eq
case h.e_a.a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart (Integrable.toL1 f hf)) a✝ = -min (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ max (-f a✝) 0 = ‖min (f a✝) 0‖
case h.e_a.a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart (Integrable.toL1 f hf)) a✝ = -min (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(Real.toNNReal (-f a✝)) = ↑‖-min (f a✝) 0‖₊
simp only [Real.coe_toNNReal', coe_nnnorm, nnnorm_neg]
no goals
case h.e_a.a
α : Type u_1
E : Type ?u.1037517
F : Type ?u.1037520
𝕜 : Type ?u.1037523
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1040214
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : Integrable f
f₁ : { x // x ∈ Lp ℝ 1 } := Integrable.toL1 f hf
eq₁ : ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart (Integrable.toL1 f hf)) a✝ = -min (↑↑(Integrable.toL1 f hf) a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ max (-f a✝) 0 = ‖min (f a✝) 0‖
rw [Real.norm_of_nonpos (min_le_right _ _), ← max_neg_neg, neg_zero]