α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
let δ : ℝ≥0 := ⟨ε / 2, (half_pos εpos).le⟩
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
have δpos : 0 < δ := half_pos εpos
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
let fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
have int_fp : Integrable (fun x => (fp x : ℝ)) μ := hf.real_toNNReal
case intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
rcases exists_lt_lowerSemicontinuous_integral_gt_nnreal fp int_fp δpos with
  ⟨gp, fp_lt_gp, gpcont, gp_lt_top, gp_integrable, gpint⟩
case intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
case intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
let fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
case intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
case intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
have int_fm : Integrable (fun x => (fm x : ℝ)) μ := hf.neg.real_toNNReal
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
case intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
rcases exists_upperSemicontinuous_le_integral_le fm int_fm δpos with
  ⟨gm, gm_le_fm, gmcont, gm_integrable, gmint⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
let g : α → EReal := fun x => (gp x : EReal) - gm x
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
have ae_g : ∀ᵐ x ∂μ, (g x).toReal = (gp x : EReal).toReal - (gm x : EReal).toReal := by
  filter_upwards [gp_lt_top] with _ hx
  rw [EReal.toReal_sub] <;> simp [hx.ne]
case lt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ (x : α), ↑(f x) < g x

case lsc
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ LowerSemicontinuous g

case int
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ Integrable fun x => EReal.toReal (g x)

case aelt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ᵐ (x : α) ∂μ, g x < ⊤

case intlt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
refine' ⟨g, ?lt, ?lsc, ?int, ?aelt, ?intlt⟩
case lt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ (x : α), ↑(f x) < g x

case lsc
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ LowerSemicontinuous g

case aelt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ᵐ (x : α) ∂μ, g x < ⊤

case intlt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
case lt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ (x : α), ↑(f x) < g x

case lsc
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ LowerSemicontinuous g

case int
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ Integrable fun x => EReal.toReal (g x)

case aelt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ᵐ (x : α) ∂μ, g x < ⊤

case intlt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
case int =>
  show Integrable (fun x => EReal.toReal (g x)) μ
  rw [integrable_congr ae_g]
  convert gp_integrable.sub gm_integrable
  simp
case lt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ (x : α), ↑(f x) < g x

case lsc
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ LowerSemicontinuous g

case aelt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ᵐ (x : α) ∂μ, g x < ⊤
case lt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ (x : α), ↑(f x) < g x

case lsc
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ LowerSemicontinuous g

case aelt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ᵐ (x : α) ∂μ, g x < ⊤

case intlt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
case intlt =>
  show (∫ x : α, (g x).toReal ∂μ) < (∫ x : α, f x ∂μ) + ε;
  exact
    calc
      (∫ x : α, (g x).toReal ∂μ) = ∫ x : α, EReal.toReal (gp x) - EReal.toReal (gm x) ∂μ :=
        integral_congr_ae ae_g
      _ = (∫ x : α, EReal.toReal (gp x) ∂μ) - ∫ x : α, ↑(gm x) ∂μ := by
        simp only [EReal.toReal_coe_ennreal, ENNReal.coe_toReal]
        exact integral_sub gp_integrable gm_integrable
      _ < (∫ x : α, ↑(fp x) ∂μ) + ↑δ - ∫ x : α, ↑(gm x) ∂μ := by
        apply sub_lt_sub_right
        convert gpint
        simp only [EReal.toReal_coe_ennreal]
      _ ≤ (∫ x : α, ↑(fp x) ∂μ) + ↑δ - ((∫ x : α, ↑(fm x) ∂μ) - δ) := (sub_le_sub_left gmint _)
      _ = (∫ x : α, f x ∂μ) + 2 * δ := by
        simp_rw [integral_eq_integral_pos_part_sub_integral_neg_part hf]; ring
      _ = (∫ x : α, f x ∂μ) + ε := by congr 1; field_simp [mul_comm]
case lt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ (x : α), ↑(f x) < g x

case lsc
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ LowerSemicontinuous g
case lt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ (x : α), ↑(f x) < g x

case lsc
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ LowerSemicontinuous g

