Documentation

Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

Derivatives of the tan and arctan functions. #

Continuity and derivatives of the tangent and arctangent functions.

theorem Real.hasDerivAt_tan {x : } (h : Real.cos x 0) :
theorem Real.tendsto_abs_tan_of_cos_eq_zero {x : } (hx : Real.cos x = 0) :
Filter.Tendsto (fun x => |Real.tan x|) (nhdsWithin x {x}) Filter.atTop
theorem Real.tendsto_abs_tan_atTop (k : ) :
Filter.Tendsto (fun x => |Real.tan x|) (nhdsWithin ((2 * k + 1) * Real.pi / 2) {(2 * k + 1) * Real.pi / 2}) Filter.atTop
@[simp]
theorem Real.deriv_tan (x : ) :
deriv Real.tan x = 1 / Real.cos x ^ 2
theorem Real.hasDerivAt_arctan (x : ) :
HasDerivAt Real.arctan (1 / (1 + x ^ 2)) x
@[simp]
theorem Real.deriv_arctan :
deriv Real.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 : 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' : E →L[] } {x : E} (hf : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun x => 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' : E →L[] } {x : E} (hf : HasFDerivAt f f' x) :
HasFDerivAt (fun x => 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' : E →L[] } {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun x => 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 => 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 => 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) :
@[simp]
theorem DifferentiableAt.arctan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
DifferentiableAt (fun x => 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 => Real.arctan (f x)) s
@[simp]
theorem Differentiable.arctan {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} (hc : Differentiable f) :
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 => 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 => 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 => 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 => Real.arctan (f x)) s