case intro
α : Type u_1
β : Type ?u.1746843
γ : Type ?u.1746846
δ : Type ?u.1746849
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
f : α → ℝ≥0
hf : Measurable f
M : ℝ≥0
hM : M ∈ upperBounds (f '' s)
⊢ (∫⁻ (x : α) in s, ↑(f x) ∂μ) < ⊤
α : Type u_1
β : Type ?u.1746843
γ : Type ?u.1746846
δ : Type ?u.1746849
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
f : α → ℝ≥0
hf : Measurable f
hbdd : BddAbove (f '' s)
⊢ (∫⁻ (x : α) in s, ↑(f x) ∂μ) < ⊤
obtain ⟨M, hM⟩ := hbdd
case intro
α : Type u_1
β : Type ?u.1746843
γ : Type ?u.1746846
δ : Type ?u.1746849
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
f : α → ℝ≥0
hf : Measurable f
M : ℝ≥0
hM : ∀ (x : ℝ≥0), x ∈ f '' s → x ≤ M
⊢ (∫⁻ (x : α) in s, ↑(f x) ∂μ) < ⊤
case intro
α : Type u_1
β : Type ?u.1746843
γ : Type ?u.1746846
δ : Type ?u.1746849
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
f : α → ℝ≥0
hf : Measurable f
M : ℝ≥0
hM : M ∈ upperBounds (f '' s)
⊢ (∫⁻ (x : α) in s, ↑(f x) ∂μ) < ⊤
rw [mem_upperBounds] at hM
case intro.refine'_1
α : Type u_1
β : Type ?u.1746843
γ : Type ?u.1746846
δ : Type ?u.1746849
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
f : α → ℝ≥0
hf : Measurable f
M : ℝ≥0
hM : ∀ (x : ℝ≥0), x ∈ f '' s → x ≤ M
⊢ ∀ (x : α), x ∈ s → ↑(f x) ≤ ↑M

case intro.refine'_2
α : Type u_1
β : Type ?u.1746843
γ : Type ?u.1746846
δ : Type ?u.1746849
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
f : α → ℝ≥0
hf : Measurable f
M : ℝ≥0
hM : ∀ (x : ℝ≥0), x ∈ f '' s → x ≤ M
⊢ (∫⁻ (x : α) in s, ↑M ∂μ) < ⊤
case intro
α : Type u_1
β : Type ?u.1746843
γ : Type ?u.1746846
δ : Type ?u.1746849
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
f : α → ℝ≥0
hf : Measurable f
M : ℝ≥0
hM : ∀ (x : ℝ≥0), x ∈ f '' s → x ≤ M
⊢ (∫⁻ (x : α) in s, ↑(f x) ∂μ) < ⊤
refine'
  lt_of_le_of_lt (set_lintegral_mono hf.coe_nnreal_ennreal (@measurable_const _ _ _ _ ↑M) _) _
no goals
case intro.refine'_1
α : Type u_1
β : Type ?u.1746843
γ : Type ?u.1746846
δ : Type ?u.1746849
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
f : α → ℝ≥0
hf : Measurable f
M : ℝ≥0
hM : ∀ (x : ℝ≥0), x ∈ f '' s → x ≤ M
⊢ ∀ (x : α), x ∈ s → ↑(f x) ≤ ↑M
simpa using hM
case intro.refine'_2
α : Type u_1
β : Type ?u.1746843
γ : Type ?u.1746846
δ : Type ?u.1746849
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
f : α → ℝ≥0
hf : Measurable f
M : ℝ≥0
hM : ∀ (x : ℝ≥0), x ∈ f '' s → x ≤ M
⊢ ↑M * ↑↑(Measure.restrict μ s) univ < ⊤
case intro.refine'_2
α : Type u_1
β : Type ?u.1746843
γ : Type ?u.1746846
δ : Type ?u.1746849
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
f : α → ℝ≥0
hf : Measurable f
M : ℝ≥0
hM : ∀ (x : ℝ≥0), x ∈ f '' s → x ≤ M
⊢ (∫⁻ (x : α) in s, ↑M ∂μ) < ⊤
rw [lintegral_const]
case intro.refine'_2
α : Type u_1
β : Type ?u.1746843
γ : Type ?u.1746846
δ : Type ?u.1746849
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
f : α → ℝ≥0
hf : Measurable f
M : ℝ≥0
hM : ∀ (x : ℝ≥0), x ∈ f '' s → x ≤ M
⊢ ↑↑(Measure.restrict μ s) univ ≠ ⊤
case intro.refine'_2
α : Type u_1
β : Type ?u.1746843
γ : Type ?u.1746846
δ : Type ?u.1746849
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
f : α → ℝ≥0
hf : Measurable f
M : ℝ≥0
hM : ∀ (x : ℝ≥0), x ∈ f '' s → x ≤ M
⊢ ↑M * ↑↑(Measure.restrict μ s) univ < ⊤
refine' ENNReal.mul_lt_top ENNReal.coe_lt_top.ne _
no goals
case intro.refine'_2
α : Type u_1
β : Type ?u.1746843
γ : Type ?u.1746846
δ : Type ?u.1746849
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
f : α → ℝ≥0
hf : Measurable f
M : ℝ≥0
hM : ∀ (x : ℝ≥0), x ∈ f '' s → x ≤ M
⊢ ↑↑(Measure.restrict μ s) univ ≠ ⊤
simp [hs]