Derivatives of the tan and arctan functions. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Continuity and derivatives of the tangent and arctangent functions.
theorem
real.has_strict_deriv_at_tan
{x : ℝ}
(h : real.cos x ≠ 0) :
has_strict_deriv_at real.tan (1 / real.cos x ^ 2) x
theorem
real.has_deriv_at_tan
{x : ℝ}
(h : real.cos x ≠ 0) :
has_deriv_at real.tan (1 / real.cos x ^ 2) x
theorem
real.tendsto_abs_tan_of_cos_eq_zero
{x : ℝ}
(hx : real.cos x = 0) :
filter.tendsto (λ (x : ℝ), |real.tan x|) (nhds_within x {x}ᶜ) filter.at_top
@[simp]
theorem
real.has_strict_deriv_at_arctan
(x : ℝ) :
has_strict_deriv_at real.arctan (1 / (1 + x ^ 2)) x
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
has_strict_deriv_at.arctan
{f : ℝ → ℝ}
{f' x : ℝ}
(hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ℝ), real.arctan (f x)) (1 / (1 + f x ^ 2) * f') x
theorem
has_deriv_at.arctan
{f : ℝ → ℝ}
{f' x : ℝ}
(hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ℝ), real.arctan (f x)) (1 / (1 + f x ^ 2) * f') x
theorem
has_deriv_within_at.arctan
{f : ℝ → ℝ}
{f' x : ℝ}
{s : set ℝ}
(hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ℝ), real.arctan (f x)) (1 / (1 + f x ^ 2) * f') s x
theorem
deriv_within_arctan
{f : ℝ → ℝ}
{x : ℝ}
{s : set ℝ}
(hf : differentiable_within_at ℝ f s x)
(hxs : unique_diff_within_at ℝ s x) :
deriv_within (λ (x : ℝ), real.arctan (f x)) s x = 1 / (1 + f x ^ 2) * deriv_within f s x
theorem
has_strict_fderiv_at.arctan
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
(hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), real.arctan (f x)) ((1 / (1 + f x ^ 2)) • f') x
theorem
has_fderiv_at.arctan
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
(hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), real.arctan (f x)) ((1 / (1 + f x ^ 2)) • f') x
theorem
has_fderiv_within_at.arctan
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
{s : set E}
(hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), real.arctan (f x)) ((1 / (1 + f x ^ 2)) • f') s x
theorem
fderiv_within_arctan
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℝ f s x)
(hxs : unique_diff_within_at ℝ s x) :
fderiv_within ℝ (λ (x : E), real.arctan (f x)) s x = (1 / (1 + f x ^ 2)) • fderiv_within ℝ f s x
@[simp]
theorem
fderiv_arctan
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
(hc : differentiable_at ℝ f x) :
theorem
differentiable_within_at.arctan
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℝ f s x) :
differentiable_within_at ℝ (λ (x : E), real.arctan (f x)) s x
@[simp]
theorem
differentiable_at.arctan
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
(hc : differentiable_at ℝ f x) :
differentiable_at ℝ (λ (x : E), real.arctan (f x)) x
theorem
differentiable_on.arctan
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
(hc : differentiable_on ℝ f s) :
differentiable_on ℝ (λ (x : E), real.arctan (f x)) s
@[simp]
theorem
differentiable.arctan
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
(hc : differentiable ℝ f) :
differentiable ℝ (λ (x : E), real.arctan (f x))
theorem
cont_diff_at.arctan
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{n : ℕ∞}
(h : cont_diff_at ℝ n f x) :
cont_diff_at ℝ n (λ (x : E), real.arctan (f x)) x
theorem
cont_diff.arctan
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{n : ℕ∞}
(h : cont_diff ℝ n f) :
cont_diff ℝ n (λ (x : E), real.arctan (f x))
theorem
cont_diff_within_at.arctan
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
{n : ℕ∞}
(h : cont_diff_within_at ℝ n f s x) :
cont_diff_within_at ℝ n (λ (x : E), real.arctan (f x)) s x
theorem
cont_diff_on.arctan
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
{n : ℕ∞}
(h : cont_diff_on ℝ n f s) :
cont_diff_on ℝ n (λ (x : E), real.arctan (f x)) s