The κ = b = 1 common-majorant slope used in Lemma 10.28

The source defines ξ as the inverse of η(x) = (exp x - 1) / x. The weak interface below is exactly at Proposition 10.20(ii): it records the explicit inverse equation, differentiability, and the source lower bound for η'. It contains no DDE solution, no weighted monotonicity, and no unit-shift ratio.

The file proves from that interface:

• the inverse-derivative formula of Proposition 10.20(ii);
• a uniform one-sided secant bound on every unit interval (κ = 1);
• the FTC derivative of the phase ∫ ξ (10.43);
• the normalized logarithmic derivative identity (10.44), with the audited correction ξ(s / b) (hence ξ s when b = 1).

structure Section10Lemma1028.Proposition1020Xi (ξ : ℝ → ℝ) : Prop

Weak, source-faithful Proposition 10.20(ii) interface for ξ on (1,∞). The field etaSlopeLower is the displayed strict > 1/2 estimate in the proposition; it is not a Lemma 10.28 conclusion.

• continuous : Continuous ξ
• positive (s : ℝ) : 1 < s → 0 < ξ s
• equation (s : ℝ) : 1 < s → Real.exp (ξ s) - 1 = s * ξ s
• differentiableAt (s : ℝ) : 1 < s → DifferentiableAt ℝ ξ s
• etaSlopeLower (s : ℝ) : 1 < s → 1 / 2 < s - (s - 1) / ξ s

theorem Section10Lemma1028.Proposition1020Xi.hasDerivAt {ξ : ℝ → ℝ} (hξ : Proposition1020Xi ξ) {s : ℝ} (hs : 1 < s) : HasDerivAt ξ (1 / (s - (s - 1) / ξ s)) s

Proposition 10.20(ii)'s inverse derivative formula, derived by differentiating the explicit equation exp (ξ s) - 1 = s ξ(s).

theorem Section10Lemma1028.Proposition1020Xi.deriv_pos {ξ : ℝ → ℝ} (hξ : Proposition1020Xi ξ) {s : ℝ} (hs : 1 < s) : 0 < deriv ξ s

The Proposition 10.20 derivative is positive.

theorem Section10Lemma1028.Proposition1020Xi.deriv_le_two {ξ : ℝ → ℝ} (hξ : Proposition1020Xi ξ) {s : ℝ} (hs : 1 < s) : deriv ξ s ≤ 2

The common derivative majorant 2 supplied by the strict η' > 1/2 bound in Proposition 10.20(ii).

theorem Section10Lemma1028.proposition1020_oneSidedCommonMajorantSlope {ξ : ℝ → ℝ} (hξ : Proposition1020Xi ξ) {t s : ℝ} (ht : 2 ≤ t) (hts : t ≤ s) : ξ s - ξ t ≤ 2 * (s - t)

One-sided common-majorant slope for ξ (the κ = 1 specialization). Unlike a unit-shift ratio for a DDE solution, this is a Proposition 10.20 calculus fact: every secant on [2,∞) has slope at most 2.

theorem Section10Lemma1028.proposition1020_secant_nonneg {ξ : ℝ → ℝ} (hξ : Proposition1020Xi ξ) {t s : ℝ} (ht : 2 ≤ t) (hts : t ≤ s) : 0 ≤ ξ s - ξ t

The matching lower secant bound; together with the previous theorem this is the controlled first-order input used by the Taylor steps in §10.

theorem Section10Lemma1028.proposition1020_unitIntervalError {ξ : ℝ → ℝ} (hξ : Proposition1020Xi ξ) {t s : ℝ} (hs : 3 ≤ s) (ht : t ∈ Set.Icc (s - 1) s) : |ξ t - ξ s| ≤ 2

Uniform unit-interval form of the common majorant.

noncomputable def Section10Lemma1028.xiPhase (ξ : ℝ → ℝ) (s : ℝ) : ℝ

The κ = 1 phase from (10.43).

Equations

• Section10Lemma1028.xiPhase ξ s = ∫ (t : ℝ) in 1..s, ξ t

theorem Section10Lemma1028.xiPhase_hasDerivAt {ξ : ℝ → ℝ} (hξ : Proposition1020Xi ξ) (s : ℝ) : HasDerivAt (xiPhase ξ) (ξ s) s

FTC-internalized equation (10.43), rather than a derivative field.

noncomputable def Section10Lemma1028.logEnvelopeMinus (R ξ : ℝ → ℝ) (c s : ℝ) : ℝ

Logarithm of the decreasing weighted envelope from Lemma 10.28.

Equations

• Section10Lemma1028.logEnvelopeMinus R ξ c s = Real.log (R s) + Section10Lemma1028.xiPhase ξ s - c * s

theorem Section10Lemma1028.lemma1028_logEnvelopeMinus_hasDerivAt {R ξ : ℝ → ℝ} (hξ : Proposition1020Xi ξ) {c s : ℝ} (hs : 0 < s) (hR : 0 < R s) (hDDE : HasDerivAt R (-(2 * R s + R (s - 1)) / s) s) : HasDerivAt (logEnvelopeMinus R ξ c) (-R (s - 1) / (s * R s) + ξ s - c - 2 / s) s

Audited normalized identity (10.44), specialized to a = 2, b = 1. The source's printed ξ(s/λ) is inconsistent with (10.43), (10.45), and the rest of the proof; at b = 1 the corrected term is ξ s.

theorem Section10Lemma1028.lemma1028_commonMajorantSlope_of_deriv_nonpos {R ξ : ℝ → ℝ} (hξ : Proposition1020Xi ξ) {c s : ℝ} (hs : 0 < s) (hR : 0 < R s) (hDDE : HasDerivAt R (-(2 * R s + R (s - 1)) / s) s) (hslope : deriv (logEnvelopeMinus R ξ c) s ≤ 0) : -R (s - 1) + s * (ξ s - c - 2 / s) * R s ≤ 0

Equation (10.44) after multiplication by the positive s R(s). This is exactly the slope-to-envelope bridge needed by the one-sided half of Lemma 10.28; it assumes a derivative sign, not a unit-shift ratio.

The remaining source step is genuinely Lemma 10.28, pp.53--58: prove the nonpositive derivative sign globally from the pairing identity by the first-crossing argument and the integration-by-parts estimate (10.53). It is intentionally not postulated here. In particular, no field or theorem assumes R(s-1) / R(s) or the Lemma 10.29 unit-shift conclusion.