awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), (f₁ + f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
      LowerSemicontinuous g ∧
        ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε

Tactic:
⟨fun x => g₁ x + g₂ x, fun x => add_le_add (f₁_le_g₁ x) (f₂_le_g₂ x), g₁cont.add g₂cont, ?_⟩

Premises used: LowerSemicontinuous.add, add_le_add, HAdd.hAdd, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
add :
  ∫⁻ (x : α), (↑((fun (x : α) ↦ g₁ x + g₂ x) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), (f₁ + f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
      LowerSemicontinuous g ∧
        ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε

Tactic:
refine
      ⟨fun x => g₁ x + g₂ x, fun x => add_le_add (f₁_le_g₁ x) (f₂_le_g₂ x), g₁cont.add g₂cont, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
add :
  ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) + (↑(g₂ x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) + (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
⊢ ∫⁻ (x : α), (↑((fun (x : α) ↦ g₁ x + g₂ x) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε

Tactic:
simp only [SimpleFunc.coe_add, ENNReal.coe_add, Pi.add_apply]

Premises used: MeasureTheory.SimpleFunc.coe_add, ENNReal.coe_add, Pi.add_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
add :
  ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ε
⊢ ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) + (↑(g₂ x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) + (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε

Tactic:
rw [lintegral_add_left f₁.measurable.coe_nnreal_ennreal,
      lintegral_add_left g₁cont.measurable.coe_nnreal_ennreal]

Premises used: Measurable.coe_nnreal_ennreal, MeasureTheory.SimpleFunc.measurable, MeasureTheory.lintegral_add_left, LowerSemicontinuous.measurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
⊢ ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2 +
      (∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2)

Tactic:
add_le_add g₁int g₂int

Premises used: add_le_add
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
h_1 :
  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
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)
⊢ ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ε

Tactic:
convert! add_le_add g₁int g₂int using 1

Premises used: add_le_add
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
rw :
  ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ +
    (ε / 2 + ε / 2)
| ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ε

Tactic:
rw [← ENNReal.add_halves ε]

Premises used: ENNReal.add_halves
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
h_1 :
  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
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)
⊢ ∫⁻ (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:
conv_lhs => rw [← ENNReal.add_halves ε]

Premises used: ENNReal.add_halves
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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∞) ∂μ +
      (ε / 2 + ε / 2) =
    ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2 +
      (∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2)

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
rcases :
  ∀ (δ : ℕ → ℝ≥0∞) (δpos : ∀ (i : ℕ), 0 < δ i) (hδ : ∑' (i : ℕ), δ i < ε),
    ∃ (g : α → ℝ≥0∞), (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
⊢ ∃ (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δ⟩

Premises used: ENNReal.exists_pos_sum_of_countable', Nat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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 < ε
⊢ ∀ (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'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
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 ∂μ + ε
⊢ ∃ (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
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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 ∂μ + ε

Tactic:
⟨fun x => ∑' n, g n x, fun x => ?_, ?_, ?_⟩

Premises used: ENNReal.ofNNReal, tsum, Nat, And.intro, Exists.intro, SummationFilter.unconditional
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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∞)
refine_3 : ∫⁻ (x : α), (fun (x : α) ↦ (∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) : ℝ≥0∞)) x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
⊢ ∃ (g : α → ℝ≥0∞), (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε

Tactic:
refine ⟨fun x => ∑' n, g n x, fun x => ?_, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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 : α
refine_1 :
  LE.le (α := ℝ≥0∞) (∑' (n : ℕ), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞))
    ((fun (x : α) ↦ (∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) : ℝ≥0∞)) x)
⊢ f x ≤ (fun (x : α) ↦ (∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) : ℝ≥0∞)) x

Tactic:
rw [← tsum_eapproxDiff f hf]

Premises used: MeasureTheory.SimpleFunc.tsum_eapproxDiff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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 : α
⊢ LE.le (α := ℝ≥0∞) (∑' (n : ℕ), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞))
    ((fun (x : α) ↦ (∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) : ℝ≥0∞)) x)

Tactic:
ENNReal.tsum_le_tsum fun n => ENNReal.coe_le_coe.2 (f_le_g n x)

Premises used: Iff.mpr, ENNReal.tsum_le_tsum, ENNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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 : α
⊢ LE.le (α := ℝ≥0∞) (∑' (n : ℕ), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞))
    ((fun (x : α) ↦ (∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) : ℝ≥0∞)) x)

Tactic:
exact ENNReal.tsum_le_tsum fun n => ENNReal.coe_le_coe.2 (f_le_g n x)

Premises used: Iff.mpr, ENNReal.tsum_le_tsum, ENNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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∞)

Tactic:
lowerSemicontinuous_tsum fun n => ?_

Premises used: lowerSemicontinuous_tsum
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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_2 : ∀ (n : ℕ), LowerSemicontinuous (β := ℝ≥0∞) fun (x : α) ↦ (↑(g n x) : ℝ≥0∞)
⊢ LowerSemicontinuous (β := ℝ≥0∞) fun (x : α) ↦ ∑' (n : ℕ), (↑(g n x) : ℝ≥0∞)

Tactic:
refine lowerSemicontinuous_tsum fun n => ?_

Premises used: lowerSemicontinuous_tsum