awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
refine_1 : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∫⁻ (x : α), g0 x ∂μ + ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + (0 + ε / 2)
have refine_2 : ∫⁻ (x : α), g1 x ∂μ ≤ 0 + ε / 2
Tactic: refine add_le_add ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
⊢ ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2
have h : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ = ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ
Tactic: convert! g0_int using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
⊢ ∫⁻ (x : α), g1 x ∂μ ≤ 0 + ε / 2
have h : 0 = ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ
Tactic: convert! g1_int
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
⊢ ∫⁻ (x : α), (fun (x : α) ↦ g0 x + g1 x) x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have g0₁ : ∫⁻ (x : α), g0 x ∂μ + ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + (0 + ε / 2)
Tactic: calc
      ∫⁻ x, g0 x + g1 x ∂μ = (∫⁻ x, g0 x ∂μ) + ∫⁻ x, g1 x ∂μ :=
        lintegral_add_left g0_cont.measurable _
      _ ≤ (∫⁻ x, f x ∂μ) + ε / 2 + (0 + ε / 2) := by
        refine add_le_add ?_ ?_
        · convert! g0_int using 2
          exact lintegral_congr_ae (fmeas.ae_eq_mk.fun_comp _)
        · convert! g1_int
          simp only [smeas, μs, lintegral_const, Set.univ_inter, MeasurableSet.univ,
            lintegral_indicator, mul_zero, restrict_apply]
      _ = (∫⁻ x, f x ∂μ) + ε := by simp only [add_assoc, ENNReal.add_halves, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
g0₁ : ∫⁻ (x : α), g0 x ∂μ + ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + (0 + ε / 2)
⊢ ∫⁻ (x : α), (fun (x : α) ↦ g0 x + g1 x) x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have g0₂ : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + (0 + ε / 2) = ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
Tactic: calc
      ∫⁻ x, g0 x + g1 x ∂μ = (∫⁻ x, g0 x ∂μ) + ∫⁻ x, g1 x ∂μ :=
        lintegral_add_left g0_cont.measurable _
      _ ≤ (∫⁻ x, f x ∂μ) + ε / 2 + (0 + ε / 2) := by
        refine add_le_add ?_ ?_
        · convert! g0_int using 2
          exact lintegral_congr_ae (fmeas.ae_eq_mk.fun_comp _)
        · convert! g1_int
          simp only [smeas, μs, lintegral_const, Set.univ_inter, MeasurableSet.univ,
            lintegral_indicator, mul_zero, restrict_apply]
      _ = (∫⁻ x, f x ∂μ) + ε := by simp only [add_assoc, ENNReal.add_halves, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ
εpos : 0 < ε
⊢ AEMeasurable f μ
have h : ∀ (x : α), f x = (↑(f x) : ℝ).toNNReal
Tactic: convert! fint.aestronglyMeasurable.real_toNNReal.aemeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ
εpos : 0 < ε
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + ε
have fmeas : AEMeasurable f μ
Tactic: have fmeas : AEMeasurable f μ := by
    convert! fint.aestronglyMeasurable.real_toNNReal.aemeasurable
    simp only [Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ
εpos : 0 < ε
fmeas : AEMeasurable f μ
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + ε
have lift : ∀ (ε : ℝ≥0) (εpos : 0 < (↑ε : ℝ)),
  ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
Tactic: lift ε to ℝ≥0 using εpos.le
Cleared hypotheses: ε, εpos
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
have obtain : ∀ (δ : ℝ≥0) (δpos : 0 < δ) (hδε : δ < ε),
  ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
Tactic: obtain ⟨δ, δpos, hδε⟩ : ∃ δ : ℝ≥0, 0 < δ ∧ δ < ε := exists_between εpos
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
have int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
Tactic: have int_f_ne_top : (∫⁻ a : α, f a ∂μ) ≠ ∞ :=
    (hasFiniteIntegral_iff_ofNNReal.1 fint.hasFiniteIntegral).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : 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) : ℝ≥0∞) ∂μ ≠ ∞
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
have rcases : ∀ (g : α → ℝ≥0∞) (f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) (gcont : LowerSemicontinuous g)
  (gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)),
  ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
Tactic: rcases exists_lt_lowerSemicontinuous_lintegral_ge_of_aemeasurable μ f fmeas
      (ENNReal.coe_ne_zero.2 δpos.ne') with
    ⟨g, f_lt_g, gcont, gint⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : 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) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
have gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
Tactic: have gint_ne : (∫⁻ x : α, g x ∂μ) ≠ ∞ := ne_top_of_le_ne_top (by simpa) gint
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : 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) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
have g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Tactic: have g_lt_top : ∀ᵐ x : α ∂μ, g x < ∞ := ae_lt_top gcont.measurable gint_ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : 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) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
⊢ ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
have h : (fun (a : α) ↦ ENNReal.ofReal (g a).toReal) =ᶠ[ae μ] g
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : 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) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
⊢ (fun (a : α) ↦ ENNReal.ofReal (g a).toReal) =ᶠ[ae μ] g
have h : ∀ (a : α) (hx : g a < ∞), ENNReal.ofReal (g a).toReal = g a
Tactic: filter_upwards [g_lt_top] with _ hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : 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) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
have Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
Tactic: 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, not_false_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : 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) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
have refine_1 : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
Tactic: refine ⟨g, f_lt_g, gcont, g_lt_top, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : 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) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
refine_1 : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
have refine_2 : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
Tactic: refine ⟨g, f_lt_g, gcont, g_lt_top, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : 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) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
have refine_1 : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
Tactic: refine ⟨gcont.measurable.ennreal_toReal.aemeasurable.aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : 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) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
have refine_1 : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ < ∞
Tactic: simp only [hasFiniteIntegral_iff_norm, Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : 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) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
have refine_2 : (∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ).toReal < (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal + (↑ε : ℝ)
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : 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) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
refine_2 :
  (∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ).toReal < (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal + (↑ε : ℝ)
⊢ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
have refine_2₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(f x) : ℝ)
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]