α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ
εpos : 0 < ε
fmeas : AEMeasurable f
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧ (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ε
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ
εpos : 0 < ε
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧ (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ε
have fmeas : AEMeasurable f μ := by
  convert fint.aestronglyMeasurable.real_toNNReal.aemeasurable
  simp only [Real.toNNReal_coe]
case intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧
            (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ
εpos : 0 < ε
fmeas : AEMeasurable f
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧ (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ε
lift ε to ℝ≥0 using εpos.le
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
⊢ ∃ δ, 0 < δ ∧ δ < ε

case intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧
            (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
case intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧
            (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
obtain ⟨δ, δpos, hδε⟩ : ∃ δ : ℝ≥0, 0 < δ ∧ δ < ε
case intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧
            (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
⊢ ∃ δ, 0 < δ ∧ δ < ε

case intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧
            (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
exact exists_between εpos
case intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧
            (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
case intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧
            (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
have int_f_ne_top : (∫⁻ a : α, f a ∂μ) ≠ ∞ :=
  (hasFiniteIntegral_iff_ofNNReal.1 fint.hasFiniteIntegral).ne
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧
            (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
case intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧
            (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
rcases exists_lt_lowerSemicontinuous_lintegral_ge_of_aemeasurable μ f fmeas
    (ENNReal.coe_ne_zero.2 δpos.ne') with
  ⟨g, f_lt_g, gcont, gint⟩
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧
            (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧
            (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
have gint_ne : (∫⁻ x : α, g x ∂μ) ≠ ∞ := ne_top_of_le_ne_top (by simpa) gint
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧
            (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧
            (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
have g_lt_top : ∀ᵐ x : α ∂μ, g x < ∞ := ae_lt_top gcont.measurable gint_ne
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧
            (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧
            (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
have Ig : (∫⁻ a : α, ENNReal.ofReal (g a).toReal ∂μ) = ∫⁻ a : α, g a ∂μ := by
  apply lintegral_congr_ae
  filter_upwards [g_lt_top] with _ hx
  simp only [hx.ne, ENNReal.ofReal_toReal, Ne.def, not_false_iff]
case intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ Integrable fun x => ENNReal.toReal (g x)

case intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
          (Integrable fun x => ENNReal.toReal (g x)) ∧
            (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
refine' ⟨g, f_lt_g, gcont, g_lt_top, _, _⟩
case h.e'_5.h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ
εpos : 0 < ε
x✝ : α
⊢ f x✝ = Real.toNNReal ↑(f x✝)
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ
εpos : 0 < ε
⊢ AEMeasurable f
convert fint.aestronglyMeasurable.real_toNNReal.aemeasurable
no goals
case h.e'_5.h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ
εpos : 0 < ε
x✝ : α
⊢ f x✝ = Real.toNNReal ↑(f x✝)
simp only [Real.toNNReal_coe]
no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
⊢ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ ≠ ⊤
simpa
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
⊢ (fun a => ENNReal.ofReal (ENNReal.toReal (g a))) =ᶠ[ae μ] fun a => g a
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
⊢ (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
apply lintegral_congr_ae
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
a✝ : α
hx : g a✝ < ⊤
⊢ ENNReal.ofReal (ENNReal.toReal (g a✝)) = g a✝
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
⊢ (fun a => ENNReal.ofReal (ENNReal.toReal (g a))) =ᶠ[ae μ] fun a => g a
filter_upwards [g_lt_top] with _ hx
no goals
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
a✝ : α
hx : g a✝ < ⊤
⊢ ENNReal.ofReal (ENNReal.toReal (g a✝)) = g a✝
simp only [hx.ne, ENNReal.ofReal_toReal, Ne.def, not_false_iff]
case intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ HasFiniteIntegral fun x => ENNReal.toReal (g x)
case intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ Integrable fun x => ENNReal.toReal (g x)
refine' ⟨gcont.measurable.ennreal_toReal.aemeasurable.aestronglyMeasurable, _⟩
case intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) < ⊤
case intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ HasFiniteIntegral fun x => ENNReal.toReal (g x)
simp only [hasFiniteIntegral_iff_norm, Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg]
no goals
case intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) < ⊤
convert gint_ne.lt_top using 1
case intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) <
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ↑(f a) ∂μ) + ↑ε

case intro.intro.intro.intro.intro.intro.refine'_2.hf
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ 0 ≤ᶠ[ae μ] fun x => ↑(f x)

case intro.intro.intro.intro.intro.intro.refine'_2.hfm
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ AEStronglyMeasurable (fun x => ↑(f x)) μ

case intro.intro.intro.intro.intro.intro.refine'_2.hf
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ 0 ≤ᶠ[ae μ] fun x => ENNReal.toReal (g x)

case intro.intro.intro.intro.intro.intro.refine'_2.hfm
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ AEStronglyMeasurable (fun x => ENNReal.toReal (g x)) μ
case intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ (∫ (x : α), ENNReal.toReal (g x) ∂μ) < (∫ (x : α), ↑(f x) ∂μ) + ↑ε
rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
no goals
case intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) <
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ↑(f a) ∂μ) + ↑ε
calc
  ENNReal.toReal (∫⁻ a : α, ENNReal.ofReal (g a).toReal ∂μ) =
      ENNReal.toReal (∫⁻ a : α, g a ∂μ) :=
    by congr 1
  _ ≤ ENNReal.toReal ((∫⁻ a : α, f a ∂μ) + δ) := by
    apply ENNReal.toReal_mono _ gint
    simpa using int_f_ne_top
  _ = ENNReal.toReal (∫⁻ a : α, f a ∂μ) + δ := by
    rw [ENNReal.toReal_add int_f_ne_top ENNReal.coe_ne_top, ENNReal.coe_toReal]
  _ < ENNReal.toReal (∫⁻ a : α, f a ∂μ) + ε := (add_lt_add_left hδε _)
  _ = (∫⁻ a : α, ENNReal.ofReal ↑(f a) ∂μ).toReal + ε := by simp
no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ENNReal.toReal (∫⁻ (a : α), g a ∂μ)
congr 1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ ≠ ⊤
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ ENNReal.toReal (∫⁻ (a : α), g a ∂μ) ≤ ENNReal.toReal ((∫⁻ (a : α), ↑(f a) ∂μ) + ↑δ)
apply ENNReal.toReal_mono _ gint
no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ ≠ ⊤
simpa using int_f_ne_top
no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ ENNReal.toReal ((∫⁻ (a : α), ↑(f a) ∂μ) + ↑δ) = ENNReal.toReal (∫⁻ (a : α), ↑(f a) ∂μ) + ↑δ
rw [ENNReal.toReal_add int_f_ne_top ENNReal.coe_ne_top, ENNReal.coe_toReal]
no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ ENNReal.toReal (∫⁻ (a : α), ↑(f a) ∂μ) + ↑ε = ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ↑(f a) ∂μ) + ↑ε
simp
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ ∀ (x : α), OfNat.ofNat 0 x ≤ (fun x => ↑(f x)) x
case intro.intro.intro.intro.intro.intro.refine'_2.hf
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ 0 ≤ᶠ[ae μ] fun x => ↑(f x)
apply Filter.eventually_of_forall fun x => _
no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ ∀ (x : α), OfNat.ofNat 0 x ≤ (fun x => ↑(f x)) x
simp
no goals
case intro.intro.intro.intro.intro.intro.refine'_2.hfm
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ AEStronglyMeasurable (fun x => ↑(f x)) μ
exact fmeas.coe_nnreal_real.aestronglyMeasurable
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ ∀ (x : α), OfNat.ofNat 0 x ≤ (fun x => ENNReal.toReal (g x)) x
case intro.intro.intro.intro.intro.intro.refine'_2.hf
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ 0 ≤ᶠ[ae μ] fun x => ENNReal.toReal (g x)
apply Filter.eventually_of_forall fun x => _
no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ ∀ (x : α), OfNat.ofNat 0 x ≤ (fun x => ENNReal.toReal (g x)) x
simp
no goals
case intro.intro.intro.intro.intro.intro.refine'_2.hfm
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
fmeas : AEMeasurable f
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), ↑(f x) ∂μ) + ↑δ
gint_ne : (∫⁻ (x : α), g x ∂μ) ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : (∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal (g a)) ∂μ) = ∫⁻ (a : α), g a ∂μ
⊢ AEStronglyMeasurable (fun x => ENNReal.toReal (g x)) μ
apply gcont.measurable.ennreal_toReal.aemeasurable.aestronglyMeasurable