case intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
⊢ ∃ g,
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧ (Integrable fun x => ↑(g x)) ∧ (∫ (x : α), ↑(f x) ∂μ) - ↑ε ≤ ∫ (x : α), ↑(g x) ∂μ
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ
εpos : 0 < ε
⊢ ∃ g,
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧ (Integrable fun x => ↑(g x)) ∧ (∫ (x : α), ↑(f x) ∂μ) - ε ≤ ∫ (x : α), ↑(g x) ∂μ
lift ε to ℝ≥0 using εpos.le
case intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
⊢ ∃ g,
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧ (Integrable fun x => ↑(g x)) ∧ (∫ (x : α), ↑(f x) ∂μ) - ↑ε ≤ ∫ (x : α), ↑(g x) ∂μ
case intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
⊢ ∃ g,
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧ (Integrable fun x => ↑(g x)) ∧ (∫ (x : α), ↑(f x) ∂μ) - ↑ε ≤ ∫ (x : α), ↑(g x) ∂μ
rw [NNReal.coe_pos, ← ENNReal.coe_pos] at εpos
case intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
⊢ ∃ g,
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧ (Integrable fun x => ↑(g x)) ∧ (∫ (x : α), ↑(f x) ∂μ) - ↑ε ≤ ∫ (x : α), ↑(g x) ∂μ
case intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
⊢ ∃ g,
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧ (Integrable fun x => ↑(g x)) ∧ (∫ (x : α), ↑(f x) ∂μ) - ↑ε ≤ ∫ (x : α), ↑(g x) ∂μ
have If : (∫⁻ x, f x ∂μ) < ∞ := hasFiniteIntegral_iff_ofNNReal.1 fint.hasFiniteIntegral
case intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
⊢ ∃ g,
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧ (Integrable fun x => ↑(g x)) ∧ (∫ (x : α), ↑(f x) ∂μ) - ↑ε ≤ ∫ (x : α), ↑(g x) ∂μ
case intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
⊢ ∃ g,
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧ (Integrable fun x => ↑(g x)) ∧ (∫ (x : α), ↑(f x) ∂μ) - ↑ε ≤ ∫ (x : α), ↑(g x) ∂μ
rcases exists_upperSemicontinuous_le_lintegral_le f If.ne εpos.ne' with ⟨g, gf, gcont, gint⟩
case intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ ∃ g,
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧ (Integrable fun x => ↑(g x)) ∧ (∫ (x : α), ↑(f x) ∂μ) - ↑ε ≤ ∫ (x : α), ↑(g x) ∂μ
case intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
⊢ ∃ g,
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧ (Integrable fun x => ↑(g x)) ∧ (∫ (x : α), ↑(f x) ∂μ) - ↑ε ≤ ∫ (x : α), ↑(g x) ∂μ
have Ig : (∫⁻ x, g x ∂μ) < ∞ := by
  refine' lt_of_le_of_lt (lintegral_mono fun x => _) If
  simpa using gf x
case intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ Integrable fun x => ↑(g x)

case intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ (∫ (x : α), ↑(f x) ∂μ) - ↑ε ≤ ∫ (x : α), ↑(g x) ∂μ
case intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ ∃ g,
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧ (Integrable fun x => ↑(g x)) ∧ (∫ (x : α), ↑(f x) ∂μ) - ↑ε ≤ ∫ (x : α), ↑(g x) ∂μ
refine' ⟨g, gf, gcont, _, _⟩
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
x : α
⊢ ↑(g x) ≤ ↑(f x)
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
⊢ (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
refine' lt_of_le_of_lt (lintegral_mono fun x => _) If
no goals
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
x : α
⊢ ↑(g x) ≤ ↑(f x)
simpa using gf x
case intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ ∀ᵐ (a : α) ∂μ, ‖↑(g a)‖ ≤ ‖↑(f a)‖
case intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ Integrable fun x => ↑(g x)
refine'
  Integrable.mono fint gcont.measurable.coe_nnreal_real.aemeasurable.aestronglyMeasurable _
no goals
case intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ ∀ᵐ (a : α) ∂μ, ‖↑(g a)‖ ≤ ‖↑(f a)‖
exact Filter.eventually_of_forall fun x => by simp [gf x]
no goals
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
x : α
⊢ ‖↑(g x)‖ ≤ ‖↑(f x)‖
simp [gf x]
case intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ↑(f a) ∂μ) - ↑ε ≤ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ↑(g a) ∂μ)

