Derivatives of the tan and arctan functions.

Continuity and derivatives of the tangent and arctangent functions.

theorem Real.hasStrictDerivAt_tan {x : ℝ} (h : cos x ≠ 0) : HasStrictDerivAt tan (1 / cos x ^ 2) x

theorem Real.hasDerivAt_tan {x : ℝ} (h : cos x ≠ 0) : HasDerivAt tan (1 / cos x ^ 2) x

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

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

theorem Real.continuousAt_tan {x : ℝ} : ContinuousAt tan x ↔ cos x ≠ 0

theorem Real.differentiableAt_tan {x : ℝ} : DifferentiableAt ℝ tan x ↔ cos x ≠ 0

@[simp]

theorem Real.deriv_tan (x : ℝ) : deriv tan x = 1 / cos x ^ 2

@[simp]

theorem Real.contDiffAt_tan {n : WithTop ℕ∞} {x : ℝ} : ContDiffAt ℝ n tan x ↔ cos x ≠ 0

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

theorem Real.differentiableAt_tan_of_mem_Ioo {x : ℝ} (h : x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) : DifferentiableAt ℝ tan x

theorem Real.tendsto_tan_div_nhdsNE_zero : Filter.Tendsto (fun (x : ℝ) => tan x / x) (nhdsWithin 0 {0}ᶜ) (nhds 1)

The limit lim_{x → 0} (tan x) / x = 1.

theorem Real.hasStrictDerivAt_arctan (x : ℝ) : HasStrictDerivAt arctan (1 / (1 + x ^ 2)) x

theorem Real.hasDerivAt_arctan (x : ℝ) : HasDerivAt arctan (1 / (1 + x ^ 2)) x

theorem Real.hasDerivAt_arctan' (x : ℝ) : HasDerivAt arctan (1 + x ^ 2)⁻¹ x

theorem Real.differentiableAt_arctan (x : ℝ) : DifferentiableAt ℝ arctan x

theorem Real.differentiable_arctan : Differentiable ℝ arctan

@[simp]

theorem Real.deriv_arctan : deriv arctan = fun (x : ℝ) => 1 / (1 + x ^ 2)

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.

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 : Set ℝ} (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 : 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

@[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

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

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

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

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

@[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

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

@[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

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

@[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)

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

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)

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

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