Documentation

Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

Derivatives of the tan and arctan functions. #

Continuity and derivatives of the tangent and arctangent functions.

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 : ) :
@[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 : 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' : E →L[] } {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' : E →L[] } {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