awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / (↑N : ℝ)
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
    PairwiseDisjoint univ E ∧
      (∀ (n : Fin N),
          ∀ x ∈ E n,
            a + ε' * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
              (f : (a : X) → ℝ) x ≤ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
        ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Fin N → Opens X
hV :
  ∀ (n : Fin N),
    E n ⊆ (↑(V n) : Set X) ∧
      (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
        (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
n : Fin N
hn : Membership.mem (γ := Finset (Fin N)) Finset.univ n
⊢ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ))) < ∞
have rw : LT.lt (α := WithTop NNReal) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (⊤ : WithTop NNReal) ∧
  ENNReal.ofReal (ε' / (↑N : ℝ)) < ⊤
Tactic: rw [WithTop.add_lt_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / (↑N : ℝ)
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
    PairwiseDisjoint univ E ∧
      (∀ (n : Fin N),
          ∀ x ∈ E n,
            a + ε' * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
              (f : (a : X) → ℝ) x ≤ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
        ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Fin N → Opens X
hV :
  ∀ (n : Fin N),
    E n ⊆ (↑(V n) : Set X) ∧
      (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
        (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
n : Fin N
hn : Membership.mem (γ := Finset (Fin N)) Finset.univ n
⊢ μ.real (↑(V n) : Set X) ≤ μ.real (E n) + ε' / (↑N : ℝ)
have rw : μ.real (↑(V n) : Set X) ≤ μ.real (E n) + (ENNReal.ofReal (ε' / (↑N : ℝ))).toReal
Tactic: rw [← ENNReal.toReal_ofReal (div_nonneg (le_of_lt hε'.1) (Nat.cast_nonneg _))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / (↑N : ℝ)
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
    PairwiseDisjoint univ E ∧
      (∀ (n : Fin N),
          ∀ x ∈ E n,
            a + ε' * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
              (f : (a : X) → ℝ) x ≤ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
        ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Fin N → Opens X
hV :
  ∀ (n : Fin N),
    E n ⊆ (↑(V n) : Set X) ∧
      (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
        (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
n : Fin N
hn : Membership.mem (γ := Finset (Fin N)) Finset.univ n
⊢ μ.real (↑(V n) : Set X) ≤ μ.real (E n) + (ENNReal.ofReal (ε' / (↑N : ℝ))).toReal
have apply : ENNReal.ofReal (ε' / (↑N : ℝ)) ≠ ∞
Tactic: apply ENNReal.toReal_le_add (hV n).2.2 (hE' n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / (↑N : ℝ)
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
    PairwiseDisjoint univ E ∧
      (∀ (n : Fin N),
          ∀ x ∈ E n,
            a + ε' * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
              (f : (a : X) → ℝ) x ≤ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
        ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Fin N → Opens X
hV :
  ∀ (n : Fin N),
    E n ⊆ (↑(V n) : Set X) ∧
      (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
        (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
n : Fin N
hn : Membership.mem (γ := Finset (Fin N)) Finset.univ n
⊢ (Λ : (a : X →C_c ℝ) → ℝ) (g n) ≤ μ.real (E n) + ε' / (↑N : ℝ)
have _ : (Λ : (a : X →C_c ℝ) → ℝ) (g n) ≤ μ.real (↑(V n) : Set X)
Tactic: calc
        _ ≤ μ.real (V n) := by
          apply (ENNReal.ofReal_le_iff_le_toReal _).mp
          · exact le_rieszMeasure_tsupport_subset Λ (fun x ↦ hg.2.2.1 n x) (hg.1 n)
          · rw [← lt_top_iff_ne_top]
            apply lt_of_le_of_lt (hV n).2.2
            rw [WithTop.add_lt_top]
            exact ⟨WithTop.lt_top_iff_ne_top.mpr (hE' n), ENNReal.ofReal_lt_top⟩
        _ ≤ _ := by
          rw [← ENNReal.toReal_ofReal (div_nonneg (le_of_lt hε'.1) (Nat.cast_nonneg _))]
          apply ENNReal.toReal_le_add (hV n).2.2 (hE' n)
          · finiteness
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / (↑N : ℝ)
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
    PairwiseDisjoint univ E ∧
      (∀ (n : Fin N),
          ∀ x ∈ E n,
            a + ε' * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
              (f : (a : X) → ℝ) x ≤ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
        ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Fin N → Opens X
hV :
  ∀ (n : Fin N),
    E n ⊆ (↑(V n) : Set X) ∧
      (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
        (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
n : Fin N
hn : Membership.mem (γ := Finset (Fin N)) Finset.univ n
_ : (Λ : (a : X →C_c ℝ) → ℝ) (g n) ≤ μ.real (↑(V n) : Set X)
⊢ (Λ : (a : X →C_c ℝ) → ℝ) (g n) ≤ μ.real (E n) + ε' / (↑N : ℝ)
have _₁ : μ.real (↑(V n) : Set X) ≤ μ.real (E n) + ε' / (↑N : ℝ)
Tactic: calc
        _ ≤ μ.real (V n) := by
          apply (ENNReal.ofReal_le_iff_le_toReal _).mp
          · exact le_rieszMeasure_tsupport_subset Λ (fun x ↦ hg.2.2.1 n x) (hg.1 n)
          · rw [← lt_top_iff_ne_top]
            apply lt_of_le_of_lt (hV n).2.2
            rw [WithTop.add_lt_top]
            exact ⟨WithTop.lt_top_iff_ne_top.mpr (hE' n), ENNReal.ofReal_lt_top⟩
        _ ≤ _ := by
          rw [← ENNReal.toReal_ofReal (div_nonneg (le_of_lt hε'.1) (Nat.cast_nonneg _))]
          apply ENNReal.toReal_le_add (hV n).2.2 (hE' n)
          · finiteness
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / (↑N : ℝ)
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
    PairwiseDisjoint univ E ∧
      (∀ (n : Fin N),
          ∀ x ∈ E n,
            a + ε' * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
              (f : (a : X) → ℝ) x ≤ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
        ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Fin N → Opens X
hV :
  ∀ (n : Fin N),
    E n ⊆ (↑(V n) : Set X) ∧
      (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
        (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
⊢ ∑ n : Fin N, (|a| + y n + ε') * (μ.real (E n) + ε' / (↑N : ℝ)) - |a| * ∑ n : Fin N, (Λ : (a : X →C_c ℝ) → ℝ) (g n) ≤
    ∑ n : Fin N, (|a| + y n + ε') * (μ.real (E n) + ε' / (↑N : ℝ)) - |a| * μ.real K
have calc_4 : μ.real K ≤ ∑ n : Fin N, (Λ : (a : X →C_c ℝ) → ℝ) (g n)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / (↑N : ℝ)
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
    PairwiseDisjoint univ E ∧
      (∀ (n : Fin N),
          ∀ x ∈ E n,
            a + ε' * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
              (f : (a : X) → ℝ) x ≤ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
        ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Fin N → Opens X
hV :
  ∀ (n : Fin N),
    E n ⊆ (↑(V n) : Set X) ∧
      (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
        (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
⊢ μ.real K ≤ ∑ n : Fin N, (Λ : (a : X →C_c ℝ) → ℝ) (g n)
have calc_4 : μ.real K ≤ (Λ : (a : X →C_c ℝ) → ℝ) (∑ x : Fin N, g x)
Tactic: rw [← map_sum Λ g _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / (↑N : ℝ)
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
    PairwiseDisjoint univ E ∧
      (∀ (n : Fin N),
          ∀ x ∈ E n,
            a + ε' * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
              (f : (a : X) → ℝ) x ≤ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
        ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Fin N → Opens X
hV :
  ∀ (n : Fin N),
    E n ⊆ (↑(V n) : Set X) ∧
      (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
        (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
⊢ μ.real K ≤ (Λ : (a : X →C_c ℝ) → ℝ) (∑ x : Fin N, g x)
have h : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((∑ n : Fin N, g n : (a : X) → ℝ) x : ℝ)
Tactic: have h x : 0 ≤ (∑ n, g n) x := by simpa using Fintype.sum_nonneg fun n ↦ (hg.2.2.1 n x).1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / (↑N : ℝ)
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
    PairwiseDisjoint univ E ∧
      (∀ (n : Fin N),
          ∀ x ∈ E n,
            a + ε' * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
              (f : (a : X) → ℝ) x ≤ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
        ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Fin N → Opens X
hV :
  ∀ (n : Fin N),
    E n ⊆ (↑(V n) : Set X) ∧
      (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
        (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
h : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((∑ n : Fin N, g n : (a : X) → ℝ) x : ℝ)
⊢ μ.real K ≤ (Λ : (a : X →C_c ℝ) → ℝ) (∑ x : Fin N, g x)
have calc_4 : LE.le (α := ℝ) (0 : ℝ) ((Λ : (a : X →C_c ℝ) → ℝ) (∑ x : Fin N, g x) : ℝ)
Tactic: apply ENNReal.toReal_le_of_le_ofReal
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / (↑N : ℝ)
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
    PairwiseDisjoint univ E ∧
      (∀ (n : Fin N),
          ∀ x ∈ E n,
            a + ε' * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
              (f : (a : X) → ℝ) x ≤ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
        ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Fin N → Opens X
hV :
  ∀ (n : Fin N),
    E n ⊆ (↑(V n) : Set X) ∧
      (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
        (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
h : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((∑ n : Fin N, g n : (a : X) → ℝ) x : ℝ)
calc_4 : LE.le (α := ℝ) (0 : ℝ) ((Λ : (a : X →C_c ℝ) → ℝ) (∑ x : Fin N, g x) : ℝ)
⊢ μ.real K ≤ (Λ : (a : X →C_c ℝ) → ℝ) (∑ x : Fin N, g x)
have calc_4₁ : (μ : (a : Set X) → ℝ≥0∞) K ≤ ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) (∑ x : Fin N, g x))
Tactic: apply ENNReal.toReal_le_of_le_ofReal
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / (↑N : ℝ)
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
    PairwiseDisjoint univ E ∧
      (∀ (n : Fin N),
          ∀ x ∈ E n,
            a + ε' * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
              (f : (a : X) → ℝ) x ≤ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
        ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Fin N → Opens X
hV :
  ∀ (n : Fin N),
    E n ⊆ (↑(V n) : Set X) ∧
      (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
        (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
h : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((∑ n : Fin N, g n : (a : X) → ℝ) x : ℝ)
⊢ (μ : (a : Set X) → ℝ≥0∞) K ≤ ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) (∑ x : Fin N, g x))
have h' : ∀ (x : X) (hx : x ∈ K), Eq (α := ℝ) ((∑ n : Fin N, g n : (a : X) → ℝ) x : ℝ) (1 : ℝ)
Tactic: have h' x (hx : x ∈ K) : (∑ n, g n) x = 1 := by simp [hg.2.1 hx]