The analytic core preceding Suzuki (10.53)

This file internalizes the exact calculus and pairing identities used before the asymptotic estimates in (10.47)--(10.53). No derivative sign, adjacent-value estimate, or Equation1053MinusExclusion is assumed.

noncomputable def Section10Equation1053.phiMinus (ξ : ℝ → ℝ) (c s : ℝ) : ℝ

The phase φ₋(s)=∫₁ˢ ξ(t)dt-cs.

Equations

• Section10Equation1053.phiMinus ξ c s = Section10Lemma1028.xiPhase ξ s - c * s

noncomputable def Section10Equation1053.psiMinus (r ξ : ℝ → ℝ) (c s : ℝ) : ℝ

The exponent ψ₋(s)=φ₋(s)-log r(s+1) in (10.46)--(10.53).

Equations

• Section10Equation1053.psiMinus r ξ c s = Section10Equation1053.phiMinus ξ c s - Real.log (r (s + 1))

noncomputable def Section10Equation1053.envelopeMinus (R ξ : ℝ → ℝ) (c s : ℝ) : ℝ

Weighted minus envelope, in a form convenient for the pairing identity.

Equations

• Section10Equation1053.envelopeMinus R ξ c s = R s * Real.exp (Section10Equation1053.phiMinus ξ c s)

@[simp]

theorem Section10Equation1053.exp_neg_psiMinus {r ξ : ℝ → ℝ} {c t : ℝ} (hr : 0 < r (t + 1)) : Real.exp (-psiMinus r ξ c t) = r (t + 1) * Real.exp (-phiMinus ξ c t)

theorem Section10Equation1053.adjoint_hasDerivAt {R : ℝ → ℝ} {β : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) {s : ℝ} (hs : 0 < s) : HasDerivAt h.adjoint ((h.adjoint s + h.adjoint (s + 1)) / s) s

The adjoint equation alone gives the exact first derivative of r. For a=2,b=1 this is the non-asymptotic precursor of source (10.41).

theorem Section10Equation1053.log_adjoint_shift_hasDerivAt {R : ℝ → ℝ} {β : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) {s : ℝ} (hs : 0 < s + 1) (hr : 0 < h.adjoint (s + 1)) : HasDerivAt (fun (t : ℝ) => Real.log (h.adjoint (t + 1))) ((h.adjoint (s + 1) + h.adjoint (s + 2)) / ((s + 1) * h.adjoint (s + 1))) s

Exact derivative of log r(s+1), before the asymptotic replacement (10.41).

theorem Section10Equation1053.psiMinus_hasDerivAt {R ξ : ℝ → ℝ} {β c s : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hξ : Section10Lemma1028.Proposition1020Xi ξ) (hs : 0 < s + 1) (hr : 0 < h.adjoint (s + 1)) : HasDerivAt (psiMinus h.adjoint ξ c) (ξ s - c - (h.adjoint (s + 1) + h.adjoint (s + 2)) / ((s + 1) * h.adjoint (s + 1))) s

Exact version of the first line used in (10.47). The paper next replaces its adjoint quotient by (λ-1)/s + O(1/s²).

theorem Section10Equation1053.canonicalXi_unit_secant {ξ : ℝ → ℝ} (hξ : Section10Lemma1028.Proposition1020Xi ξ) {s t : ℝ} (hs : 3 ≤ s) (ht : t ∈ Set.Icc (s - 1) s) : 0 ≤ ξ s - ξ t ∧ ξ s - ξ t ≤ 2 * (s - t)

A pointwise Taylor/secant estimate for the canonical phase on a unit interval. This is the part of (10.47) supplied solely by Proposition 10.20.

theorem Section10Equation1053.exp_neg_integral_by_parts {ψ p q : ℝ → ℝ} {a b : ℝ} (hψ : ∀ t ∈ Set.uIcc a b, HasDerivAt ψ (p t) t) (hp : ∀ t ∈ Set.uIcc a b, HasDerivAt p (q t) t) (hp0 : ∀ t ∈ Set.uIcc a b, p t ≠ 0) (hmain : IntervalIntegrable (fun (t : ℝ) => Real.exp (-ψ t)) MeasureTheory.volume a b) (hrem : IntervalIntegrable (fun (t : ℝ) => Real.exp (-ψ t) * q t / p t ^ 2) MeasureTheory.volume a b) : ∫ (t : ℝ) in a..b, Real.exp (-ψ t) = Real.exp (-ψ a) / p a - Real.exp (-ψ b) / p b - ∫ (t : ℝ) in a..b, Real.exp (-ψ t) * q t / p t ^ 2

Exact integration-by-parts identity underlying (10.53). It deliberately keeps the remainder integral explicit; bounding it is precisely where source (10.41)--(10.42), (10.47)--(10.52), and the asymptotics of Proposition 10.20 enter.

theorem Section10Equation1053.pairing_zero_weighted_identity {R ξ : ℝ → ℝ} {β c s : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hs : β < s) (hr : ∀ t ∈ Set.Icc (s - 1) s, 0 < h.adjoint (t + 1)) : s * h.adjoint s * R s = ∫ (t : ℝ) in s - 1..s, envelopeMinus R ξ c t * Real.exp (-psiMinus h.adjoint ξ c t)

Pairing-zero rewritten in the weighted variables used in (10.54), with no monotonicity hypothesis.