case e_f
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun a => f a) = fun a => ⨆ (n : ℕ), ↑(eapprox f n) a
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), ⨆ (n : ℕ), ↑(eapprox f n) a ∂μ
congr
case e_f.h
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ f a = ⨆ (n : ℕ), ↑(eapprox f n) a
case e_f
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun a => f a) = fun a => ⨆ (n : ℕ), ↑(eapprox f n) a
ext a
no goals
case e_f.h
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ f a = ⨆ (n : ℕ), ↑(eapprox f n) a
rw [iSup_eapprox_apply f hf]
case hf
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), Measurable fun a => ↑(eapprox f n) a

case h_mono
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Monotone fun n a => ↑(eapprox f n) a
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (∫⁻ (a : α), ⨆ (n : ℕ), ↑(eapprox f n) a ∂μ) = ⨆ (n : ℕ), ∫⁻ (a : α), ↑(eapprox f n) a ∂μ
rw [lintegral_iSup]
no goals
case hf
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), Measurable fun a => ↑(eapprox f n) a
measurability
case h_mono
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
i j : ℕ
h : i ≤ j
⊢ (fun n a => ↑(eapprox f n) a) i ≤ (fun n a => ↑(eapprox f n) a) j
case h_mono
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Monotone fun n a => ↑(eapprox f n) a
intro i j h
no goals
case h_mono
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
i j : ℕ
h : i ≤ j
⊢ (fun n a => ↑(eapprox f n) a) i ≤ (fun n a => ↑(eapprox f n) a) j
exact monotone_eapprox f h
case e_s
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun n => ∫⁻ (a : α), ↑(eapprox f n) a ∂μ) = fun n => SimpleFunc.lintegral (eapprox f n) μ
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (⨆ (n : ℕ), ∫⁻ (a : α), ↑(eapprox f n) a ∂μ) = ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ
congr
case e_s.h
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ (∫⁻ (a : α), ↑(eapprox f n) a ∂μ) = SimpleFunc.lintegral (eapprox f n) μ
case e_s
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun n => ∫⁻ (a : α), ↑(eapprox f n) a ∂μ) = fun n => SimpleFunc.lintegral (eapprox f n) μ
ext n
no goals
case e_s.h
α : Type u_1
β : Type ?u.485014
γ : Type ?u.485017
δ : Type ?u.485020
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ (∫⁻ (a : α), ↑(eapprox f n) a ∂μ) = SimpleFunc.lintegral (eapprox f n) μ
rw [(eapprox f n).lintegral_eq_lintegral]