awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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| ≤ ζ
rw : |trapezoidal_error f 1 a b| ≤ ζ / 12 * HPow.hPow (β := ℕ) (b - a) 3
⊢ |trapezoidal_error f 1 a b| ≤ HPow.hPow (β := ℕ) (b - a) 3 * ζ / 12

Tactic:
rw [mul_div_assoc, mul_comm]

Premises used: mul_div_assoc, mul_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hy : y ∈ Set.Icc a b
unfold :
  HasDerivWithinAt
    (fun (t : ℝ) ↦
      (t - a) / (↑1 : ℝ) *
          ((f a + f t) / 2 +
            ∑ k ∈ Finset.range (HSub.hSub (α := ℕ) 1 1), f (a + HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (t - a) / (↑1 : ℝ))) -
        ∫ (x : ℝ) in a..t, f x)
    (dg y) (Set.Icc a b) y
⊢ HasDerivWithinAt g (dg y) (Set.Icc a b) y

Tactic:
unfold g trapezoidal_error trapezoidal_integral

Premises used: trapezoidal_integral, trapezoidal_error
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hy : y ∈ Set.Icc a b
simp : HasDerivWithinAt (fun (t : ℝ) ↦ (t - a) * ((f a + f t) / 2) - ∫ (x : ℝ) in a..t, f x) (dg y) (Set.Icc a b) y
⊢ HasDerivWithinAt
    (fun (t : ℝ) ↦
      (t - a) / (↑1 : ℝ) *
          ((f a + f t) / 2 +
            ∑ k ∈ Finset.range (HSub.hSub (α := ℕ) 1 1), f (a + HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (t - a) / (↑1 : ℝ))) -
        ∫ (x : ℝ) in a..t, f x)
    (dg y) (Set.Icc a b) y

Tactic:
simp only [Nat.cast_one, div_one, tsub_self, Finset.range_zero, sum_empty, add_zero]

Premises used: tsub_self, Finset.sum_empty, add_zero, div_one, Nat.cast_one, Finset.range_zero
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hy : y ∈ Set.Icc a b
simp_rw : HasDerivWithinAt (fun (t : ℝ) ↦ (t - a) / 2 * (f a + f t) - ∫ (x : ℝ) in a..t, f x) (dg y) (Set.Icc a b) y
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ (t - a) * ((f a + f t) / 2) - ∫ (x : ℝ) in a..t, f x) (dg y) (Set.Icc a b) y

Tactic:
simp_rw [← mul_comm_div]

Premises used: mul_comm_div
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hy : y ∈ Set.Icc a b
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ (t - a) / 2 * (f a + f t) - ∫ (x : ℝ) in a..t, f x) (dg y) (Set.Icc a b) y

Tactic:
fun_sub (fun_mul (div_const (sub_const _ (hasDerivWithinAt_id _ _)) _)
      (const_add _ (h_df y hy).hasDerivWithinAt)) ?_

Premises used: HasDerivWithinAt.div_const, HasDerivWithinAt.const_add, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.fun_mul, HasDerivWithinAt.fun_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hy : y ∈ Set.Icc a b
refine : HasDerivWithinAt (fun (t : ℝ) ↦ ∫ (x : ℝ) in a..t, f x) (f y) (Set.Icc a b) y
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ (t - a) / 2 * (f a + f t) - ∫ (x : ℝ) in a..t, f x) (dg y) (Set.Icc a b) y

Tactic:
refine fun_sub (fun_mul (div_const (sub_const _ (hasDerivWithinAt_id _ _)) _)
      (const_add _ (h_df y hy).hasDerivWithinAt)) ?_

Premises used: HasDerivWithinAt.div_const, HasDerivWithinAt.const_add, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.fun_mul, HasDerivWithinAt.fun_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hy : y ∈ Set.Icc a b
⊢ Fact (y ∈ Set.Icc a b)

Tactic:
have := Fact.mk hy
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hy : y ∈ Set.Icc a b
this : Fact (y ∈ Set.Icc a b)
hf : IntervalIntegrable f volume a y
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (nhdsWithin y (Set.Icc a b)) volume
hb : ContinuousWithinAt f (Set.Icc a b) y
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ ∫ (x : ℝ) in a..t, f x) (f y) (Set.Icc a b) y

Tactic:
apply integral_hasDerivWithinAt_right

