no goals
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ (∫⁻ (a : α), f a + g a ∂μ) = ∫⁻ (a : α), (⨆ (n : ℕ), ↑(eapprox f n) a) + ⨆ (n : ℕ), ↑(eapprox g n) a ∂μ
simp only [iSup_eapprox_apply, hf, hg]
case e_f
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ (fun a => (⨆ (n : ℕ), ↑(eapprox f n) a) + ⨆ (n : ℕ), ↑(eapprox g n) a) = fun a =>
    ⨆ (n : ℕ), (↑(eapprox f n) + ↑(eapprox g n)) a
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ (∫⁻ (a : α), (⨆ (n : ℕ), ↑(eapprox f n) a) + ⨆ (n : ℕ), ↑(eapprox g n) a ∂μ) =
    ∫⁻ (a : α), ⨆ (n : ℕ), (↑(eapprox f n) + ↑(eapprox g n)) a ∂μ
congr
case e_f.h
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ ((⨆ (n : ℕ), ↑(eapprox f n) a) + ⨆ (n : ℕ), ↑(eapprox g n) a) = ⨆ (n : ℕ), (↑(eapprox f n) + ↑(eapprox g n)) a
case e_f
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ (fun a => (⨆ (n : ℕ), ↑(eapprox f n) a) + ⨆ (n : ℕ), ↑(eapprox g n) a) = fun a =>
    ⨆ (n : ℕ), (↑(eapprox f n) + ↑(eapprox g n)) a
funext a
case e_f.h
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ (⨆ (a_1 : ℕ), ↑(eapprox f a_1) a + ↑(eapprox g a_1) a) = ⨆ (n : ℕ), (↑(eapprox f n) + ↑(eapprox g n)) a

case e_f.h.hf
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ Monotone fun n => ↑(eapprox f n) a

case e_f.h.hg
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ Monotone fun n => ↑(eapprox g n) a
case e_f.h
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ ((⨆ (n : ℕ), ↑(eapprox f n) a) + ⨆ (n : ℕ), ↑(eapprox g n) a) = ⨆ (n : ℕ), (↑(eapprox f n) + ↑(eapprox g n)) a
rw [ENNReal.iSup_add_iSup_of_monotone]
no goals
case e_f.h
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ (⨆ (a_1 : ℕ), ↑(eapprox f a_1) a + ↑(eapprox g a_1) a) = ⨆ (n : ℕ), (↑(eapprox f n) + ↑(eapprox g n)) a
rfl
case e_f.h.hf
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
i j : ℕ
h : i ≤ j
⊢ (fun n => ↑(eapprox f n) a) i ≤ (fun n => ↑(eapprox f n) a) j
case e_f.h.hf
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ Monotone fun n => ↑(eapprox f n) a
intro i j h
no goals
case e_f.h.hf
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
i j : ℕ
h : i ≤ j
⊢ (fun n => ↑(eapprox f n) a) i ≤ (fun n => ↑(eapprox f n) a) j
exact monotone_eapprox _ h a
case e_f.h.hg
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
i j : ℕ
h : i ≤ j
⊢ (fun n => ↑(eapprox g n) a) i ≤ (fun n => ↑(eapprox g n) a) j
case e_f.h.hg
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ Monotone fun n => ↑(eapprox g n) a
intro i j h
no goals
case e_f.h.hg
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
i j : ℕ
h : i ≤ j
⊢ (fun n => ↑(eapprox g n) a) i ≤ (fun n => ↑(eapprox g n) a) j
exact monotone_eapprox _ h a
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ (⨆ (n : ℕ), ∫⁻ (a : α), (↑(eapprox f n) + ↑(eapprox g n)) a ∂μ) =
    ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ + SimpleFunc.lintegral (eapprox g n) μ

case hf
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ ∀ (n : ℕ), Measurable fun a => (↑(eapprox f n) + ↑(eapprox g n)) a

case h_mono
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ Monotone fun n a => (↑(eapprox f n) + ↑(eapprox g n)) a
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ (∫⁻ (a : α), ⨆ (n : ℕ), (↑(eapprox f n) + ↑(eapprox g n)) a ∂μ) =
    ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ + SimpleFunc.lintegral (eapprox g n) μ
