case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), ↑fs x ≤ f x
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ε
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ε
obtain ⟨fs, fs_le_f, int_fs⟩ :
  ∃ fs : α →ₛ ℝ≥0, (∀ x, fs x ≤ f x) ∧ (∫⁻ x, f x ∂μ) ≤ (∫⁻ x, fs x ∂μ) + ε / 2 := by
  have aux := ENNReal.lt_add_right int_f (ENNReal.half_pos ε0).ne'
  conv_rhs at aux => rw [lintegral_eq_nnreal (fun x => (f x : ℝ≥0∞)) μ]
  erw [ENNReal.biSup_add] at aux  <;> [skip; exact ⟨0, fun x => by simp⟩]
  simp only [lt_iSup_iff] at aux
  rcases aux with ⟨fs, fs_le_f, int_fs⟩
  refine' ⟨fs, fun x => by simpa only [ENNReal.coe_le_coe] using fs_le_f x, _⟩
  convert int_fs.le
  rw [← SimpleFunc.lintegral_eq_lintegral]
  rfl
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), ↑fs x ≤ f x
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
int_fs_lt_top : (∫⁻ (x : α), ↑(↑fs x) ∂μ) ≠ ⊤
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ε
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), ↑fs x ≤ f x
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ε
have int_fs_lt_top : (∫⁻ x, fs x ∂μ) ≠ ∞ := by
  refine' ne_top_of_le_ne_top int_f (lintegral_mono fun x => _)
  simpa only [ENNReal.coe_le_coe] using fs_le_f x
case intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), ↑fs x ≤ f x
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
int_fs_lt_top : (∫⁻ (x : α), ↑(↑fs x) ∂μ) ≠ ⊤
g : α → ℝ≥0
g_le_fs : ∀ (x : α), g x ≤ ↑fs x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(↑fs x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ε / 2
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ε
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), ↑fs x ≤ f x
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
int_fs_lt_top : (∫⁻ (x : α), ↑(↑fs x) ∂μ) ≠ ⊤
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ε
obtain ⟨g, g_le_fs, gcont, gint⟩ :
  ∃ g : α → ℝ≥0,
    (∀ x, g x ≤ fs x) ∧ UpperSemicontinuous g ∧ (∫⁻ x, fs x ∂μ) ≤ (∫⁻ x, g x ∂μ) + ε / 2 :=
  fs.exists_upperSemicontinuous_le_lintegral_le int_fs_lt_top (ENNReal.half_pos ε0).ne'
case intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), ↑fs x ≤ f x
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
int_fs_lt_top : (∫⁻ (x : α), ↑(↑fs x) ∂μ) ≠ ⊤
g : α → ℝ≥0
g_le_fs : ∀ (x : α), g x ≤ ↑fs x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(↑fs x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ε / 2
⊢ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ε
case intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), ↑fs x ≤ f x
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
int_fs_lt_top : (∫⁻ (x : α), ↑(↑fs x) ∂μ) ≠ ⊤
g : α → ℝ≥0
g_le_fs : ∀ (x : α), g x ≤ ↑fs x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(↑fs x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ε / 2
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ε
refine' ⟨g, fun x => (g_le_fs x).trans (fs_le_f x), gcont, _⟩
no goals
case intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), ↑fs x ≤ f x
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
int_fs_lt_top : (∫⁻ (x : α), ↑(↑fs x) ∂μ) ≠ ⊤
g : α → ℝ≥0
g_le_fs : ∀ (x : α), g x ≤ ↑fs x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(↑fs x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ε / 2
⊢ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ε
calc
  (∫⁻ x, f x ∂μ) ≤ (∫⁻ x, fs x ∂μ) + ε / 2 := int_fs
  _ ≤ (∫⁻ x, g x ∂μ) + ε / 2 + ε / 2 := (add_le_add gint le_rfl)
  _ = (∫⁻ x, g x ∂μ) + ε := by rw [add_assoc, ENNReal.add_halves]
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
aux : (∫⁻ (x : α), ↑(f x) ∂μ) < (∫⁻ (x : α), ↑(f x) ∂μ) + ε / 2
⊢ ∃ fs, (∀ (x : α), ↑fs x ≤ f x) ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∃ fs, (∀ (x : α), ↑fs x ≤ f x) ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
have aux := ENNReal.lt_add_right int_f (ENNReal.half_pos ε0).ne'
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
aux :
  (∫⁻ (x : α), ↑(f x) ∂μ) <
    (⨆ (φ : α →ₛ ℝ≥0) (_ : ∀ (x : α), ↑(↑φ x) ≤ ↑(f x)), SimpleFunc.lintegral (SimpleFunc.map ENNReal.some φ) μ) + ε / 2
⊢ ∃ fs, (∀ (x : α), ↑fs x ≤ f x) ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
aux : (∫⁻ (x : α), ↑(f x) ∂μ) < (∫⁻ (x : α), ↑(f x) ∂μ) + ε / 2
⊢ ∃ fs, (∀ (x : α), ↑fs x ≤ f x) ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
conv_rhs at aux => rw [lintegral_eq_nnreal (fun x => (f x : ℝ≥0∞)) μ]
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
aux :
  (∫⁻ (x : α), ↑(f x) ∂μ) <
    ⨆ (i : α →ₛ ℝ≥0) (_ : i ∈ fun φ => ∀ (x : α), ↑(↑φ x) ≤ ↑(f x)),
      SimpleFunc.lintegral (SimpleFunc.map ENNReal.some i) μ + ε / 2
⊢ ∃ fs, (∀ (x : α), ↑fs x ≤ f x) ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
aux :
  (∫⁻ (x : α), ↑(f x) ∂μ) <
    (⨆ (φ : α →ₛ ℝ≥0) (_ : ∀ (x : α), ↑(↑φ x) ≤ ↑(f x)), SimpleFunc.lintegral (SimpleFunc.map ENNReal.some φ) μ) + ε / 2
⊢ ∃ fs, (∀ (x : α), ↑fs x ≤ f x) ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
erw [ENNReal.biSup_add] at aux  <;> [skip; exact ⟨0, fun x => by simp⟩]
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
aux : ∃ i i_1, (∫⁻ (x : α), ↑(f x) ∂μ) < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some i) μ + ε / 2
⊢ ∃ fs, (∀ (x : α), ↑fs x ≤ f x) ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
aux :
  (∫⁻ (x : α), ↑(f x) ∂μ) <
    ⨆ (i : α →ₛ ℝ≥0) (_ : i ∈ fun φ => ∀ (x : α), ↑(↑φ x) ≤ ↑(f x)),
      SimpleFunc.lintegral (SimpleFunc.map ENNReal.some i) μ + ε / 2
