# Derivatives of the `tan` and `arctan` functions. #

Continuity and derivatives of the tangent and arctangent functions.

source
theorem Real.hasStrictDerivAt_tan {x : ℝ} (h : cos x ≠ 0) :
HasStrictDerivAt tan (1 / cos x ^ 2) x
source
theorem Real.hasDerivAt_tan {x : ℝ} (h : cos x ≠ 0) :
HasDerivAt tan (1 / cos x ^ 2) x
source
theorem Real.tendsto_abs_tan_of_cos_eq_zero {x : ℝ} (hx : cos x = 0) :
Filter.Tendsto (fun (x : ℝ) => |tan x|) (nhdsWithin x {x}ᶜ) Filter.atTop
source
theorem Real.tendsto_abs_tan_atTop (k : ℤ) :
Filter.Tendsto (fun (x : ℝ) => |tan x|) (nhdsWithin ((2 * ↑k + 1) * Real.pi / 2) {(2 * ↑k + 1) * Real.pi / 2}ᶜ) Filter.atTop
source
theorem Real.continuousAt_tan {x : ℝ} :
ContinuousAt tan x ↔ cos x ≠ 0
source
theorem Real.differentiableAt_tan {x : ℝ} :
DifferentiableAt ℝ tan x ↔ cos x ≠ 0
source
@[simp]
theorem Real.deriv_tan (x : ℝ) :
deriv tan x = 1 / cos x ^ 2
source
@[simp]
theorem Real.contDiffAt_tan {n : WithTop ℕ∞} {x : ℝ} :
ContDiffAt ℝ n tan x ↔ cos x ≠ 0
source
theorem Real.hasDerivAt_tan_of_mem_Ioo {x : ℝ} (h : x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) :
HasDerivAt tan (1 / cos x ^ 2) x
source
theorem Real.differentiableAt_tan_of_mem_Ioo {x : ℝ} (h : x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) :
DifferentiableAt ℝ tan x
source
theorem Real.hasStrictDerivAt_arctan (x : ℝ) :
HasStrictDerivAt arctan (1 / (1 + x ^ 2)) x
source
theorem Real.hasDerivAt_arctan (x : ℝ) :
HasDerivAt arctan (1 / (1 + x ^ 2)) x
source
theorem Real.hasDerivAt_arctan' (x : ℝ) :
HasDerivAt arctan (1 + x ^ 2)⁻¹ x
source
theorem Real.differentiableAt_arctan (x : ℝ) :
DifferentiableAt ℝ arctan x
source
theorem Real.differentiable_arctan :
Differentiable ℝ arctan
source
@[simp]
theorem Real.deriv_arctan :
deriv arctan = fun (x : ℝ) => 1 / (1 + x ^ 2)
source
theorem Real.contDiff_arctan {n : WithTop ℕ∞} :
ContDiff ℝ n arctan

### Lemmas for derivatives of the composition of `Real.arctan` with a differentiable function #

In this section we register lemmas for the derivatives of the composition of `Real.arctan` with a differentiable function, for standalone use and use with `simp`.

source
theorem HasStrictDerivAt.arctan {f : ℝ → ℝ} {f' x : ℝ} (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ℝ) => Real.arctan (f x)) (1 / (1 + f x ^ 2) * f') x
source
theorem HasDerivAt.arctan {f : ℝ → ℝ} {f' x : ℝ} (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ℝ) => Real.arctan (f x)) (1 / (1 + f x ^ 2) * f') x
source
theorem HasDerivWithinAt.arctan {f : ℝ → ℝ} {f' x : ℝ} {s : Set ℝ} (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : ℝ) => Real.arctan (f x)) (1 / (1 + f x ^ 2) * f') s x
source
theorem derivWithin_arctan {f : ℝ → ℝ} {x : ℝ} {s : Set ℝ} (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
derivWithin (fun (x : ℝ) => Real.arctan (f x)) s x = 1 / (1 + f x ^ 2) * derivWithin f s x
source
@[simp]
theorem deriv_arctan {f : ℝ → ℝ} {x : ℝ} (hc : DifferentiableAt ℝ f x) :
deriv (fun (x : ℝ) => Real.arctan (f x)) x = 1 / (1 + f x ^ 2) * deriv f x
source
theorem HasStrictFDerivAt.arctan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E} (hf : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun (x : E) => Real.arctan (f x)) ((1 / (1 + f x ^ 2)) • f') x
source
theorem HasFDerivAt.arctan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E} (hf : HasFDerivAt f f' x) :
HasFDerivAt (fun (x : E) => Real.arctan (f x)) ((1 / (1 + f x ^ 2)) • f') x
source
theorem HasFDerivWithinAt.arctan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun (x : E) => Real.arctan (f x)) ((1 / (1 + f x ^ 2)) • f') s x
source
theorem fderivWithin_arctan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
fderivWithin ℝ (fun (x : E) => Real.arctan (f x)) s x = (1 / (1 + f x ^ 2)) • fderivWithin ℝ f s x
source
@[simp]
theorem fderiv_arctan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hc : DifferentiableAt ℝ f x) :
fderiv ℝ (fun (x : E) => Real.arctan (f x)) x = (1 / (1 + f x ^ 2)) • fderiv ℝ f x
source
theorem DifferentiableWithinAt.arctan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} (hf : DifferentiableWithinAt ℝ f s x) :
DifferentiableWithinAt ℝ (fun (x : E) => Real.arctan (f x)) s x
source
@[simp]
theorem DifferentiableAt.arctan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hc : DifferentiableAt ℝ f x) :
DifferentiableAt ℝ (fun (x : E) => Real.arctan (f x)) x
source
theorem DifferentiableOn.arctan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} (hc : DifferentiableOn ℝ f s) :
DifferentiableOn ℝ (fun (x : E) => Real.arctan (f x)) s
source
@[simp]
theorem Differentiable.arctan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hc : Differentiable ℝ f) :
Differentiable ℝ fun (x : E) => Real.arctan (f x)
source
theorem ContDiffAt.arctan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {n : ℕ∞} (h : ContDiffAt ℝ (↑n) f x) :
ContDiffAt ℝ (↑n) (fun (x : E) => Real.arctan (f x)) x
source
theorem ContDiff.arctan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {n : ℕ∞} (h : ContDiff ℝ (↑n) f) :
ContDiff ℝ ↑n fun (x : E) => Real.arctan (f x)
source
theorem ContDiffWithinAt.arctan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} {n : ℕ∞} (h : ContDiffWithinAt ℝ (↑n) f s x) :
ContDiffWithinAt ℝ (↑n) (fun (x : E) => Real.arctan (f x)) s x
source
theorem ContDiffOn.arctan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {n : ℕ∞} (h : ContDiffOn ℝ (↑n) f s) :
ContDiffOn ℝ (↑n) (fun (x : E) => Real.arctan (f x)) s