def
definition
arctanTwoInterval
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Numerics.Interval.Trig on GitHub at line 161.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
158 linarith
159
160/-- Interval containing arctan 2 = π/4 + arctan(1/3) -/
161def arctanTwoInterval : Interval :=
162 let pi4 := smulPos (1 / 4) piInterval (by norm_num)
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