awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ trapezoidal_error f 1 a t
dg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
bound_ddg : ∀ (x : ℝ) (hx : x ∈ Set.Icc a b), |ddg x| ≤ ζ / 2 * HPow.hPow (β := ℕ) (x - a) 1
φ φ' : ℝ → ℝ
h : ∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x
h0 : φ a = 0
c : ℝ
n : ℕ
h_bound : ∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n
t : ℝ
ht : t ∈ Set.Icc a b
⊢ |φ t| ≤ c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (t - a) ^ (n + 1)
have hB : ∀ (x : ℝ), HasDerivAt (fun (y : ℝ) ↦ c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (y - a) ^ (n + 1)) (c * (x - a) ^ n) x
Tactic: have hB (x) : HasDerivAt (fun y ↦ c / (n + 1) * (y - a) ^ (n + 1)) (c * (x - a) ^ n) x := by
      convert!
        (hasDerivAt_const x (c / (n + 1))).mul
          (((hasDerivAt_id x).sub (hasDerivAt_const x a)).pow (n + 1)) using 1
      simp [sub_eq_add_neg, field]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ trapezoidal_error f 1 a t
dg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
bound_ddg : ∀ (x : ℝ) (hx : x ∈ Set.Icc a b), |ddg x| ≤ ζ / 2 * HPow.hPow (β := ℕ) (x - a) 1
⊢ |trapezoidal_error f 1 a b| ≤ ζ / 12 * HPow.hPow (β := ℕ) (b - a) 3
have key : ∀ {φ φ' : ℝ → ℝ} (h : ∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x) (h0 : φ a = 0) {c : ℝ} {n : ℕ}
  (h_bound : ∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n),
  ∀ t ∈ Set.Icc a b, |φ t| ≤ c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (t - a) ^ (n + 1)
Tactic: have key {φ φ' : ℝ → ℝ} (h : ∀ x ∈ Icc a b, HasDerivWithinAt φ (φ' x) (Icc a b) x) (h0 : φ a = 0)
      {c : ℝ} {n : ℕ} (h_bound : ∀ t ∈ Icc a b, |φ' t| ≤ c * (t - a) ^ n) :
      ∀ t ∈ Icc a b, |φ t| ≤ c / (n + 1) * (t - a) ^ (n + 1) := by
    intro t ht
    have hB (x) : HasDerivAt (fun y ↦ c / (n + 1) * (y - a) ^ (n + 1)) (c * (x - a) ^ n) x := by
      convert!
        (hasDerivAt_const x (c / (n + 1))).mul
          (((hasDerivAt_id x).sub (hasDerivAt_const x a)).pow (n + 1)) using 1
      simp [sub_eq_add_neg, field]
    simpa [Real.norm_eq_abs, h0] using image_norm_le_of_norm_deriv_right_le_deriv_boundary
      (fun x hx ↦ (h x hx).continuousWithinAt)
      (fun x hx ↦ by grind [Icc_mem_nhdsGE_of_mem, mono_of_mem_nhdsWithin])
      (by simp [h0]) hB (fun x hx ↦ h_bound x (Ico_subset_Icc_self hx)) ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) (b - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
Tactic: have h0 : ∀ k : ℕ, ak (k + 1) - ak k = h := by simp [ak, ← sub_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) (b - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have hab : 0 < b - a
Tactic: have hab : 0 < b - a := sub_pos.mpr a_lt_b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) (b - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have hpos : 0 < h
Tactic: have hpos : 0 < h := by positivity
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) (b - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have hb : b = a + (↑N : ℝ) * h
Tactic: have hb : b = a + N * h := by field
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) (b - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have rw : |∑ i ∈ Finset.range N, trapezoidal_error f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h)| ≤
  HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
Tactic: rw [hb, ← sum_trapezoidal_error_adjacent_intervals N_nonzero
    (hb ▸ h_df.continuousOn.intervalIntegrable_of_Icc a_lt_b.le)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
⊢ |∑ i ∈ Finset.range N, trapezoidal_error f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h)| ≤
    HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have grw : ∑ i ∈ Finset.range N, |trapezoidal_error f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h)| ≤
  HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