case aelt
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ᵐ (x : α) ∂μ, g x < ⊤
case aelt =>
  show ∀ᵐ x : α ∂μ, g x < ⊤
  filter_upwards [gp_lt_top] with ?_ hx
  simp only [sub_eq_add_neg, Ne.def, (EReal.add_lt_top _ _).ne, lt_top_iff_ne_top,
    lt_top_iff_ne_top.1 hx, EReal.coe_ennreal_eq_top_iff, not_false_iff, EReal.neg_eq_top_iff,
    EReal.coe_ennreal_ne_bot]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
a✝ : α
hx : gp a✝ < ⊤
⊢ EReal.toReal (↑(gp a✝) - ↑↑(gm a✝)) = EReal.toReal ↑(gp a✝) - EReal.toReal ↑↑(gm a✝)
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
⊢ ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
filter_upwards [gp_lt_top] with _ hx
no goals
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
a✝ : α
hx : gp a✝ < ⊤
⊢ EReal.toReal (↑(gp a✝) - ↑↑(gm a✝)) = EReal.toReal ↑(gp a✝) - EReal.toReal ↑↑(gm a✝)
rw [EReal.toReal_sub] <;> simp [hx.ne]
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ Integrable fun x => EReal.toReal (g x)
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ Integrable fun x => EReal.toReal (g x)
show Integrable (fun x => EReal.toReal (g x)) μ
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ Integrable fun x => EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ Integrable fun x => EReal.toReal (g x)
rw [integrable_congr ae_g]
case h.e'_5.h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x✝ : α
⊢ EReal.toReal ↑(gp x✝) - EReal.toReal ↑↑(gm x✝) = ((fun x => ENNReal.toReal (gp x)) - fun x => ↑(gm x)) x✝
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ Integrable fun x => EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
convert gp_integrable.sub gm_integrable
no goals
case h.e'_5.h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x✝ : α
⊢ EReal.toReal ↑(gp x✝) - EReal.toReal ↑↑(gm x✝) = ((fun x => ENNReal.toReal (gp x)) - fun x => ↑(gm x)) x✝
simp
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
show (∫ x : α, (g x).toReal ∂μ) < (∫ x : α, f x ∂μ) + ε
no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), f x ∂μ) + ε
exact
  calc
    (∫ x : α, (g x).toReal ∂μ) = ∫ x : α, EReal.toReal (gp x) - EReal.toReal (gm x) ∂μ :=
      integral_congr_ae ae_g
    _ = (∫ x : α, EReal.toReal (gp x) ∂μ) - ∫ x : α, ↑(gm x) ∂μ := by
      simp only [EReal.toReal_coe_ennreal, ENNReal.coe_toReal]
      exact integral_sub gp_integrable gm_integrable
    _ < (∫ x : α, ↑(fp x) ∂μ) + ↑δ - ∫ x : α, ↑(gm x) ∂μ := by
      apply sub_lt_sub_right
      convert gpint
      simp only [EReal.toReal_coe_ennreal]
    _ ≤ (∫ x : α, ↑(fp x) ∂μ) + ↑δ - ((∫ x : α, ↑(fm x) ∂μ) - δ) := (sub_le_sub_left gmint _)
    _ = (∫ x : α, f x ∂μ) + 2 * δ := by
      simp_rw [integral_eq_integral_pos_part_sub_integral_neg_part hf]; ring
    _ = (∫ x : α, f x ∂μ) + ε := by congr 1; field_simp [mul_comm]
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ (∫ (x : α), ENNReal.toReal (gp x) - ↑(gm x) ∂μ) = (∫ (x : α), ENNReal.toReal (gp x) ∂μ) - ∫ (x : α), ↑(gm x) ∂μ
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ (∫ (x : α), EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x) ∂μ) =
    (∫ (x : α), EReal.toReal ↑(gp x) ∂μ) - ∫ (x : α), ↑(gm x) ∂μ
