LeanChemicalTheories / math.deriv

theorem deriv_within_div_pow {C x : ℝ} (hx : x ≠ 0) (s : set ℝ) (hu : unique_diff_within_at ℝ s x) (n : ℕ) :

1 < n → deriv_within (λ (y : ℝ), C / y ^ n) s x = -↑n * C / x ^ (n + 1)

theorem has_deriv_at_div_pow {C x : ℝ} (hx : x ≠ 0) (n : ℕ) :

1 < n → has_deriv_at (λ (y : ℝ), C / y ^ n) (-↑n * C / x ^ (n + 1)) x

theorem differentiable_at_div_pow {C x : ℝ} (hx : x ≠ 0) (n : ℕ) :

theorem deriv_div_pow {C x : ℝ} (hx : x ≠ 0) (n : ℕ) :

1 < n → deriv (λ (y : ℝ), C / y ^ n) x = -↑n * C / x ^ (n + 1)

theorem deriv_inv_rpow {C z : ℝ} (hz : 0 < z) (r : ℝ) :

1 ≤ r → deriv (λ (x : ℝ), C / x ^ r) z = -r * C / z ^ (r + 1)

theorem differentiable_at_inv_rpow {C z : ℝ} (hz : 0 < z) (r : ℝ) :

1 ≤ r → differentiable_at ℝ (λ (x : ℝ), C / x ^ r) z

theorem deriv_abs_of_nonneg_rpow {z : ℝ} (hpos : ∀ (x : ℝ), 0 ≤ x) (r : ℝ) :

1 ≤ r → deriv (λ (x : ℝ), |x ^ r|) z = r * z ^ (r - 1)

theorem deriv_inv_abs_rpow {C z : ℝ} (hz : 0 < z) (hC : 0 < C) (hpos : ∀ (x : ℝ), 0 < x) (r : ℝ) :

1 ≤ r → deriv (λ (x : ℝ), |C| / |x ^ r|) z = -r * C / z ^ (r + 1)

theorem differentiable_at_inv_abs_rpow {C z : ℝ} (hz : 0 < z) (hC : 0 < C) (hpos : ∀ (x : ℝ), 0 < x) (r : ℝ) :

1 ≤ r → differentiable_at ℝ (λ (x : ℝ), |C| / |x ^ r|) z