arctan_two_eq
The identity arctan(2) equals pi over 4 plus arctan of 1/3 is obtained by splitting via the tangent addition formula after setting arctan(1) to pi/4. Numerics code that builds interval bounds for arctan cites this decomposition to reduce the argument to a known multiple of pi plus a smaller term. The tactic proof invokes Mathlib's arctan_add after checking the product condition, then closes with linear arithmetic.
claim$arctan 2 = pi/4 + arctan(1/3)$
background
The module supplies constructive interval bounds for arctan and tan via derivative comparisons. Upstream Interval structures from Numerics.Interval.Basic and Recognition.Certification define closed intervals with endpoints satisfying lo ≤ hi. The module documentation states that the arctan(2) identity is proved using Real.arctan_add from Mathlib, alongside polynomial bounds justified by monotoneOn_of_deriv_nonneg on [0, ∞).
proof idea
The tactic proof first rewrites arctan(1) to pi/4 using tan(pi/4) = 1 and arctan_tan. It then applies arctan_add to arctan(1) + arctan(1/3) after confirming the product is less than 1, normalizes, and finishes with linarith.
why it matters in Recognition Science
This feeds arctan_two_in_interval, which rewrites the equality and applies add_contains_add to place arctan(2) inside arctanTwoInterval. It supplies the exact splitting identity required by the trig module's constructive bounds, supporting the numerics layer that underpins Recognition Science interval computations.
scope and limits
- Does not derive the arctan addition formula.
- Does not produce numerical approximations or interval bounds.
- Does not extend the identity to other arguments.
- Does not address complex arctan or higher-dimensional cases.
Lean usage
rw [arctan_two_eq]formal statement (Lean)
151theorem arctan_two_eq : arctan 2 = Real.pi / 4 + arctan (1 / 3) := by
proof body
Tactic-mode proof.
152 have h1 : arctan 1 = Real.pi / 4 := by
153 rw [← tan_pi_div_four]
154 exact arctan_tan (by linarith [pi_pos]) (by linarith [pi_pos])
155 have hadd : arctan 1 + arctan (1 / 3) = arctan 2 := by
156 rw [arctan_add (by norm_num : (1 : ℝ) * (1 / 3) < 1)]
157 congr 1; norm_num
158 linarith
159
160/-- Interval containing arctan 2 = π/4 + arctan(1/3) -/