case e_f
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun a => r * f a) = fun a => ⨆ (n : ℕ), ↑(const α r * eapprox f n) a
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ (∫⁻ (a : α), r * f a ∂μ) = ∫⁻ (a : α), ⨆ (n : ℕ), ↑(const α r * eapprox f n) a ∂μ
congr
case e_f.h
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ r * f a = ⨆ (n : ℕ), ↑(const α r * eapprox f n) a
case e_f
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun a => r * f a) = fun a => ⨆ (n : ℕ), ↑(const α r * eapprox f n) a
funext a
case e_f.h
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ (⨆ (i : ℕ), r * ↑(eapprox f i) a) = ⨆ (n : ℕ), ↑(const α r * eapprox f n) a
case e_f.h
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ r * f a = ⨆ (n : ℕ), ↑(const α r * eapprox f n) a
rw [← iSup_eapprox_apply f hf, ENNReal.mul_iSup]
no goals
case e_f.h
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ (⨆ (i : ℕ), r * ↑(eapprox f i) a) = ⨆ (n : ℕ), ↑(const α r * eapprox f n) a
rfl
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ (⨆ (n : ℕ), ∫⁻ (a : α), ↑(const α r * eapprox f n) a ∂μ) = ⨆ (n : ℕ), r * SimpleFunc.lintegral (eapprox f n) μ

case hf
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), Measurable fun a => ↑(const α r * eapprox f n) a

case h_mono
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ Monotone fun n a => ↑(const α r * eapprox f n) a
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ (∫⁻ (a : α), ⨆ (n : ℕ), ↑(const α r * eapprox f n) a ∂μ) = ⨆ (n : ℕ), r * SimpleFunc.lintegral (eapprox f n) μ
rw [lintegral_iSup]
case e_s
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun n => ∫⁻ (a : α), ↑(const α r * eapprox f n) a ∂μ) = fun n => r * SimpleFunc.lintegral (eapprox f n) μ
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ (⨆ (n : ℕ), ∫⁻ (a : α), ↑(const α r * eapprox f n) a ∂μ) = ⨆ (n : ℕ), r * SimpleFunc.lintegral (eapprox f n) μ
congr
case e_s.h
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ (∫⁻ (a : α), ↑(const α r * eapprox f n) a ∂μ) = r * SimpleFunc.lintegral (eapprox f n) μ
case e_s
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun n => ∫⁻ (a : α), ↑(const α r * eapprox f n) a ∂μ) = fun n => r * SimpleFunc.lintegral (eapprox f n) μ
funext n
no goals
case e_s.h
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ (∫⁻ (a : α), ↑(const α r * eapprox f n) a ∂μ) = r * SimpleFunc.lintegral (eapprox f n) μ
rw [← SimpleFunc.const_mul_lintegral, ← SimpleFunc.lintegral_eq_lintegral]
case hf
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ Measurable fun a => ↑(const α r * eapprox f n) a
case hf
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), Measurable fun a => ↑(const α r * eapprox f n) a
intro n
no goals
case hf
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ Measurable fun a => ↑(const α r * eapprox f n) a
exact SimpleFunc.measurable _
case h_mono
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
i j : ℕ
h : i ≤ j
a : α
⊢ (fun n a => ↑(const α r * eapprox f n) a) i a ≤ (fun n a => ↑(const α r * eapprox f n) a) j a
case h_mono
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ Monotone fun n a => ↑(const α r * eapprox f n) a
intro i j h a
no goals
case h_mono
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
i j : ℕ
h : i ≤ j
a : α
⊢ (fun n a => ↑(const α r * eapprox f n) a) i a ≤ (fun n a => ↑(const α r * eapprox f n) a) j a
exact mul_le_mul_left' (monotone_eapprox _ h _) _
no goals
α : Type u_1
β : Type ?u.933531
γ : Type ?u.933534
δ : Type ?u.933537
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ (⨆ (n : ℕ), r * SimpleFunc.lintegral (eapprox f n) μ) = r * ∫⁻ (a : α), f a ∂μ
rw [← ENNReal.mul_iSup, lintegral_eq_iSup_eapprox_lintegral hf]