# Derivatives of the tan and arctan functions. #

Continuity and derivatives of the tangent and arctangent functions.

theorem Real.hasDerivAt_tan {x : } (h : 0) :
theorem Real.tendsto_abs_tan_of_cos_eq_zero {x : } (hx : = 0) :
Filter.Tendsto (fun (x : ) => ||) (nhdsWithin x {x}) Filter.atTop
theorem Real.tendsto_abs_tan_atTop (k : ) :
Filter.Tendsto (fun (x : ) => ||) (nhdsWithin ((2 * k + 1) * Real.pi / 2) {(2 * k + 1) * Real.pi / 2}) Filter.atTop
@[simp]
theorem Real.deriv_tan (x : ) :
= 1 / ^ 2
@[simp]
theorem Real.contDiffAt_tan {n : ℕ∞} {x : } :
0
@[simp]
theorem Real.deriv_arctan :
= fun (x : ) => 1 / (1 + x ^ 2)

### 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.

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
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
theorem HasDerivWithinAt.arctan {f : } {f' : } {x : } {s : } (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : ) => Real.arctan (f x)) (1 / (1 + f x ^ 2) * f') s x
theorem derivWithin_arctan {f : } {x : } {s : } (hf : ) (hxs : ) :
derivWithin (fun (x : ) => Real.arctan (f x)) s x = 1 / (1 + f x ^ 2) * derivWithin f s x
@[simp]
theorem deriv_arctan {f : } {x : } (hc : ) :
deriv (fun (x : ) => Real.arctan (f x)) x = 1 / (1 + f x ^ 2) * deriv f x
theorem HasStrictFDerivAt.arctan {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : ) :
HasStrictFDerivAt (fun (x : E) => Real.arctan (f x)) ((1 / (1 + f x ^ 2)) f') x
theorem HasFDerivAt.arctan {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : HasFDerivAt f f' x) :
HasFDerivAt (fun (x : E) => Real.arctan (f x)) ((1 / (1 + f x ^ 2)) f') x
theorem HasFDerivWithinAt.arctan {E : Type u_1} [] {f : E} {f' : } {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
theorem fderivWithin_arctan {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) (hxs : ) :
fderivWithin (fun (x : E) => Real.arctan (f x)) s x = (1 / (1 + f x ^ 2))
@[simp]
theorem fderiv_arctan {E : Type u_1} [] {f : E} {x : E} (hc : ) :
fderiv (fun (x : E) => Real.arctan (f x)) x = (1 / (1 + f x ^ 2)) fderiv f x
theorem DifferentiableWithinAt.arctan {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) :
DifferentiableWithinAt (fun (x : E) => Real.arctan (f x)) s x
@[simp]
theorem DifferentiableAt.arctan {E : Type u_1} [] {f : E} {x : E} (hc : ) :
DifferentiableAt (fun (x : E) => Real.arctan (f x)) x
theorem DifferentiableOn.arctan {E : Type u_1} [] {f : E} {s : Set E} (hc : ) :
DifferentiableOn (fun (x : E) => Real.arctan (f x)) s
@[simp]
theorem Differentiable.arctan {E : Type u_1} [] {f : E} (hc : ) :
Differentiable fun (x : E) => Real.arctan (f x)
theorem ContDiffAt.arctan {E : Type u_1} [] {f : E} {x : E} {n : ℕ∞} (h : ContDiffAt n f x) :
ContDiffAt n (fun (x : E) => Real.arctan (f x)) x
theorem ContDiff.arctan {E : Type u_1} [] {f : E} {n : ℕ∞} (h : ) :
ContDiff n fun (x : E) => Real.arctan (f x)
theorem ContDiffWithinAt.arctan {E : Type u_1} [] {f : E} {x : E} {s : Set E} {n : ℕ∞} (h : ) :
ContDiffWithinAt n (fun (x : E) => Real.arctan (f x)) s x
theorem ContDiffOn.arctan {E : Type u_1} [] {f : E} {s : Set E} {n : ℕ∞} (h : ContDiffOn n f s) :
ContDiffOn n (fun (x : E) => Real.arctan (f x)) s