⊢ ∃ fs, (∀ (x : α), ↑fs x ≤ f x) ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
simp only [lt_iSup_iff] at aux
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : fs ∈ fun φ => ∀ (x : α), ↑(↑φ x) ≤ ↑(f x)
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some fs) μ + ε / 2
⊢ ∃ fs, (∀ (x : α), ↑fs x ≤ f x) ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
aux : ∃ i i_1, (∫⁻ (x : α), ↑(f x) ∂μ) < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some i) μ + ε / 2
⊢ ∃ fs, (∀ (x : α), ↑fs x ≤ f x) ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
rcases aux with ⟨fs, fs_le_f, int_fs⟩
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : fs ∈ fun φ => ∀ (x : α), ↑(↑φ x) ≤ ↑(f x)
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some fs) μ + ε / 2
⊢ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : fs ∈ fun φ => ∀ (x : α), ↑(↑φ x) ≤ ↑(f x)
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some fs) μ + ε / 2
⊢ ∃ fs, (∀ (x : α), ↑fs x ≤ f x) ∧ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
refine' ⟨fs, fun x => by simpa only [ENNReal.coe_le_coe] using fs_le_f x, _⟩
case h.e'_4.h.e'_5
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : fs ∈ fun φ => ∀ (x : α), ↑(↑φ x) ≤ ↑(f x)
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some fs) μ + ε / 2
⊢ (∫⁻ (x : α), ↑(↑fs x) ∂μ) = SimpleFunc.lintegral (SimpleFunc.map ENNReal.some fs) μ
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : fs ∈ fun φ => ∀ (x : α), ↑(↑φ x) ≤ ↑(f x)
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some fs) μ + ε / 2
⊢ (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
convert int_fs.le
case h.e'_4.h.e'_5
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : fs ∈ fun φ => ∀ (x : α), ↑(↑φ x) ≤ ↑(f x)
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some fs) μ + ε / 2
⊢ (∫⁻ (x : α), ↑(↑fs x) ∂μ) = ∫⁻ (a : α), ↑(SimpleFunc.map ENNReal.some fs) a ∂μ
case h.e'_4.h.e'_5
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : fs ∈ fun φ => ∀ (x : α), ↑(↑φ x) ≤ ↑(f x)
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some fs) μ + ε / 2
⊢ (∫⁻ (x : α), ↑(↑fs x) ∂μ) = SimpleFunc.lintegral (SimpleFunc.map ENNReal.some fs) μ
rw [← SimpleFunc.lintegral_eq_lintegral]
no goals
case h.e'_4.h.e'_5
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : fs ∈ fun φ => ∀ (x : α), ↑(↑φ x) ≤ ↑(f x)
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some fs) μ + ε / 2
⊢ (∫⁻ (x : α), ↑(↑fs x) ∂μ) = ∫⁻ (a : α), ↑(SimpleFunc.map ENNReal.some fs) a ∂μ
rfl
no goals
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
aux :
  (∫⁻ (x : α), ↑(f x) ∂μ) <
    (⨆ (φ : α →ₛ ℝ≥0) (_ : ∀ (x : α), ↑(↑φ x) ≤ ↑(f x)), SimpleFunc.lintegral (SimpleFunc.map ENNReal.some φ) μ) + ε / 2
x : α
⊢ ↑(↑0 x) ≤ ↑(f x)
simp
no goals
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : fs ∈ fun φ => ∀ (x : α), ↑(↑φ x) ≤ ↑(f x)
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) < SimpleFunc.lintegral (SimpleFunc.map ENNReal.some fs) μ + ε / 2
x : α
⊢ ↑fs x ≤ f x
simpa only [ENNReal.coe_le_coe] using fs_le_f x
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), ↑fs x ≤ f x
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
x : α
⊢ ↑(↑fs x) ≤ ↑(f x)
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), ↑fs x ≤ f x
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
⊢ (∫⁻ (x : α), ↑(↑fs x) ∂μ) ≠ ⊤
refine' ne_top_of_le_ne_top int_f (lintegral_mono fun x => _)
no goals
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), ↑fs x ≤ f x
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
x : α
⊢ ↑(↑fs x) ≤ ↑(f x)
simpa only [ENNReal.coe_le_coe] using fs_le_f x
no goals
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
int_f : (∫⁻ (x : α), ↑(f x) ∂μ) ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), ↑fs x ≤ f x
int_fs : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(↑fs x) ∂μ) + ε / 2
int_fs_lt_top : (∫⁻ (x : α), ↑(↑fs x) ∂μ) ≠ ⊤
g : α → ℝ≥0
g_le_fs : ∀ (x : α), g x ≤ ↑fs x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(↑fs x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ε / 2
⊢ (∫⁻ (x : α), ↑(g x) ∂μ) + ε / 2 + ε / 2 = (∫⁻ (x : α), ↑(g x) ∂μ) + ε
rw [add_assoc, ENNReal.add_halves]