Tactic: grw [abs_sum_le_sum_abs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
this : ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
⊢ ∑ i ∈ Finset.range N, |trapezoidal_error f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h)| ≤
    HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have norm_cast : ∑ x ∈ Finset.range N, |trapezoidal_error f 1 (a + (↑x : ℝ) * h) (a + (↑(x + 1) : ℝ) * h)| ≤
  HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (↑(12 * HPow.hPow (β := ℕ) N 2) : ℝ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
this : ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
⊢ (↑N : ℝ) * (ζ / 12 * HPow.hPow (β := ℕ) h 3) =
    HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (↑(12 * HPow.hPow (β := ℕ) N 2) : ℝ)
have push_cast : (↑N : ℝ) * (ζ / 12 * HPow.hPow (β := ℕ) h 3) =
  HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
this : ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
⊢ ∑ x ∈ Finset.range N, |trapezoidal_error f 1 (a + (↑x : ℝ) * h) (a + (↑(x + 1) : ℝ) * h)| ≤
    HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (↑(12 * HPow.hPow (β := ℕ) N 2) : ℝ)
have _ : ∑ k ∈ Finset.range N, ζ / 12 * HPow.hPow (β := ℕ) h 3 = (↑N : ℝ) * (ζ / 12 * HPow.hPow (β := ℕ) h 3)
Tactic: calc
      _ ≤ ∑ k ∈ range N, ζ / 12 * h ^ 3 := sum_le_sum this
      _ = N * (ζ / 12 * h ^ 3)          := by simp [sum_const]
      _ = _                             := by push_cast; field
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
this : ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
_ : ∑ k ∈ Finset.range N, ζ / 12 * HPow.hPow (β := ℕ) h 3 = (↑N : ℝ) * (ζ / 12 * HPow.hPow (β := ℕ) h 3)
⊢ ∑ x ∈ Finset.range N, |trapezoidal_error f 1 (a + (↑x : ℝ) * h) (a + (↑(x + 1) : ℝ) * h)| ≤
    HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (↑(12 * HPow.hPow (β := ℕ) N 2) : ℝ)
have _₁ : (↑N : ℝ) * (ζ / 12 * HPow.hPow (β := ℕ) h 3) =
  HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (↑(12 * HPow.hPow (β := ℕ) N 2) : ℝ)
Tactic: calc
      _ ≤ ∑ k ∈ range N, ζ / 12 * h ^ 3 := sum_le_sum this
      _ = N * (ζ / 12 * h ^ 3)          := by simp [sum_const]
      _ = _                             := by push_cast; field
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
⊢ ∑ i ∈ Finset.range N, |trapezoidal_error f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h)| ≤
    HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have suffices : ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
Tactic: suffices ∀ k ∈ range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ (ζ / 12) * h ^ 3 by
    norm_cast
    calc
      _ ≤ ∑ k ∈ range N, ζ / 12 * h ^ 3 := sum_le_sum this
      _ = N * (ζ / 12 * h ^ 3)          := by simp [sum_const]
      _ = _                             := by push_cast; field
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
k : ℕ
hk : k ∈ Finset.range N
⊢ |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
have hk₁ : k < N
Tactic: rw [Finset.mem_range] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
k : ℕ
hk : k < N
⊢ a ≤ ak k
have simp : 0 ≤ (↑k : ℝ) * h
Tactic: simp only [ak, le_add_iff_nonneg_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
k : ℕ
hk : k < N
⊢ |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
have h1 : a ≤ ak k
Tactic: have h1 : a ≤ ak k := by simp only [ak, le_add_iff_nonneg_right]; positivity
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
⊢ ak (k + 1) ≤ b
have simp : a + (↑(k + 1) : ℝ) * h ≤ a + (↑N : ℝ) * h
Tactic: simp only [ak, hb]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
⊢ a + (↑(k + 1) : ℝ) * h ≤ a + (↑N : ℝ) * h
have h₁ : 0 ≤ h
Tactic: grw [Nat.lt_iff_add_one_le.mp hk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h₁ : 0 ≤ h
⊢ a + (↑(k + 1) : ℝ) * h ≤ a + (↑N : ℝ) * h
have grw : a + (↑N : ℝ) * h ≤ a + (↑N : ℝ) * h
Tactic: grw [Nat.lt_iff_add_one_le.mp hk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
⊢ |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
have h2 : ak (k + 1) ≤ b
Tactic: have h2 : ak (k + 1) ≤ b := by simp only [ak, hb]; grw [Nat.lt_iff_add_one_le.mp hk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
⊢ |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
have h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
Tactic: have h3 : Icc (ak k) (ak (k + 1)) ⊆ Icc a b := Icc_subset_Icc h1 h2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
⊢ ak k < ak (k + 1)
have rwa : 0 < ak (k + 1) - ak k
Tactic: rwa [← sub_pos, h0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
⊢ |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
have h4 : ak k < ak (k + 1)
Tactic: have h4 : ak k < ak (k + 1) := by rwa [← sub_pos, h0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
⊢ _root_.derivWithin f (Set.Icc a b) x = _root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))) x
have rw : _root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))) x = _root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))) x
Tactic: rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_df x (h3 hx))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
⊢ |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
have h5 : EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
  (Set.Icc (ak k) (ak (k + 1)))
Tactic: have h5 : EqOn (derivWithin f (Icc a b))
      (derivWithin f (Icc (ak k) (ak (k + 1)))) (Icc (ak k) (ak (k + 1))) := by
    intro x hx
    rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_df x (h3 hx))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
⊢ iteratedDerivWithin 2 f (Set.Icc a b) x = iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x
have simp : _root_.derivWithin (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b) x =
  _root_.derivWithin (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1)))) (Set.Icc (ak k) (ak (k + 1))) x
Tactic: simp only [iteratedDerivWithin_succ', iteratedDerivWithin_zero]