`arctan_two_in_interval`

proved

show as: view math explainer →

module: IndisputableMonolith.Numerics.Interval.Trig
domain: Numerics
line: 166 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Numerics.Interval.Trig on GitHub at line 166.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 163  add pi4 arctanOneThirdInterval
 164
 165/-- **PROVED**: arctan(2) is in arctanTwoInterval. -/
 166theorem arctan_two_in_interval :
 167    arctanTwoInterval.contains (arctan 2) := by
 168  rw [arctan_two_eq]
 169  unfold arctanTwoInterval
 170  apply add_contains_add
 171  · -- π/4 is in (1/4) · piInterval
 172    have hpi := pi_in_piInterval
 173    have := smulPos_contains_smul (q := 1 / 4) (by norm_num : (0 : ℚ) < 1 / 4) hpi
 174    simp only [Rat.cast_div, Rat.cast_one, Rat.cast_ofNat] at this
 175    convert this using 1
 176    ring
 177  · exact arctan_one_third_in_interval
 178
 179end IndisputableMonolith.Numerics

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.