α : Type u_1
β : Type ?u.4410
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun μ =>
    ⨆ (n : ℕ),
      ∑ x in SimpleFunc.range (SimpleFunc.eapprox (fun x => f x) n),
        x * ↑↑μ (↑(SimpleFunc.eapprox (fun x => f x) n) ⁻¹' {x})
α : Type u_1
β : Type ?u.4410
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun μ => ∫⁻ (x : α), f x ∂μ
simp only [lintegral_eq_iSup_eapprox_lintegral, hf, SimpleFunc.lintegral]
α : Type u_1
β : Type ?u.4410
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
x✝ : i ∈ SimpleFunc.range (SimpleFunc.eapprox (fun x => f x) n)
⊢ Measurable fun μ => i * ↑↑μ (↑(SimpleFunc.eapprox (fun x => f x) n) ⁻¹' {i})
α : Type u_1
β : Type ?u.4410
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun μ =>
    ⨆ (n : ℕ),
      ∑ x in SimpleFunc.range (SimpleFunc.eapprox (fun x => f x) n),
        x * ↑↑μ (↑(SimpleFunc.eapprox (fun x => f x) n) ⁻¹' {x})
refine' measurable_iSup fun n => Finset.measurable_sum _ fun i _ => _
α : Type u_1
β : Type ?u.4410
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
x✝ : i ∈ SimpleFunc.range (SimpleFunc.eapprox (fun x => f x) n)
⊢ Measurable fun μ => ↑↑μ (↑(SimpleFunc.eapprox (fun x => f x) n) ⁻¹' {i})
α : Type u_1
β : Type ?u.4410
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
x✝ : i ∈ SimpleFunc.range (SimpleFunc.eapprox (fun x => f x) n)
⊢ Measurable fun μ => i * ↑↑μ (↑(SimpleFunc.eapprox (fun x => f x) n) ⁻¹' {i})
refine' Measurable.const_mul _ _
no goals
α : Type u_1
β : Type ?u.4410
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
x✝ : i ∈ SimpleFunc.range (SimpleFunc.eapprox (fun x => f x) n)
⊢ Measurable fun μ => ↑↑μ (↑(SimpleFunc.eapprox (fun x => f x) n) ⁻¹' {i})
exact measurable_coe ((SimpleFunc.eapprox f n).measurableSet_preimage _)