noncomputable def Section10CanonicalXi.xiSlope (s : ℝ) : ℝ

Equations

• Section10CanonicalXi.xiSlope s = s - (s - 1) / Section10CanonicalXi.xi s

theorem Section10CanonicalXi.xi_hasDerivAt {s : ℝ} (hs : 1 < s) : HasDerivAt xi (xiSlope s)⁻¹ s

theorem Section10CanonicalXi.xi_deriv {s : ℝ} (hs : 1 < s) : deriv xi s = (xiSlope s)⁻¹

theorem Section10CanonicalXi.xiSlope_hasDerivAt {s : ℝ} (hs : 1 < s) : HasDerivAt xiSlope (1 - 1 / xi s + (s - 1) * (xiSlope s)⁻¹ / xi s ^ 2) s

theorem Section10CanonicalXi.xiSlope_pos {s : ℝ} (hs : 1 < s) : 0 < xiSlope s

theorem Section10CanonicalXi.xi_hasDerivAt_deriv {s : ℝ} (hs : 1 < s) : HasDerivAt (deriv xi) (-(1 - 1 / xi s + (s - 1) * (xiSlope s)⁻¹ / xi s ^ 2) / xiSlope s ^ 2) s

Exact second implicit-derivative formula for the canonical inverse.

theorem Section10CanonicalXi.xi_twiceDifferentiableAt {s : ℝ} (hs : 1 < s) : DifferentiableAt ℝ (deriv xi) s

theorem Section10CanonicalXi.xi_secondDeriv {s : ℝ} (hs : 1 < s) : deriv (deriv xi) s = -(1 - 1 / xi s + (s - 1) * (xiSlope s)⁻¹ / xi s ^ 2) / xiSlope s ^ 2

theorem Section10CanonicalXi.xi_gt_one {s : ℝ} (hs : Real.exp 1 ≤ s) : 1 < xi s

theorem Section10CanonicalXi.log_lt_xi {s : ℝ} (hs : Real.exp 1 ≤ s) : Real.log s < xi s

theorem Section10CanonicalXi.two_le_log {s : ℝ} (hs : Real.exp 2 ≤ s) : 2 ≤ Real.log s

theorem Section10CanonicalXi.two_lt_xi {s : ℝ} (hs : Real.exp 2 ≤ s) : 2 < xi s

theorem Section10CanonicalXi.xiSlope_eq {s : ℝ} (hs : 1 < s) : xiSlope s = (s * (xi s - 1) + 1) / xi s

theorem Section10CanonicalXi.xi_deriv_sub_reciprocal_eq {s : ℝ} (hs : 1 < s) : deriv xi s - 1 / s = (s - 1) / (s * (s * (xi s - 1) + 1))

theorem Section10CanonicalXi.xi_deriv_asymptotic {s : ℝ} (hs : Real.exp 2 ≤ s) : |deriv xi s - 1 / s| ≤ 2 / (s * Real.log s)

Quantitative first-order asymptotic, with explicit threshold and constant.

theorem Section10CanonicalXi.xiSlope_ge_half {s : ℝ} (hs : Real.exp 2 ≤ s) : s / 2 ≤ xiSlope s

theorem Section10CanonicalXi.xi_deriv_nonneg {s : ℝ} (hs : 1 < s) : 0 ≤ deriv xi s

theorem Section10CanonicalXi.xi_deriv_le_two_div {s : ℝ} (hs : Real.exp 2 ≤ s) : deriv xi s ≤ 2 / s

noncomputable def Section10CanonicalXi.xiCurvatureFactor (s : ℝ) : ℝ

Equations

• Section10CanonicalXi.xiCurvatureFactor s = 1 - 1 / Section10CanonicalXi.xi s + (s - 1) * (Section10CanonicalXi.xiSlope s)⁻¹ / Section10CanonicalXi.xi s ^ 2

theorem Section10CanonicalXi.xiCurvatureFactor_nonneg {s : ℝ} (hs : Real.exp 2 ≤ s) : 0 ≤ xiCurvatureFactor s

theorem Section10CanonicalXi.xiCurvatureFactor_le_three_halves {s : ℝ} (hs : Real.exp 2 ≤ s) : xiCurvatureFactor s ≤ 3 / 2

theorem Section10CanonicalXi.xi_secondDeriv_asymptotic {s : ℝ} (hs : Real.exp 2 ≤ s) : |deriv (deriv xi) s| ≤ 6 / s ^ 2

Quantitative second-order asymptotic, with explicit threshold and constant.

theorem Section10CanonicalXi.xi_deriv_asymptotic_unitWindow {s t : ℝ} (hs : Real.exp 2 ≤ s) (ht : t ∈ Set.Icc s (s + 1)) : |deriv xi t - 1 / t| ≤ 2 / (s * Real.log s)

First-derivative estimate uniformly on the unit window [s,s+1].

theorem Section10CanonicalXi.xi_secondDeriv_asymptotic_unitWindow {s t : ℝ} (hs : Real.exp 2 ≤ s) (ht : t ∈ Set.Icc s (s + 1)) : |deriv (deriv xi) t| ≤ 6 / s ^ 2

Second-derivative estimate uniformly on the unit window [s,s+1].