case h
α : Type u_1
β : Type ?u.296013
γ : Type ?u.296016
δ : Type ?u.296019
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᵐ[μ] f
⊢ (fun a => ↑‖f a‖₊) =ᵐ[μ] fun a => ENNReal.ofReal (f a)
α : Type u_1
β : Type ?u.296013
γ : Type ?u.296016
δ : Type ?u.296019
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᵐ[μ] f
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
apply lintegral_congr_ae
case h
α : Type u_1
β : Type ?u.296013
γ : Type ?u.296016
δ : Type ?u.296019
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᵐ[μ] f
x : α
hx : OfNat.ofNat 0 x ≤ f x
⊢ ↑‖f x‖₊ = ENNReal.ofReal (f x)
case h
α : Type u_1
β : Type ?u.296013
γ : Type ?u.296016
δ : Type ?u.296019
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᵐ[μ] f
⊢ (fun a => ↑‖f a‖₊) =ᵐ[μ] fun a => ENNReal.ofReal (f a)
filter_upwards [h_nonneg]with x hx
no goals
case h
α : Type u_1
β : Type ?u.296013
γ : Type ?u.296016
δ : Type ?u.296019
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᵐ[μ] f
x : α
hx : OfNat.ofNat 0 x ≤ f x
⊢ ↑‖f x‖₊ = ENNReal.ofReal (f x)
rw [Real.nnnorm_of_nonneg hx, ENNReal.ofReal_eq_coe_nnreal hx]