# The arctan function. #

Inequalities, identities and Real.tan as a PartialHomeomorph between (-(π / 2), π / 2) and the whole line.

The result of arctan x + arctan y is given by arctan_add, arctan_add_eq_add_pi or arctan_add_eq_sub_pi depending on whether x * y < 1 and 0 < x. As an application of arctan_add we give four Machin-like formulas (linear combinations of arctangents equal to π / 4 = arctan 1), including John Machin's original one at four_mul_arctan_inv_5_sub_arctan_inv_239.

theorem Real.tan_add {x : } {y : } (h : ((∀ (k : ), x (2 * k + 1) * Real.pi / 2) ∀ (l : ), y (2 * l + 1) * Real.pi / 2) (∃ (k : ), x = (2 * k + 1) * Real.pi / 2) ∃ (l : ), y = (2 * l + 1) * Real.pi / 2) :
Real.tan (x + y) = () / (1 - )
theorem Real.tan_add' {x : } {y : } (h : (∀ (k : ), x (2 * k + 1) * Real.pi / 2) ∀ (l : ), y (2 * l + 1) * Real.pi / 2) :
Real.tan (x + y) = () / (1 - )
theorem Real.tan_two_mul {x : } :
Real.tan (2 * x) = 2 * / (1 - ^ 2)
theorem Real.continuous_tan :
Continuous fun (x : {x : | 0}) => Real.tan x
theorem Real.image_tan_Ioo :
Real.tan '' Set.Ioo (-()) () = Set.univ
def Real.tanOrderIso :
(Set.Ioo (-()) ()) ≃o

Real.tan as an OrderIso between (-(π / 2), π / 2) and ℝ.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def Real.arctan (x : ) :

Inverse of the tan function, returns values in the range -π / 2 < arctan x and arctan x < π / 2

Equations
Instances For
@[simp]
theorem Real.tan_arctan (x : ) :
= x
theorem Real.arctan_mem_Ioo (x : ) :
Set.Ioo (-()) ()
@[simp]
theorem Real.range_arctan :
= Set.Ioo (-()) ()
theorem Real.arctan_tan {x : } (hx₁ : -() < x) (hx₂ : x < ) :
= x
theorem Real.cos_arctan_pos (x : ) :
0 <
theorem Real.cos_sq_arctan (x : ) :
^ 2 = 1 / (1 + x ^ 2)
theorem Real.sin_arctan (x : ) :
= x / (1 + x ^ 2)
theorem Real.cos_arctan (x : ) :
= 1 / (1 + x ^ 2)
theorem Real.arctan_eq_arcsin (x : ) :
= Real.arcsin (x / (1 + x ^ 2))
theorem Real.arcsin_eq_arctan {x : } (h : x Set.Ioo (-1) 1) :
= Real.arctan (x / (1 - x ^ 2))
@[simp]
theorem Real.arctan_zero :
= 0
@[simp]
theorem Real.arctan_eq_zero_iff {x : } :
= 0 x = 0
theorem Real.arctan_eq_of_tan_eq {x : } {y : } (h : = y) (hx : x Set.Ioo (-()) ()) :
= x
@[simp]
theorem Real.arctan_one :
=
@[simp]
theorem Real.arctan_neg (x : ) :
theorem Real.arctan_eq_arccos {x : } (h : 0 x) :
theorem Real.arccos_eq_arctan {x : } (h : 0 < x) :
= Real.arctan ((1 - x ^ 2) / x)
theorem Real.arctan_inv_of_pos {x : } (h : 0 < x) :
= -
theorem Real.arctan_inv_of_neg {x : } (h : x < 0) :
= -() -
theorem Real.arctan_ne_mul_pi_div_two {x : } (k : ) :
(2 * k + 1) * Real.pi / 2
theorem Real.arctan_add_arctan_lt_pi_div_two {x : } {y : } (h : x * y < 1) :
<
theorem Real.arctan_add {x : } {y : } (h : x * y < 1) :
= Real.arctan ((x + y) / (1 - x * y))
theorem Real.arctan_add_eq_add_pi {x : } {y : } (h : 1 < x * y) (hx : 0 < x) :
= Real.arctan ((x + y) / (1 - x * y)) + Real.pi
theorem Real.arctan_add_eq_sub_pi {x : } {y : } (h : 1 < x * y) (hx : x < 0) :
= Real.arctan ((x + y) / (1 - x * y)) - Real.pi
theorem Real.two_mul_arctan {x : } (h₁ : -1 < x) (h₂ : x < 1) :
2 * = Real.arctan (2 * x / (1 - x ^ 2))
theorem Real.two_mul_arctan_add_pi {x : } (h : 1 < x) :
2 * = Real.arctan (2 * x / (1 - x ^ 2)) + Real.pi
theorem Real.two_mul_arctan_sub_pi {x : } (h : x < -1) :
2 * = Real.arctan (2 * x / (1 - x ^ 2)) - Real.pi

John Machin's 1706 formula, which he used to compute π to 100 decimal places.

Real.tan as a PartialHomeomorph between (-(π / 2), π / 2) and the whole line.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]