rw [lintegral_iSup]
case e_s
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ (fun n => ∫⁻ (a : α), (↑(eapprox f n) + ↑(eapprox g n)) a ∂μ) = fun n =>
    SimpleFunc.lintegral (eapprox f n) μ + SimpleFunc.lintegral (eapprox g n) μ
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ (⨆ (n : ℕ), ∫⁻ (a : α), (↑(eapprox f n) + ↑(eapprox g n)) a ∂μ) =
    ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ + SimpleFunc.lintegral (eapprox g n) μ
congr
case e_s.h
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ (∫⁻ (a : α), (↑(eapprox f n) + ↑(eapprox g n)) a ∂μ) =
    SimpleFunc.lintegral (eapprox f n) μ + SimpleFunc.lintegral (eapprox g n) μ
case e_s
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ (fun n => ∫⁻ (a : α), (↑(eapprox f n) + ↑(eapprox g n)) a ∂μ) = fun n =>
    SimpleFunc.lintegral (eapprox f n) μ + SimpleFunc.lintegral (eapprox g n) μ
funext n
case e_s.h
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ (∫⁻ (a : α), (↑(eapprox f n) + ↑(eapprox g n)) a ∂μ) = ∫⁻ (a : α), ↑(eapprox f n + eapprox g n) a ∂μ
case e_s.h
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ (∫⁻ (a : α), (↑(eapprox f n) + ↑(eapprox g n)) a ∂μ) =
    SimpleFunc.lintegral (eapprox f n) μ + SimpleFunc.lintegral (eapprox g n) μ
rw [← SimpleFunc.add_lintegral, ← SimpleFunc.lintegral_eq_lintegral]
no goals
case e_s.h
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ (∫⁻ (a : α), (↑(eapprox f n) + ↑(eapprox g n)) a ∂μ) = ∫⁻ (a : α), ↑(eapprox f n + eapprox g n) a ∂μ
rfl
no goals
case hf
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ ∀ (n : ℕ), Measurable fun a => (↑(eapprox f n) + ↑(eapprox g n)) a
measurability
case h_mono
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
i j : ℕ
h : i ≤ j
a : α
⊢ (fun n a => (↑(eapprox f n) + ↑(eapprox g n)) a) i a ≤ (fun n a => (↑(eapprox f n) + ↑(eapprox g n)) a) j a
case h_mono
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ Monotone fun n a => (↑(eapprox f n) + ↑(eapprox g n)) a
intro i j h a
no goals
case h_mono
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
i j : ℕ
h : i ≤ j
a : α
⊢ (fun n a => (↑(eapprox f n) + ↑(eapprox g n)) a) i a ≤ (fun n a => (↑(eapprox f n) + ↑(eapprox g n)) a) j a
exact add_le_add (monotone_eapprox _ h _) (monotone_eapprox _ h _)
case refine'_2
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
i j : ℕ
h : i ≤ j
⊢ (fun n => SimpleFunc.lintegral (eapprox g n) μ) i ≤ (fun n => SimpleFunc.lintegral (eapprox g n) μ) j
case refine'_2
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ Monotone fun n => SimpleFunc.lintegral (eapprox g n) μ
intro i j h
no goals
case refine'_2
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
i j : ℕ
h : i ≤ j
⊢ (fun n => SimpleFunc.lintegral (eapprox g n) μ) i ≤ (fun n => SimpleFunc.lintegral (eapprox g n) μ) j
exact SimpleFunc.lintegral_mono (monotone_eapprox _ h) (le_refl μ)
no goals
α : Type u_1
β : Type ?u.853934
γ : Type ?u.853937
δ : Type ?u.853940
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ ((⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ) + ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox g n) μ) =
    (∫⁻ (a : α), f a ∂μ) + ∫⁻ (a : α), g a ∂μ
rw [lintegral_eq_iSup_eapprox_lintegral hf, lintegral_eq_iSup_eapprox_lintegral hg]