simp only [EReal.toReal_coe_ennreal, ENNReal.coe_toReal]
no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ (∫ (x : α), ENNReal.toReal (gp x) - ↑(gm x) ∂μ) = (∫ (x : α), ENNReal.toReal (gp x) ∂μ) - ∫ (x : α), ↑(gm x) ∂μ
exact integral_sub gp_integrable gm_integrable
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ (∫ (x : α), EReal.toReal ↑(gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + ↑δ
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ((∫ (x : α), EReal.toReal ↑(gp x) ∂μ) - ∫ (x : α), ↑(gm x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + ↑δ - ∫ (x : α), ↑(gm x) ∂μ
apply sub_lt_sub_right
case h.e'_3.h.e'_8.h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x✝ : α
⊢ EReal.toReal ↑(gp x✝) = ENNReal.toReal (gp x✝)
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ (∫ (x : α), EReal.toReal ↑(gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + ↑δ
convert gpint
no goals
case h.e'_3.h.e'_8.h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x✝ : α
⊢ EReal.toReal ↑(gp x✝) = ENNReal.toReal (gp x✝)
simp only [EReal.toReal_coe_ennreal]
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ (∫ (x : α), ↑(Real.toNNReal (f x)) ∂μ) + ↑{ val := ε / 2, property := (_ : 0 ≤ ε / 2) } -
      ((∫ (x : α), ↑(Real.toNNReal (-f x)) ∂μ) - ↑{ val := ε / 2, property := (_ : 0 ≤ ε / 2) }) =
    ((∫ (x : α), ↑(Real.toNNReal (f x)) ∂μ) - ∫ (x : α), ↑(Real.toNNReal (-f x)) ∂μ) +
      2 * ↑{ val := ε / 2, property := (_ : 0 ≤ ε / 2) }
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ (∫ (x : α), ↑(fp x) ∂μ) + ↑δ - ((∫ (x : α), ↑(fm x) ∂μ) - ↑δ) = (∫ (x : α), f x ∂μ) + 2 * ↑δ
simp_rw [integral_eq_integral_pos_part_sub_integral_neg_part hf]
no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ (∫ (x : α), ↑(Real.toNNReal (f x)) ∂μ) + ↑{ val := ε / 2, property := (_ : 0 ≤ ε / 2) } -
      ((∫ (x : α), ↑(Real.toNNReal (-f x)) ∂μ) - ↑{ val := ε / 2, property := (_ : 0 ≤ ε / 2) }) =
    ((∫ (x : α), ↑(Real.toNNReal (f x)) ∂μ) - ∫ (x : α), ↑(Real.toNNReal (-f x)) ∂μ) +
      2 * ↑{ val := ε / 2, property := (_ : 0 ≤ ε / 2) }
ring
case e_a
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ 2 * ↑δ = ε
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ (∫ (x : α), f x ∂μ) + 2 * ↑δ = (∫ (x : α), f x ∂μ) + ε
congr 1
no goals
case e_a
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ 2 * ↑δ = ε
field_simp [mul_comm]
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ᵐ (x : α) ∂μ, g x < ⊤
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ᵐ (x : α) ∂μ, g x < ⊤
show ∀ᵐ x : α ∂μ, g x < ⊤
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x✝ : α
hx : gp x✝ < ⊤
⊢ ↑(gp x✝) - ↑↑(gm x✝) < ⊤
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ᵐ (x : α) ∂μ, g x < ⊤
filter_upwards [gp_lt_top] with ?_ hx
no goals
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x✝ : α
hx : gp x✝ < ⊤
⊢ ↑(gp x✝) - ↑↑(gm x✝) < ⊤
simp only [sub_eq_add_neg, Ne.def, (EReal.add_lt_top _ _).ne, lt_top_iff_ne_top,
  lt_top_iff_ne_top.1 hx, EReal.coe_ennreal_eq_top_iff, not_false_iff, EReal.neg_eq_top_iff,
  EReal.coe_ennreal_ne_bot]
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ (x : α), ↑(f x) < g x
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ (x : α), ↑(f x) < g x
show ∀ x, (f x : EReal) < g x
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ ↑(f x) < g x
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ (x : α), ↑(f x) < g x
intro x
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ ↑↑(Real.toNNReal (f x)) - ↑↑(Real.toNNReal (-f x)) < g x
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ ↑(f x) < g x
rw [EReal.coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal (f x)]
case refine'_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ ↑↑(Real.toNNReal (f x)) < ↑(gp x)

case refine'_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ ↑↑(gm x) ≤ ↑↑(Real.toNNReal (-f x))

case refine'_3
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ ↑↑(gm x) ≠ ⊥

case refine'_4
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ ↑↑(Real.toNNReal (-f x)) ≠ ⊤
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ ↑↑(Real.toNNReal (f x)) - ↑↑(Real.toNNReal (-f x)) < g x
refine' EReal.sub_lt_sub_of_lt_of_le _ _ _ _
case refine'_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ ↑(Real.toNNReal (f x)) < gp x
case refine'_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ ↑↑(Real.toNNReal (f x)) < ↑(gp x)
simp only [EReal.coe_ennreal_lt_coe_ennreal_iff]
no goals
case refine'_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ ↑(Real.toNNReal (f x)) < gp x
exact fp_lt_gp x
case refine'_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ gm x ≤ Real.toNNReal (-f x)
case refine'_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ ↑↑(gm x) ≤ ↑↑(Real.toNNReal (-f x))
simp only [ENNReal.coe_le_coe, EReal.coe_ennreal_le_coe_ennreal_iff]
no goals
case refine'_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ gm x ≤ Real.toNNReal (-f x)
exact gm_le_fm x
no goals
case refine'_3
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ ↑↑(gm x) ≠ ⊥
simp only [EReal.coe_ennreal_ne_bot, Ne.def, not_false_iff]
no goals
case refine'_4
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ ↑↑(Real.toNNReal (-f x)) ≠ ⊤
simp only [EReal.coe_nnreal_ne_top, Ne.def, not_false_iff]
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ LowerSemicontinuous g
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ LowerSemicontinuous g
show LowerSemicontinuous g
case hf
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ LowerSemicontinuous fun z => ↑(gp z)

case hg
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ LowerSemicontinuous fun z => -↑↑(gm z)

case hcont
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ (x : α), ContinuousAt (fun p => p.fst + p.snd) (↑(gp x), -↑↑(gm x))
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ LowerSemicontinuous g
apply LowerSemicontinuous.add'
no goals
case hf
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ LowerSemicontinuous fun z => ↑(gp z)
exact continuous_coe_ennreal_ereal.comp_lowerSemicontinuous gpcont fun x y hxy =>
    EReal.coe_ennreal_le_coe_ennreal_iff.2 hxy
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ UpperSemicontinuous fun z => ↑↑(gm z)
case hg
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ LowerSemicontinuous fun z => -↑↑(gm z)
apply continuous_neg.comp_upperSemicontinuous_antitone _ fun x y hxy =>
    EReal.neg_le_neg_iff.2 hxy
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ UpperSemicontinuous fun z => ↑↑(gm z)
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ UpperSemicontinuous fun z => ↑↑(gm z)
dsimp
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ UpperSemicontinuous fun z => ↑(gm z)
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ UpperSemicontinuous fun z => ↑↑(gm z)
apply continuous_coe_ennreal_ereal.comp_upperSemicontinuous _ fun x y hxy =>
    EReal.coe_ennreal_le_coe_ennreal_iff.2 hxy
no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ UpperSemicontinuous fun z => ↑(gm z)
exact ENNReal.continuous_coe.comp_upperSemicontinuous gmcont fun x y hxy =>
    ENNReal.coe_le_coe.2 hxy
case hcont
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑(gp x), -↑↑(gm x))
case hcont
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
⊢ ∀ (x : α), ContinuousAt (fun p => p.fst + p.snd) (↑(gp x), -↑↑(gm x))
intro x
no goals
case hcont
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑(gp x), -↑↑(gm x))
exact EReal.continuousAt_add (by simp) (by simp)
no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ (↑(gp x), -↑↑(gm x)).fst ≠ ⊤ ∨ (↑(gp x), -↑↑(gm x)).snd ≠ ⊥
simp
no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := { val := ε / 2, property := (_ : 0 ≤ ε / 2) }
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
int_fp : Integrable fun x => ↑(fp x)
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable fun x => ENNReal.toReal (gp x)
gpint : (∫ (x : α), ENNReal.toReal (gp x) ∂μ) < (∫ (x : α), ↑(fp x) ∂μ) + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
int_fm : Integrable fun x => ↑(fm x)
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable fun x => ↑(gm x)
gmint : (∫ (x : α), ↑(fm x) ∂μ) - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, EReal.toReal (g x) = EReal.toReal ↑(gp x) - EReal.toReal ↑↑(gm x)
x : α
⊢ (↑(gp x), -↑↑(gm x)).fst ≠ ⊥ ∨ (↑(gp x), -↑↑(gm x)).snd ≠ ⊤
simp