def G67Analytic.A : ℕ → ℝ → ℝ

The odd Taylor polynomial for twice the inverse hyperbolic tangent. The degree is a symbolic parameter; no degree search is involved.

Equations

• G67Analytic.A 0 x✝ = 0
• G67Analytic.A n.succ x✝ = G67Analytic.A n x✝ + 2 * x✝ ^ (2 * n + 1) / (2 * ↑n + 1)

def G67Analytic.B : ℕ → ℝ → ℝ

Its derivative, retained in recursive factored form.

Equations

• G67Analytic.B 0 x✝ = 0
• G67Analytic.B n.succ x✝ = G67Analytic.B n x✝ + 2 * x✝ ^ (2 * n)

theorem G67Analytic.A_zero (n : ℕ) : A n 0 = 0

theorem G67Analytic.A_nonneg (n : ℕ) {x : ℝ} (hx : 0 ≤ x) : 0 ≤ A n x

theorem G67Analytic.A_deriv (n : ℕ) (x : ℝ) : HasDerivAt (A n) (B n x) x

theorem G67Analytic.B_residual (n : ℕ) (x : ℝ) : (1 - x ^ 2) * B n x = 2 * (1 - x ^ (2 * n))

theorem G67Analytic.A_le_log_ratio (n : ℕ) {x : ℝ} (hx : 0 ≤ x) (hX : x < 1) : A n x ≤ Real.log (1 + x) - Real.log (1 - x)

The polynomial is below the logarithmic ratio throughout its analytic domain.

noncomputable def G67Analytic.logLower (n : ℕ) (z : ℝ) : ℝ

A log-free rational lower envelope, valid for every order.

Equations

• G67Analytic.logLower n z = G67Analytic.A n ((z - 1) / (z + 1))

theorem G67Analytic.logLower_nonneg (n : ℕ) {z : ℝ} (hz : 1 ≤ z) : 0 ≤ logLower n z

theorem G67Analytic.logLower_le_log (n : ℕ) {z : ℝ} (hz : 1 ≤ z) : logLower n z ≤ Real.log z

theorem G67Analytic.logLower_continuousOn (n : ℕ) : ContinuousOn (logLower n) (Set.Ici 1)

Polynomial-envelope continuity uses its certified derivative.

noncomputable def G67Analytic.profileLower (n : ℕ) (s : ℝ) : ℝ

The profile envelope preserves the full original logarithm.

Equations

• G67Analytic.profileLower n s = G67Analytic.logLower n ((1 / 2 - s - 4 / 53) / (4 / 53)) / (1 / 2 - s)

theorem G67Analytic.profileLower_le (n : ℕ) {s : ℝ} (hs : s ≤ 1 / 2 - 2 * (4 / 53)) : profileLower n s ≤ G67SumCoordinate.profile s