α : Type u_1
E : Type ?u.1125327
F : Type ?u.1125330
𝕜 : Type ?u.1125333
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.1128024
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_2
inst✝ : NormedAddCommGroup H
f : { x // x ∈ Lp H 1 }
⊢ ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑f a‖₊ ∂μ) = ∫ (a : α), ‖↑↑f a‖ ∂μ
α : Type u_1
E : Type ?u.1125327
F : Type ?u.1125330
𝕜 : Type ?u.1125333
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.1128024
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_2
inst✝ : NormedAddCommGroup H
f : { x // x ∈ Lp H 1 }
⊢ ‖f‖ = ∫ (a : α), ‖↑↑f a‖ ∂μ
simp only [snorm, snorm', ENNReal.one_toReal, ENNReal.rpow_one, Lp.norm_def, if_false,
  ENNReal.one_ne_top, one_ne_zero, _root_.div_one]
α : Type u_1
E : Type ?u.1125327
F : Type ?u.1125330
𝕜 : Type ?u.1125333
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.1128024
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_2
inst✝ : NormedAddCommGroup H
f : { x // x ∈ Lp H 1 }
⊢ ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑f a‖₊ ∂μ) = ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ‖↑↑f a‖ ∂μ)
α : Type u_1
E : Type ?u.1125327
F : Type ?u.1125330
𝕜 : Type ?u.1125333
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.1128024
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_2
inst✝ : NormedAddCommGroup H
f : { x // x ∈ Lp H 1 }
⊢ ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑f a‖₊ ∂μ) = ∫ (a : α), ‖↑↑f a‖ ∂μ
rw [integral_eq_lintegral_of_nonneg_ae (eventually_of_forall (by simp [norm_nonneg]))
    (Lp.aestronglyMeasurable f).norm]
no goals
α : Type u_1
E : Type ?u.1125327
F : Type ?u.1125330
𝕜 : Type ?u.1125333
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.1128024
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_2
inst✝ : NormedAddCommGroup H
f : { x // x ∈ Lp H 1 }
⊢ ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑f a‖₊ ∂μ) = ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ‖↑↑f a‖ ∂μ)
simp [ofReal_norm_eq_coe_nnnorm]
no goals
α : Type u_1
E : Type ?u.1125327
F : Type ?u.1125330
𝕜 : Type ?u.1125333
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.1128024
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_2
inst✝ : NormedAddCommGroup H
f : { x // x ∈ Lp H 1 }
⊢ ∀ (x : α), OfNat.ofNat 0 x ≤ ‖↑↑f x‖
simp [norm_nonneg]