Premises used: intervalIntegral.integral_hasDerivWithinAt_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hy : y ∈ Set.Icc a b
this : Fact (y ∈ Set.Icc a b)
⊢ IntervalIntegrable f volume a y

Tactic:
(h_df.continuousOn.mono (Icc_subset_Icc le_rfl hy.2)).intervalIntegrable_of_Icc hy.1

Premises used: le_rfl, DifferentiableOn.continuousOn, ContinuousOn.intervalIntegrable_of_Icc, And.right, And.left, Set.Icc_subset_Icc, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hy : y ∈ Set.Icc a b
this : Fact (y ∈ Set.Icc a b)
⊢ IntervalIntegrable f volume a y

Tactic:
exact (h_df.continuousOn.mono (Icc_subset_Icc le_rfl hy.2)).intervalIntegrable_of_Icc hy.1

Premises used: le_rfl, DifferentiableOn.continuousOn, ContinuousOn.intervalIntegrable_of_Icc, And.right, And.left, Set.Icc_subset_Icc, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hy : y ∈ Set.Icc a b
this : Fact (y ∈ Set.Icc a b)
⊢ StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (nhdsWithin y (Set.Icc a b)) volume

Tactic:
h_df.continuousOn.stronglyMeasurableAtFilter_nhdsWithin measurableSet_Icc y

Premises used: DifferentiableOn.continuousOn, measurableSet_Icc, ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hy : y ∈ Set.Icc a b
this : Fact (y ∈ Set.Icc a b)
⊢ StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (nhdsWithin y (Set.Icc a b)) volume

Tactic:
exact h_df.continuousOn.stronglyMeasurableAtFilter_nhdsWithin measurableSet_Icc y

Premises used: DifferentiableOn.continuousOn, measurableSet_Icc, ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hy : y ∈ Set.Icc a b
this : Fact (y ∈ Set.Icc a b)
⊢ ContinuousWithinAt f (Set.Icc a b) y

Tactic:
h_df.continuousOn.continuousWithinAt hy

Premises used: DifferentiableOn.continuousOn, ContinuousOn.continuousWithinAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hy : y ∈ Set.Icc a b
this : Fact (y ∈ Set.Icc a b)
⊢ ContinuousWithinAt f (Set.Icc a b) y

Tactic:
exact h_df.continuousOn.continuousWithinAt hy

Premises used: DifferentiableOn.continuousOn, ContinuousOn.continuousWithinAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
⊢ ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y

Tactic:
have h_dg (y : ℝ) (hy : y ∈ Icc a b) : HasDerivWithinAt g (dg y) (Icc a b) y := by
    unfold g trapezoidal_error trapezoidal_integral
    simp only [Nat.cast_one, div_one, tsub_self, Finset.range_zero, sum_empty, add_zero]
    simp_rw [← mul_comm_div]
    refine fun_sub (fun_mul (div_const (sub_const _ (hasDerivWithinAt_id _ _)) _)
      (const_add _ (h_df y hy).hasDerivWithinAt)) ?_
    have := Fact.mk hy -- Needed for integral_hasDerivWithinAt_right
    apply integral_hasDerivWithinAt_right
    · exact (h_df.continuousOn.mono (Icc_subset_Icc le_rfl hy.2)).intervalIntegrable_of_Icc hy.1
    · exact h_df.continuousOn.stronglyMeasurableAtFilter_nhdsWithin measurableSet_Icc y
    · exact h_df.continuousOn.continuousWithinAt hy
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hx : y ∈ Set.Icc a b
dfaky : ℝ := _root_.derivWithin f (Set.Icc a b) y
⊢ ddg y = 1 / 2 * dfaky + (1 / 2 * dfaky + ddg y) - dfaky

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hx : y ∈ Set.Icc a b
dfaky : ℝ := _root_.derivWithin f (Set.Icc a b) y
rw : HasDerivWithinAt dg (1 / 2 * dfaky + (1 / 2 * dfaky + ddg y) - dfaky) (Set.Icc a b) y
⊢ HasDerivWithinAt dg (ddg y) (Set.Icc a b) y

Tactic:
rw [(by ring : ddg y = (1 / 2) * dfaky + ((1 / 2) * dfaky + ddg y) - dfaky)]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hx : y ∈ Set.Icc a b
dfaky : ℝ := _root_.derivWithin f (Set.Icc a b) y
⊢ HasDerivWithinAt dg (1 / 2 * dfaky + (1 / 2 * dfaky + ddg y) - dfaky) (Set.Icc a b) y

