arctan_one_third_in_interval

formal source

 127/-- **PROVED**: arctan(1/3) is in arctanOneThirdInterval.
 128    Lower bound from `h_lower(1/3) = 24628/76545 ≥ 321/1000`.
 129    Upper bound from `g_upper(1/3) = 391/1215 ≤ 322/1000`. -/
 130theorem arctan_one_third_in_interval :
 131    arctanOneThirdInterval.contains (arctan (1 / 3)) := by
 132  simp only [contains, arctanOneThirdInterval]
 133  constructor
 134  · -- lower: ↑(321/1000 : ℚ) ≤ arctan(1/3)
 135    have hlo := lower_poly_le_arctan (1 / 3) (by norm_num)
 136    have hval : h_lower (1 / 3) = 24628 / 76545 := by unfold h_lower; norm_num
 137    rw [hval] at hlo
 138    have hq : ((321 / 1000 : ℚ) : ℝ) ≤ (24628 : ℝ) / 76545 := by push_cast; norm_num
 139    linarith
 140  · -- upper: arctan(1/3) ≤ ↑(322/1000 : ℚ)
 141    have hhi := arctan_le_upper_poly (1 / 3) (by norm_num)
 142    have hval : g_upper (1 / 3) = 391 / 1215 := by unfold g_upper; norm_num
 143    rw [hval] at hhi
 144    have hq : (391 : ℝ) / 1215 ≤ ((322 / 1000 : ℚ) : ℝ) := by push_cast; norm_num
 145    linarith
 146
 147/-! ## §3. Constructive arctan(2) interval via addition formula -/
 148
 149/-- **PROVED**: `arctan(2) = π/4 + arctan(1/3)`.
 150    From the addition formula: `arctan(1) + arctan(1/3) = arctan(2)`. -/
 151theorem arctan_two_eq : arctan 2 = Real.pi / 4 + arctan (1 / 3) := by
 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) -/