Derivatives of trigonometric expressions

The first and second derivatives of t ↦ cos (c t) are -c sin (c t) and -c² cos (c t) (TauCeti.deriv_cos_mul, TauCeti.deriv_deriv_cos_mul).

For every real exponent p, the map (k, θ) ↦ (1 - k² sin² θ) ^ p is smooth on the open set {(k, θ) | k ^ 2 < 1}, where its base is positive, and its partial derivative in k there is -2 p k sin² θ (1 - k² sin² θ) ^ (p - 1). The exponents p = -1/2 and p = 1/2 give the integrands of Legendre's elliptic integrals of the first and second kind.

theorem TauCeti.contDiffOn_one_sub_sq_mul_sin_sq_rpow {n : WithTop ℕ∞} (p : ℝ) : ContDiffOn ℝ n (fun (z : ℝ × ℝ) => (1 - z.1 ^ 2 * Real.sin z.2 ^ 2) ^ p) {z : ℝ × ℝ | z.1 ^ 2 < 1}

For every real exponent p, the map (k, θ) ↦ (1 - k² sin² θ) ^ p is smooth on {(k, θ) | k ^ 2 < 1}.

theorem TauCeti.deriv_cos_mul (c t : ℝ) : deriv (fun (s : ℝ) => Real.cos (c * s)) t = -(c * Real.sin (c * t))

The derivative of t ↦ cos (c t) is -c sin (c t).

theorem TauCeti.deriv_deriv_cos_mul (c t : ℝ) : deriv (deriv fun (s : ℝ) => Real.cos (c * s)) t = -(c ^ 2 * Real.cos (c * t))

The second derivative of t ↦ cos (c t) is -c² cos (c t).

theorem TauCeti.hasDerivAt_one_sub_sq_mul_sin_sq_rpow {k : ℝ} (hk : k ^ 2 < 1) (p θ : ℝ) : HasDerivAt (fun (k : ℝ) => (1 - k ^ 2 * Real.sin θ ^ 2) ^ p) (-(2 * p * k * Real.sin θ ^ 2 * (1 - k ^ 2 * Real.sin θ ^ 2) ^ (p - 1))) k

For k ^ 2 < 1 and every real exponent p, the derivative in k of (1 - k² sin² θ) ^ p is -2 p k sin² θ (1 - k² sin² θ) ^ (p - 1).