α : Type u_1
β : Type ?u.295320
γ : Type ?u.295323
δ : Type ?u.295326
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
⊢ (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ≤ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ
α : Type u_1
β : Type ?u.295320
γ : Type ?u.295323
δ : Type ?u.295326
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
⊢ (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ≤ ∫⁻ (x : α), ↑‖f x‖₊ ∂μ
simp_rw [← ofReal_norm_eq_coe_nnnorm]
α : Type u_1
β : Type ?u.295320
γ : Type ?u.295323
δ : Type ?u.295326
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
x : α
⊢ f x ≤ ‖f x‖
α : Type u_1
β : Type ?u.295320
γ : Type ?u.295323
δ : Type ?u.295326
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
⊢ (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ≤ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ
refine' lintegral_mono fun x => ENNReal.ofReal_le_ofReal _
α : Type u_1
β : Type ?u.295320
γ : Type ?u.295323
δ : Type ?u.295326
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
x : α
⊢ f x ≤ abs (f x)
α : Type u_1
β : Type ?u.295320
γ : Type ?u.295323
δ : Type ?u.295326
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
x : α
⊢ f x ≤ ‖f x‖
rw [Real.norm_eq_abs]
no goals
α : Type u_1
β : Type ?u.295320
γ : Type ?u.295323
δ : Type ?u.295326
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
x : α
⊢ f x ≤ abs (f x)
exact le_abs_self (f x)