Tactic:
fun_sub (fun_add (const_mul _ (const_add _ (h_df y hx).hasDerivWithinAt))
      (fun_mul (div_const (sub_const _ (hasDerivWithinAt_id _ _)) _) ?_))
      (h_df y hx).hasDerivWithinAt

Premises used: HasDerivWithinAt.div_const, HasDerivWithinAt.const_add, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.const_mul, HasDerivWithinAt.fun_mul, HasDerivWithinAt.fun_sub, HasDerivWithinAt.fun_add
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hx : y ∈ Set.Icc a b
dfaky : ℝ := _root_.derivWithin f (Set.Icc a b) y
refine : HasDerivWithinAt (_root_.derivWithin f (Set.Icc a b)) (iteratedDerivWithin 2 f (Set.Icc a b) y) (Set.Icc a b) y
⊢ HasDerivWithinAt dg (1 / 2 * dfaky + (1 / 2 * dfaky + ddg y) - dfaky) (Set.Icc a b) y

Tactic:
refine fun_sub (fun_add (const_mul _ (const_add _ (h_df y hx).hasDerivWithinAt))
      (fun_mul (div_const (sub_const _ (hasDerivWithinAt_id _ _)) _) ?_))
      (h_df y hx).hasDerivWithinAt

Premises used: HasDerivWithinAt.div_const, HasDerivWithinAt.const_add, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.const_mul, HasDerivWithinAt.fun_mul, HasDerivWithinAt.fun_sub, HasDerivWithinAt.fun_add
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hx : y ∈ Set.Icc a b
dfaky : ℝ := _root_.derivWithin f (Set.Icc a b) y
rw :
  HasDerivWithinAt (_root_.derivWithin f (Set.Icc a b)) ((fun (g : ℝ → ℝ) ↦ _root_.derivWithin g (Set.Icc a b))^[2] f y)
    (Set.Icc a b) y
⊢ HasDerivWithinAt (_root_.derivWithin f (Set.Icc a b)) (iteratedDerivWithin 2 f (Set.Icc a b) y) (Set.Icc a b) y

Tactic:
rw [iteratedDerivWithin_eq_iterate]

Premises used: iteratedDerivWithin_eq_iterate
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hx : y ∈ Set.Icc a b
dfaky : ℝ := _root_.derivWithin f (Set.Icc a b) y
⊢ HasDerivWithinAt (_root_.derivWithin f (Set.Icc a b)) ((fun (g : ℝ → ℝ) ↦ _root_.derivWithin g (Set.Icc a b))^[2] f y)
    (Set.Icc a b) y

Tactic:
(h_ddf y hx).hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, Nat.iterate, derivWithin
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
y : ℝ
hx : y ∈ Set.Icc a b
dfaky : ℝ := _root_.derivWithin f (Set.Icc a b) y
⊢ HasDerivWithinAt (_root_.derivWithin f (Set.Icc a b)) ((fun (g : ℝ → ℝ) ↦ _root_.derivWithin g (Set.Icc a b))^[2] f y)
    (Set.Icc a b) y

Tactic:
exact (h_ddf y hx).hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
⊢ ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y

Tactic:
have h_ddg (y : ℝ) (hx : y ∈ Icc a b) : HasDerivWithinAt dg (ddg y) (Icc a b) y := by
    -- The eventual expression for g'' has several terms that cancel, which we have to undo here
    -- so that the various HasDerivWithinAt theorems will have everything they need.
    let dfaky := derivWithin f (Icc a b) y
    rw [(by ring : ddg y = (1 / 2) * dfaky + ((1 / 2) * dfaky + ddg y) - dfaky)]
    refine fun_sub (fun_add (const_mul _ (const_add _ (h_df y hx).hasDerivWithinAt))
      (fun_mul (div_const (sub_const _ (hasDerivWithinAt_id _ _)) _) ?_))
      (h_df y hx).hasDerivWithinAt
    rw [iteratedDerivWithin_eq_iterate]
    exact (h_ddf y hx).hasDerivWithinAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
x : ℝ
hx : x ∈ Set.Icc a b
simp_rw : |x - a| / 2 * |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ / 2 * (x - a)
⊢ |ddg x| ≤ ζ / 2 * HPow.hPow (β := ℕ) (x - a) 1

Tactic:
simp_rw [pow_one, ddg, abs_mul, abs_div, abs_two]

Premises used: abs_mul, abs_div, pow_one, abs_two