lower_poly_le_arctan
The inequality x − x³/3 + x⁵/5 − x⁷/7 ≤ arctan(x) holds for every real x ≥ 0. Numerics developers constructing rigorous enclosures for arctan(1/3) cite the result to anchor their lower estimate. The argument reduces the claim to nonnegativity of the difference function, establishes its monotonicity on [0, ∞) by verifying a nonnegative derivative via lower_le_inv_one_add_sq, and checks the zero value at the origin.
claim$x - x^3/3 + x^5/5 - x^7/7 ≤ arctan(x)$ for all real $x ≥ 0$.
background
The module supplies constructive interval bounds for arctan via derivative comparison. h_lower is the explicit polynomial x − x³/3 + x⁵/5 − x⁷/7 whose derivative equals 1 − t² + t⁴ − t⁶. Upstream results establish that h_lower is continuous and differentiable, together with the comparison lower_le_inv_one_add_sq that places this derivative below 1/(1 + t²). The local setting follows the module's use of monotoneOn_of_deriv_nonneg on the ray [0, ∞) to obtain all arctan bounds constructively.
proof idea
The proof reduces the target to nonnegativity of arctan x − h_lower x. It applies monotoneOn_of_deriv_nonneg on the convex set Ici 0 after confirming continuity of the difference and differentiability on the interior. The derivative comparison 1/(1 + t²) − (1 − t² + t⁴ − t⁶) ≥ 0 follows from lower_le_inv_one_add_sq. The difference vanishes at zero by direct evaluation, so monotonicity forces the inequality for all x ≥ 0.
why it matters in Recognition Science
This theorem supplies the lower half of the arctan interval bounds required by arctan_one_third_in_interval, which establishes that arctan(1/3) lies inside a rational interval. That enclosure is used to obtain a rigorous value for arctan(2) = π/4 + arctan(1/3) and therefore for π itself. Within the Recognition Science framework the result closes the lower-bound step of the eight-tick octave numerics that ultimately constrains the fine-structure constant inside (137.030, 137.039).
scope and limits
- Does not extend the inequality to negative arguments.
- Does not supply matching upper bounds.
- Does not address convergence of the infinite arctan series.
- Does not treat complex-valued arctan.
Lean usage
have hlo := lower_poly_le_arctan (1 / 3) (by norm_num)formal statement (Lean)
102theorem lower_poly_le_arctan (x : ℝ) (hx : 0 ≤ x) : h_lower x ≤ arctan x := by
proof body
Term-mode proof.
103 suffices h : 0 ≤ arctan x - h_lower x by linarith
104 have hkey : MonotoneOn (fun t => arctan t - h_lower t) (Set.Ici 0) :=
105 monotoneOn_of_deriv_nonneg (convex_Ici 0)
106 ((continuous_arctan.sub h_lower_continuous).continuousOn)
107 (fun t _ => ((hasDerivAt_arctan t).differentiableAt.sub
108 (h_lower_differentiable t)).differentiableWithinAt)
109 (fun t ht => by
110 simp only [Set.nonempty_Iio, interior_Ici'] at ht
111 have hd : HasDerivAt (fun s => arctan s - h_lower s)
112 (1/(1+t^2) - (1 - t^2 + t^4 - t^6)) t :=
113 (hasDerivAt_arctan t).sub (h_lower_deriv t)
114 rw [hd.deriv]
115 linarith [lower_le_inv_one_add_sq t])
116 linarith [hkey (Set.mem_Ici.mpr (le_refl 0)) (Set.mem_Ici.mpr hx) hx,
117 show arctan 0 - h_lower 0 = 0 by simp [h_lower, arctan_zero]]
118
119/-! ## §2. Constructive arctan(1/3) interval -/
120
121/-- Interval containing arctan(1/3) ≈ 0.32175 -/