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
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g₁ x
g₁cont : LowerSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), (f₂ : (a : α) → ℝ≥0) x ≤ g₂ x
g₂cont : LowerSemicontinuous g₂
g₂int : ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ε
have h : ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ε =
  ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2 +
    (∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2)
Tactic: convert! add_le_add g₁int g₂int using 1
-- 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
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g₁ x
g₁cont : LowerSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), (f₂ : (a : α) → ℝ≥0) x ≤ g₂ x
g₂cont : LowerSemicontinuous g₂
g₂int : ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
| ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ε
have rw : ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + (ε / 2 + ε / 2)
Tactic: rw [← ENNReal.add_halves ε]
-- 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
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g₁ x
g₁cont : LowerSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), (f₂ : (a : α) → ℝ≥0) x ≤ g₂ x
g₂cont : LowerSemicontinuous g₂
g₂int : ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ε =
    ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2 +
      (∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2)
have h : ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ +
    (ε / 2 + ε / 2) =
  ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2 +
    (∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2)
Tactic: conv_lhs => rw [← ENNReal.add_halves ε]
-- 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
⊢ ∃ (g : α → ℝ≥0∞), (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
have rcases : ∀ (δ : ℕ → ℝ≥0∞) (δpos : ∀ (i : ℕ), 0 < δ i) (hδ : ∑' (i : ℕ), δ i < ε),
  ∃ (g : α → ℝ≥0∞), (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
Tactic: rcases ENNReal.exists_pos_sum_of_countable' εpos ℕ with ⟨δ, δpos, hδ⟩
-- 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
⊢ ∃ (g : α → ℝ≥0∞), (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
have this : ∀ (n : ℕ),
  ∃ (g : α → ℝ≥0),
    (∀ (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g x) ∧
      LowerSemicontinuous g ∧
        ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
Tactic: have :
    ∀ n,
      ∃ g : α → ℝ≥0,
        (∀ x, eapproxDiff f n x ≤ g x) ∧
          LowerSemicontinuous g ∧
            (∫⁻ x, g x ∂μ) ≤ (∫⁻ x, eapproxDiff f n x ∂μ) + δ n :=
    fun n =>
    SimpleFunc.exists_le_lowerSemicontinuous_lintegral_ge μ (eapproxDiff f n)
      (δpos n).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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
this :
  ∀ (n : ℕ),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧
          ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤
            ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
⊢ ∃ (g : α → ℝ≥0∞), (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
have choose : ∀ (g : (n : ℕ) → α → ℝ≥0) (f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x)
  (gcont : ∀ (n : ℕ), LowerSemicontinuous (g n))
  (hg :
    ∀ (n : ℕ),
      ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤
        ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n),
  ∃ (g : α → ℝ≥0∞), (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
Tactic: choose g f_le_g gcont hg using this
Cleared hypotheses: this
-- 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
⊢ ∃ (g : α → ℝ≥0∞), (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
have refine_1 : ∀ (x : α), f x ≤ (fun (x : α) ↦ (∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) : ℝ≥0∞)) x
Tactic: refine ⟨fun x => ∑' n, g n x, fun x => ?_, ?_, ?_⟩
-- 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
refine_1 : ∀ (x : α), f x ≤ (fun (x : α) ↦ (∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) : ℝ≥0∞)) x
⊢ ∃ (g : α → ℝ≥0∞), (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
have refine_2 : LowerSemicontinuous (β := ℝ≥0∞) fun (x : α) ↦ ∑' (n : ℕ), (↑(g n x) : ℝ≥0∞)
Tactic: refine ⟨fun x => ∑' n, g n x, fun x => ?_, ?_, ?_⟩
-- 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
refine_1 : ∀ (x : α), f x ≤ (fun (x : α) ↦ (∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) : ℝ≥0∞)) x
refine_2 : LowerSemicontinuous (β := ℝ≥0∞) fun (x : α) ↦ ∑' (n : ℕ), (↑(g n x) : ℝ≥0∞)
⊢ ∃ (g : α → ℝ≥0∞), (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
have refine_3 : ∫⁻ (x : α), (fun (x : α) ↦ (∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) : ℝ≥0∞)) x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
Tactic: refine ⟨fun x => ∑' n, g n x, fun x => ?_, ?_, ?_⟩
-- 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
x : α
⊢ f x ≤ (fun (x : α) ↦ (∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) : ℝ≥0∞)) x
have refine_1 : LE.le (α := ℝ≥0∞) (∑' (n : ℕ), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞))
  ((fun (x : α) ↦ (∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) : ℝ≥0∞)) x)
Tactic: rw [← tsum_eapproxDiff f hf]
-- 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
⊢ LowerSemicontinuous (β := ℝ≥0∞) fun (x : α) ↦ ∑' (n : ℕ), (↑(g n x) : ℝ≥0∞)
have refine_2 : ∀ (n : ℕ), LowerSemicontinuous (β := ℝ≥0∞) fun (x : α) ↦ (↑(g n x) : ℝ≥0∞)
Tactic: refine lowerSemicontinuous_tsum fun n => ?_
-- 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
⊢ ∫⁻ (x : α), ∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) ∂μ = ∑' (n : ℕ), ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ
have rw : Eq (α := ℝ≥0∞) (∑' (i : ℕ), ∫⁻ (a : α), (↑(g i a) : ℝ≥0∞) ∂μ) (∑' (n : ℕ), ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ)
Tactic: rw [lintegral_tsum fun n => (gcont n).measurable.coe_nnreal_ennreal.aemeasurable]
-- 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑' (n : ℕ), ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ)
      (∑' (n : ℕ), δ n) ≤
    ∫⁻ (x : α), f x ∂μ + ε
have refine : ∑' (n : ℕ), ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), f x ∂μ
Tactic: refine add_le_add ?_ hδ.le
-- 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
⊢ ∑' (n : ℕ), ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), f x ∂μ
have rw : ∫⁻ (a : α), ∑' (i : ℕ), (↑(((eapproxDiff f i : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), f x ∂μ
Tactic: rw [← lintegral_tsum]
-- 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
rw : ∫⁻ (a : α), ∑' (i : ℕ), (↑(((eapproxDiff f i : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), f x ∂μ
⊢ ∑' (n : ℕ), ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), f x ∂μ
have rw₁ : ∀ (i : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(((eapproxDiff f i : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞)) μ
Tactic: rw [← lintegral_tsum]
-- 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
⊢ ∫⁻ (a : α), ∑' (i : ℕ), (↑(((eapproxDiff f i : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), f x ∂μ
have simp_rw : ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), f a ∂μ
Tactic: simp_rw [tsum_eapproxDiff f hf, le_refl]
-- 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
⊢ ∫⁻ (x : α), (fun (x : α) ↦ (∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) : ℝ≥0∞)) x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
have n : ∫⁻ (x : α), ∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) ∂μ = ∑' (n : ℕ), ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ
Tactic: calc
      ∫⁻ x, ∑' n : ℕ, g n x ∂μ = ∑' n, ∫⁻ x, g n x ∂μ := by
        rw [lintegral_tsum fun n => (gcont n).measurable.coe_nnreal_ennreal.aemeasurable]
      _ ≤ ∑' n, ((∫⁻ x, eapproxDiff f n x ∂μ) + δ n) := ENNReal.tsum_le_tsum hg
      _ = ∑' n, ∫⁻ x, eapproxDiff f n x ∂μ + ∑' n, δ n := ENNReal.tsum_add
      _ ≤ (∫⁻ x : α, f x ∂μ) + ε := by
        refine add_le_add ?_ hδ.le
        rw [← lintegral_tsum]
        · simp_rw [tsum_eapproxDiff f hf, le_refl]
        · intro n; exact (SimpleFunc.measurable _).coe_nnreal_ennreal.aemeasurable
-- 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
n : ∫⁻ (x : α), ∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) ∂μ = ∑' (n : ℕ), ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ
⊢ ∫⁻ (x : α), (fun (x : α) ↦ (∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) : ℝ≥0∞)) x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
have n₁ : HAdd.hAdd (α := ℝ≥0∞) (∑' (n : ℕ), ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ)
    (∑' (n : ℕ), δ n) ≤
  ∫⁻ (x : α), f x ∂μ + ε
Tactic: calc
      ∫⁻ x, ∑' n : ℕ, g n x ∂μ = ∑' n, ∫⁻ x, g n x ∂μ := by
        rw [lintegral_tsum fun n => (gcont n).measurable.coe_nnreal_ennreal.aemeasurable]
      _ ≤ ∑' n, ((∫⁻ x, eapproxDiff f n x ∂μ) + δ n) := ENNReal.tsum_le_tsum hg
      _ = ∑' n, ∫⁻ x, eapproxDiff f n x ∂μ + ∑' n, δ n := ENNReal.tsum_add
      _ ≤ (∫⁻ x : α, f x ∂μ) + ε := by
        refine add_le_add ?_ hδ.le
        rw [← lintegral_tsum]
        · simp_rw [tsum_eapproxDiff f hf, le_refl]
        · intro n; exact (SimpleFunc.measurable _).coe_nnreal_ennreal.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
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have this : ε / 2 ≠ 0
Tactic: have : ε / 2 ≠ 0 := (ENNReal.half_pos ε0).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
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have rcases : ∀ (w : α → ℝ≥0) (wpos : ∀ (x : α), 0 < w x) (wmeas : Measurable w) (wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2),
  ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
Tactic: rcases exists_pos_lintegral_lt_of_sigmaFinite μ this with ⟨w, wpos, wmeas, wint⟩
-- 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 : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have rcases : ∀ (g : α → ℝ≥0∞) (le_g : ∀ (x : α), f' x ≤ g x) (gcont : LowerSemicontinuous g)
  (gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2),
  ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
Tactic: rcases exists_le_lowerSemicontinuous_lintegral_ge μ f' (fmeas.add wmeas).coe_nnreal_ennreal
      this with
    ⟨g, le_g, gcont, gint⟩
-- 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 : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have refine_1 : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
Tactic: refine ⟨g, fun x => ?_, gcont, ?_⟩
-- 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 : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
refine_1 : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have refine_2 : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
Tactic: refine ⟨g, fun x => ?_, gcont, ?_⟩