Incremental derivatives

Differentiability and derivative formulas for the maps t ↦ f⁽ᵏ⁾(t · x) and their finite sums, used to differentiate the exponential factors in Niven's argument.

theorem differentiableAt_mul_const_ofReal (x : ℂ) (t : ℝ) : DifferentiableAt ℝ (fun (t : ℝ) => ↑t * x) t

Given x ∈ ℂ, the map t ↦ t * x is differentiable at t.

theorem deriv_mul_const_ofReal (x : ℂ) (t : ℝ) : deriv (fun (t : ℝ) => ↑t * x) t = x

d/dt (t * x) = x.

theorem differentiableAt_comp_mul_real (f : ℂ → ℂ) (x : ℂ) (t : ℝ) (hf : DifferentiableAt ℂ f (↑t * x)) : DifferentiableAt ℝ (fun (t : ℝ) => f (↑t * x)) t

If f is differentiable at t * x, then u ↦ f(u * x) is differentiable at t.

theorem differentiableAt_exp_neg_mul (x : ℂ) (t : ℝ) : DifferentiableAt ℝ (fun (t : ℝ) => Complex.exp (-(↑t * x))) t

For x ∈ ℂ, the map t ↦ e^(-(t * x)) is differentiable at t.

theorem continuousWithinAt_iteratedDeriv_comp_mul (f : ℂ → ℂ) (x : ℂ) (n : ℕ) (t : ℝ) (hderiv : DifferentiableAt ℂ (iteratedDeriv n f) (↑t * x)) : ContinuousWithinAt (fun (t : ℝ) => iteratedDeriv n f (↑t * x)) (Set.uIcc 0 1) t

If f^(n) is differentiable at t * x, then t ↦ f^(n)(t * x) is continuous on [0, 1] at t.

theorem differentiableAt_iteratedDeriv_comp_mul (f : ℂ → ℂ) (x : ℂ) (k : ℕ) (t : ℝ) (hderiv : DifferentiableAt ℂ (iteratedDeriv k f) (↑t * x)) : DifferentiableAt ℝ (fun (t : ℝ) => iteratedDeriv k f (↑t * x)) t

If f⁽ᵏ⁾ is differentiable at t * x, then t ↦ f⁽ᵏ⁾(t * x) is differentiable at t.

theorem deriv_iteratedDeriv_comp_mul (f : ℂ → ℂ) (x : ℂ) (k : ℕ) (t : ℝ) (hderiv : DifferentiableAt ℂ (iteratedDeriv k f) (↑t * x)) : deriv (fun (t : ℝ) => iteratedDeriv k f (↑t * x)) t = x * iteratedDeriv (k + 1) f (↑t * x)

If f⁽ⁱ⁾ is differentiable at t * x, then d/dt f⁽ᵏ⁾(t * x)) = x * f⁽ᵏ⁺¹⁾(t * x).

theorem differentiableAt_sum_iteratedDeriv (f : ℂ → ℂ) (x : ℂ) (n : ℕ) (t : ℝ) (hderiv : ∀ k ≤ n, DifferentiableAt ℂ (iteratedDeriv k f) (↑t * x)) : DifferentiableAt ℝ (fun (t : ℝ) => ∑ k ∈ Finset.range (n + 1), iteratedDeriv k f (↑t * x)) t

If f⁽ᵏ⁾ is differentiable at t * x for every k ≤ n, then t ↦ ∑ₖ₌₀ⁿ f⁽ᵏ⁾(t * x) is differentiable at t.

theorem sum_deriv_iteratedDeriv_comp_mul (f : ℂ → ℂ) (x : ℂ) (n : ℕ) (t : ℝ) (hderiv : ∀ k ≤ n, DifferentiableAt ℂ (iteratedDeriv k f) (↑t * x)) : deriv (fun (t : ℝ) => ∑ i ∈ Finset.range (n + 1), iteratedDeriv i f (↑t * x)) t = ∑ i ∈ Finset.range (n + 1), x * iteratedDeriv (i + 1) f (↑t * x)

If f⁽ᵏ⁾ is differentiable at t * x for every k ≤ n, then d/dt ∑ᵢ₌₀ⁿ f⁽ⁱ⁾(t * x)) = ∑ᵢ₌₀ⁿ x * f⁽ⁱ⁺¹⁾(t * x).