α : Type u_1
β : Type ?u.935860
γ : Type ?u.935863
δ : Type ?u.935866
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
⊢ (⨆ (i : α →ₛ ℝ≥0∞), r * ⨆ (_ : ↑i ≤ fun a => f a), SimpleFunc.lintegral i μ) ≤ ∫⁻ (a : α), r * f a ∂μ
α : Type u_1
β : Type ?u.935860
γ : Type ?u.935863
δ : Type ?u.935866
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
⊢ (r * ∫⁻ (a : α), f a ∂μ) ≤ ∫⁻ (a : α), r * f a ∂μ
rw [lintegral, ENNReal.mul_iSup]
α : Type u_1
β : Type ?u.935860
γ : Type ?u.935863
δ : Type ?u.935866
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
⊢ (r * ⨆ (_ : ↑s ≤ fun a => f a), SimpleFunc.lintegral s μ) ≤ ∫⁻ (a : α), r * f a ∂μ
α : Type u_1
β : Type ?u.935860
γ : Type ?u.935863
δ : Type ?u.935866
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
⊢ (⨆ (i : α →ₛ ℝ≥0∞), r * ⨆ (_ : ↑i ≤ fun a => f a), SimpleFunc.lintegral i μ) ≤ ∫⁻ (a : α), r * f a ∂μ
refine' iSup_le fun s => _
α : Type u_1
β : Type ?u.935860
γ : Type ?u.935863
δ : Type ?u.935866
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
⊢ (⨆ (_ : ↑s ≤ fun a => f a), r * SimpleFunc.lintegral s μ) ≤ ∫⁻ (a : α), r * f a ∂μ
α : Type u_1
β : Type ?u.935860
γ : Type ?u.935863
δ : Type ?u.935866
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
⊢ (r * ⨆ (_ : ↑s ≤ fun a => f a), SimpleFunc.lintegral s μ) ≤ ∫⁻ (a : α), r * f a ∂μ
rw [ENNReal.mul_iSup]
α : Type u_1
β : Type ?u.935860
γ : Type ?u.935863
δ : Type ?u.935866
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
⊢ (↑s ≤ fun a => f a) → r * SimpleFunc.lintegral s μ ≤ ∫⁻ (a : α), r * f a ∂μ
α : Type u_1
β : Type ?u.935860
γ : Type ?u.935863
δ : Type ?u.935866
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
⊢ (⨆ (_ : ↑s ≤ fun a => f a), r * SimpleFunc.lintegral s μ) ≤ ∫⁻ (a : α), r * f a ∂μ
simp only [iSup_le_iff]
α : Type u_1
β : Type ?u.935860
γ : Type ?u.935863
δ : Type ?u.935866
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : ↑s ≤ fun a => f a
⊢ r * SimpleFunc.lintegral s μ ≤ ∫⁻ (a : α), r * f a ∂μ
α : Type u_1
β : Type ?u.935860
γ : Type ?u.935863
δ : Type ?u.935866
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
⊢ (↑s ≤ fun a => f a) → r * SimpleFunc.lintegral s μ ≤ ∫⁻ (a : α), r * f a ∂μ
intro hs
α : Type u_1
β : Type ?u.935860
γ : Type ?u.935863
δ : Type ?u.935866
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : ↑s ≤ fun a => f a
⊢ SimpleFunc.lintegral (const α r * s) μ ≤ ⨆ (g : α →ₛ ℝ≥0∞) (_ : ↑g ≤ fun a => r * f a), SimpleFunc.lintegral g μ
α : Type u_1
β : Type ?u.935860
γ : Type ?u.935863
δ : Type ?u.935866
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : ↑s ≤ fun a => f a
⊢ r * SimpleFunc.lintegral s μ ≤ ∫⁻ (a : α), r * f a ∂μ
rw [← SimpleFunc.const_mul_lintegral, lintegral]
α : Type u_1
β : Type ?u.935860
γ : Type ?u.935863
δ : Type ?u.935866
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : ↑s ≤ fun a => f a
x : α
⊢ ↑(const α r * s) x ≤ (fun a => r * f a) x
α : Type u_1
β : Type ?u.935860
γ : Type ?u.935863
δ : Type ?u.935866
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : ↑s ≤ fun a => f a
⊢ SimpleFunc.lintegral (const α r * s) μ ≤ ⨆ (g : α →ₛ ℝ≥0∞) (_ : ↑g ≤ fun a => r * f a), SimpleFunc.lintegral g μ
refine' le_iSup_of_le (const α r * s) (le_iSup_of_le (fun x => _) le_rfl)
no goals
α : Type u_1
β : Type ?u.935860
γ : Type ?u.935863
δ : Type ?u.935866
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : ↑s ≤ fun a => f a
x : α
⊢ ↑(const α r * s) x ≤ (fun a => r * f a) x
exact mul_le_mul_left' (hs x) _