α : Type u_2
β : Type u_1
γ : Type ?u.1315289
δ : Type ?u.1315292
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
⊢ ENNReal.toReal (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) = ENNReal.toReal (∫⁻ (a : α), edist (f a) 0 ∂μ)
α : Type u_2
β : Type u_1
γ : Type ?u.1315289
δ : Type ?u.1315292
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
⊢ ‖toL1 f hf‖ = ENNReal.toReal (∫⁻ (a : α), edist (f a) 0 ∂μ)
simp [toL1, snorm, snorm']
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1315289
δ : Type ?u.1315292
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
⊢ ENNReal.toReal (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) = ENNReal.toReal (∫⁻ (a : α), edist (f a) 0 ∂μ)
simp [edist_eq_coe_nnnorm]