case intro.intro.intro.intro.refine'_2.hf
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ 0 ≤ᶠ[ae μ] fun x => ↑(g x)

case intro.intro.intro.intro.refine'_2.hfm
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ AEStronglyMeasurable (fun x => ↑(g x)) μ

case intro.intro.intro.intro.refine'_2.hf
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ 0 ≤ᶠ[ae μ] fun x => ↑(f x)

case intro.intro.intro.intro.refine'_2.hfm
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ AEStronglyMeasurable (fun x => ↑(f x)) μ
case intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ (∫ (x : α), ↑(f x) ∂μ) - ↑ε ≤ ∫ (x : α), ↑(g x) ∂μ
rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
case intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ↑(f a) ∂μ) ≤ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ↑(g a) ∂μ) + ↑ε
case intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ↑(f a) ∂μ) - ↑ε ≤ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ↑(g a) ∂μ)
rw [sub_le_iff_le_add]
case h.e'_3.h.e'_1.h.e'_4.h
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
x✝ : α
⊢ ENNReal.ofReal ↑(f x✝) = ↑(f x✝)

case h.e'_4
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ↑(g a) ∂μ) + ↑ε = ENNReal.toReal ((∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε)

case intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε ≠ ⊤
case intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ↑(f a) ∂μ) ≤ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ↑(g a) ∂μ) + ↑ε
convert ENNReal.toReal_mono _ gint
no goals
case h.e'_3.h.e'_1.h.e'_4.h
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
x✝ : α
⊢ ENNReal.ofReal ↑(f x✝) = ↑(f x✝)
simp
case h.e'_4
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ↑(g a) ∂μ) + ↑ε =
    ENNReal.toReal (∫⁻ (x : α), ↑(g x) ∂μ) + ENNReal.toReal ↑ε
case h.e'_4
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ↑(g a) ∂μ) + ↑ε = ENNReal.toReal ((∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε)
rw [ENNReal.toReal_add Ig.ne ENNReal.coe_ne_top]
no goals
case h.e'_4
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ↑(g a) ∂μ) + ↑ε =
    ENNReal.toReal (∫⁻ (x : α), ↑(g x) ∂μ) + ENNReal.toReal ↑ε
simp
no goals
case intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε ≠ ⊤
simpa using Ig.ne
case intro.intro.intro.intro.refine'_2.hf.hp
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ ∀ (x : α), OfNat.ofNat 0 x ≤ (fun x => ↑(g x)) x
case intro.intro.intro.intro.refine'_2.hf
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ 0 ≤ᶠ[ae μ] fun x => ↑(g x)
apply Filter.eventually_of_forall
no goals
case intro.intro.intro.intro.refine'_2.hf.hp
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ ∀ (x : α), OfNat.ofNat 0 x ≤ (fun x => ↑(g x)) x
simp
no goals
case intro.intro.intro.intro.refine'_2.hfm
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ AEStronglyMeasurable (fun x => ↑(g x)) μ
exact gcont.measurable.coe_nnreal_real.aemeasurable.aestronglyMeasurable
case intro.intro.intro.intro.refine'_2.hf.hp
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ ∀ (x : α), OfNat.ofNat 0 x ≤ (fun x => ↑(f x)) x
case intro.intro.intro.intro.refine'_2.hf
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ 0 ≤ᶠ[ae μ] fun x => ↑(f x)
apply Filter.eventually_of_forall
no goals
case intro.intro.intro.intro.refine'_2.hf.hp
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ ∀ (x : α), OfNat.ofNat 0 x ≤ (fun x => ↑(f x)) x
simp
no goals
case intro.intro.intro.intro.refine'_2.hfm
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : WeaklyRegular μ
f : α → ℝ≥0
fint : Integrable fun x => ↑(f x)
ε : ℝ≥0
εpos : 0 < ↑ε
If : (∫⁻ (x : α), ↑(f x) ∂μ) < ⊤
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : (∫⁻ (x : α), ↑(f x) ∂μ) ≤ (∫⁻ (x : α), ↑(g x) ∂μ) + ↑ε
Ig : (∫⁻ (x : α), ↑(g x) ∂μ) < ⊤
⊢ AEStronglyMeasurable (fun x => ↑(f x)) μ
exact fint.aestronglyMeasurable