arctanOneThirdInterval

formal source

 119/-! ## §2. Constructive arctan(1/3) interval -/
 120
 121/-- Interval containing arctan(1/3) ≈ 0.32175 -/
 122def arctanOneThirdInterval : Interval where
 123  lo := 321 / 1000  -- 0.321
 124  hi := 322 / 1000  -- 0.322
 125  valid := by norm_num
 126
 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