5.4. Global saddle asymptotics
The damping bounds now determine the exterior signs of f_+, f_-, f_0. On each contour, the
centered phase is quadratic near T = 0, the factor P_j(T+iu) is asymptotic to P_j(iu), and
the remaining contour is negligible.
Fix 0 < \epsilon < \epsilon_0, let \lambda = d/2, and recall u_0, U from
Definition 5.2.1 and u_* from Definition 5.3.1. For u > -1 and
P \in \{P_+, P_-, P_0\} put
I_{\lambda,P}(u) = \int_{\mathbb{R}}e^{\mathcal{L}_u(T)}P(T + iu)\,dT
with \mathcal{L}_u from Definition 5.3.8. For all sufficiently large d
(equation (70)),
\Bigl|I_{\lambda,P}(u) - P(iu)\sqrt{\dfrac{2\pi}{\lambda V(u)}}\Bigr| < |P(iu)|\sqrt{\dfrac{2\pi}{\lambda V(u)}}
uniformly for u \ge u_* when P = P_+, and uniformly for u \ge u_0 when P = P_- or
P = P_0; in particular I_{\lambda,P}(u), and hence f_j(e^{v(u)}), has the sign of
P(iu) there. The same holds for every polynomial P of degree at most 3 with
\overline{P(\zeta)} = P(-\bar\zeta), on any range u \ge u_0(P) > -1 on which P(iu) stays
bounded away from 0; the formalization treats the two branches u \le U (gamma-controlled)
and u \ge U (shell-controlled) separately.
Lean code for Lemma5.4.1●4 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/UpperBound/GaussianError.leancomplete
theorem CohnElkies.eventually_firstBranch_fullGaussianError : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (P : ℂ → ℂ) (u₀ : ℝ), CohnElkies.IsSaddlePolynomial ε P → CohnElkies.SaddleRangeBounds P u₀ → ∀ᶠ (ℓ : ℝ) in Filter.atTop, ∀ (u : ℝ), -1 < u → u ≤ 1 + ε / 2 → Real.log ℓ / 4 ≤ ℓ * (1 + u) → u₀ ≤ u → ‖(∫ (T : ℝ), CohnElkies.centeredIntegrand ε ℓ P u (CohnElkies.vℓ ε ℓ u) T) - ∫ (T : ℝ), CohnElkies.gaussianIntegrand ε ℓ P u T‖ < ‖P (Complex.I * ↑u)‖ * ∫ (T : ℝ), CohnElkies.saddleSourceGaussianKernel ε ℓ u T
theorem CohnElkies.eventually_firstBranch_fullGaussianError : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (P : ℂ → ℂ) (u₀ : ℝ), CohnElkies.IsSaddlePolynomial ε P → CohnElkies.SaddleRangeBounds P u₀ → ∀ᶠ (ℓ : ℝ) in Filter.atTop, ∀ (u : ℝ), -1 < u → u ≤ 1 + ε / 2 → Real.log ℓ / 4 ≤ ℓ * (1 + u) → u₀ ≤ u → ‖(∫ (T : ℝ), CohnElkies.centeredIntegrand ε ℓ P u (CohnElkies.vℓ ε ℓ u) T) - ∫ (T : ℝ), CohnElkies.gaussianIntegrand ε ℓ P u T‖ < ‖P (Complex.I * ↑u)‖ * ∫ (T : ℝ), CohnElkies.saddleSourceGaussianKernel ε ℓ u T
Report §4.3, first branch: the centred integral of a saddle polynomial `P` is approximated by its Gaussian with an error smaller than the Gaussian mass `‖P(iu)‖ ∫ e^{-λV T²/2}`. -
theoremdefined in CohnElkies/UpperBound/GaussianError.leancomplete
theorem CohnElkies.eventually_secondBranch_fullGaussianError : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (P : ℂ → ℂ) (u₀ : ℝ), CohnElkies.IsSaddlePolynomial ε P → CohnElkies.SaddleRangeBounds P u₀ → ∀ᶠ (ℓ : ℝ) in Filter.atTop, ∀ (δ : ℝ), ε / 2 ≤ δ → u₀ ≤ 1 + δ → ‖(∫ (T : ℝ), CohnElkies.centeredIntegrand ε ℓ P (1 + δ) (CohnElkies.vℓ ε ℓ (1 + δ)) T) - ∫ (T : ℝ), CohnElkies.gaussianIntegrand ε ℓ P (1 + δ) T‖ < ‖P (Complex.I * ↑(1 + δ))‖ * ∫ (T : ℝ), CohnElkies.saddleSourceGaussianKernel ε ℓ (1 + δ) T
theorem CohnElkies.eventually_secondBranch_fullGaussianError : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (P : ℂ → ℂ) (u₀ : ℝ), CohnElkies.IsSaddlePolynomial ε P → CohnElkies.SaddleRangeBounds P u₀ → ∀ᶠ (ℓ : ℝ) in Filter.atTop, ∀ (δ : ℝ), ε / 2 ≤ δ → u₀ ≤ 1 + δ → ‖(∫ (T : ℝ), CohnElkies.centeredIntegrand ε ℓ P (1 + δ) (CohnElkies.vℓ ε ℓ (1 + δ)) T) - ∫ (T : ℝ), CohnElkies.gaussianIntegrand ε ℓ P (1 + δ) T‖ < ‖P (Complex.I * ↑(1 + δ))‖ * ∫ (T : ℝ), CohnElkies.saddleSourceGaussianKernel ε ℓ (1 + δ) T
Report §4.3, second branch: the centred integral of a saddle polynomial `P` is approximated by its Gaussian with an error smaller than the Gaussian mass.
-
theoremdefined in CohnElkies/UpperBound/Signs.leancomplete
theorem CohnElkies.eventually_mellinProfile_re_mul_pos_firstBranch : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (P : ℂ → ℂ) (u₀ : ℝ), CohnElkies.IsSaddlePolynomial ε P → CohnElkies.SaddleRangeBounds P u₀ → ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (c u : ℝ), -1 < u → u ≤ 1 + ε / 2 → Real.log (↑d / 2) / 4 ≤ ↑d / 2 * (1 + u) → u₀ ≤ u → 0 < (P (Complex.I * ↑u)).re * (CohnElkies.mellinProfile ε (↑d / 2) P c (Real.exp (CohnElkies.logRadius ε d u))).re
theorem CohnElkies.eventually_mellinProfile_re_mul_pos_firstBranch : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (P : ℂ → ℂ) (u₀ : ℝ), CohnElkies.IsSaddlePolynomial ε P → CohnElkies.SaddleRangeBounds P u₀ → ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (c u : ℝ), -1 < u → u ≤ 1 + ε / 2 → Real.log (↑d / 2) / 4 ≤ ↑d / 2 * (1 + u) → u₀ ≤ u → 0 < (P (Complex.I * ↑u)).re * (CohnElkies.mellinProfile ε (↑d / 2) P c (Real.exp (CohnElkies.logRadius ε d u))).re
Report §4.3, first branch: at the saddle point of height `u` (`-1 < u ≤ 1 + ε/2`, with `log λ / 4 ≤ λ(1 + u)`) the profile `f_P` of a saddle polynomial with range bounds on `u ≥ u₀` has the sign of `P(iu)`, whatever its origin value `c`.
-
theoremdefined in CohnElkies/UpperBound/Signs.leancomplete
theorem CohnElkies.eventually_mellinProfile_re_mul_pos_secondBranch : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (P : ℂ → ℂ) (u₀ : ℝ), CohnElkies.IsSaddlePolynomial ε P → CohnElkies.SaddleRangeBounds P u₀ → ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (c u : ℝ), 1 + ε / 2 ≤ u → u₀ ≤ u → 0 < (P (Complex.I * ↑u)).re * (CohnElkies.mellinProfile ε (↑d / 2) P c (Real.exp (CohnElkies.logRadius ε d u))).re
theorem CohnElkies.eventually_mellinProfile_re_mul_pos_secondBranch : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (P : ℂ → ℂ) (u₀ : ℝ), CohnElkies.IsSaddlePolynomial ε P → CohnElkies.SaddleRangeBounds P u₀ → ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (c u : ℝ), 1 + ε / 2 ≤ u → u₀ ≤ u → 0 < (P (Complex.I * ↑u)).re * (CohnElkies.mellinProfile ε (↑d / 2) P c (Real.exp (CohnElkies.logRadius ε d u))).re
Report §4.3, second branch: at the saddle point of height `u ≥ 1 + ε/2` the profile `f_P` of a saddle polynomial with range bounds on `u ≥ u₀` has the sign of `P(iu)`.
Contour shift. The poles of the integrand in (38) are t = -i(\lambda + 2n), n \ge 0, so
Lemma 5.2.17 allows the contour to be shifted to t = \lambda(T + iu) whenever u > -1
(CohnElkies.expL_stationary_eq).
At r = e^{v(u)} the shifted Mellin inversion formula reads (equation (71))
f_j(e^{v(u)})
= \dfrac{\lambda E_\lambda(i\lambda u)}{2\pi}\,e^{-(1+u)\lambda v(u)}\,I_{\lambda,P_j}(u),
with a positive prefactor. By Lemma 5.2.16, P_+(iu) > 0 for u > -1,
while P_-(iu) < 0 and P_0(iu) > 0 for u \ge u_0; their fixed degrees and uniform lower
bounds on those ranges give (equation (72))
\dfrac{|P(T+iu)|}{|P(iu)|} \ll_\epsilon 1 + |T|^3,
\dfrac{P(T+iu)}{P(iu)} = 1 + O_\epsilon(|T| + |T|^3).
Central interval. Choose K \to \infty (depending on d and u) and set
T_* = K/\sqrt{\lambda V(u)}. By (50) of Lemma 5.3.12, the phase on |T| \le T_* is
\mathcal{L}_u(T) = -\tfrac{\lambda V(u)}{2}T^2 + O(\lambda M_3|T|^3). The approximation is
uniform
if the central interval shrinks and the cubic error tends to zero:
T_* = o_\epsilon(1), K^3M_3/(\sqrt\lambda\,V(u)^{3/2}) = o_\epsilon(1). Under these
conditions,
(72) and the substitution x = \sqrt{\lambda V(u)}\,T give
\int_{|T|\le T_*}e^{\mathcal{L}_u(T)}P(T+iu)\,dT
= P(iu)\sqrt{2\pi/(\lambda V(u))}\,(1 + o_\epsilon(1)),
using \int_{-K}^Ke^{-x^2/2}\,dx \to \sqrt{2\pi}. It remains to show that the integral over
|T| > T_* is o_\epsilon(|P(iu)|/\sqrt{\lambda V(u)}); we verify the conditions and the tail
bound separately on [u_*, U] and [U,\infty).
Gamma-controlled range u_* \le u \le U. Put \eta = 1+u and L = \lambda\eta. By (56)–(57) of
Lemma 5.3.16 and Lemma 5.3.17,
L \ge \tfrac14\log\lambda, V(u) \asymp_\epsilon \eta^{-1},
M_3 \ll_\epsilon \eta^{-2}. Choosing K = L^{1/12}, so that K \to \infty and
K^3 = o(\sqrt L),
gives T_*/\eta \ll_\epsilon L^{-5/12} and
K^3M_3/(\sqrt\lambda V(u)^{3/2}) \ll_\epsilon L^{-1/4}. The
damping bounds (55) and (53) (Lemma 5.3.15, Lemma 5.3.14) are
quadratic for |T| \le \eta and linear for |T| \ge \eta.
Consequently
\sup_{|T|\le T_*}|\mathcal{L}_u(T) + \tfrac{\lambda V(u)}{2}T^2| \ll_\epsilon L^{-1/4},
\sqrt{\lambda V(u)}\int_{T_*\le|T|\le\eta}(1+|T|^3)e^{-D_u(T)}\,dT
\ll_\epsilon e^{-c_\epsilon K^2},
\sqrt{\lambda V(u)}\int_{|T|\ge\eta}(1+|T|^3)e^{-D_u(T)}\,dT \ll_\epsilon e^{-c_\epsilon L}
(the Gaussian tail via \int_K^\infty e^{-cx^2}\,dx \le e^{-cK^2}/(2cK), the exponential tail via
\int_\eta^\infty(1+T^3)e^{-c\epsilon\lambda T}\,dT \ll (1+\eta^3)e^{-c\epsilon L}/\lambda). Both
tail
estimates tend to zero uniformly because L \ge (\log\lambda)/4, proving (70) on [u_*, U].
Shell-controlled range u \ge U. Write \delta = u - 1. By (63) and (66) of
Lemma 5.3.21,
the remote shell controls both curvature and third moment:
V(u) \asymp_\epsilon V_B \gg_\epsilon 1
and M_3 \ll_\epsilon V(u). Take K = \lambda^{1/12}; then T_* \ll_\epsilon \lambda^{-5/12}
and
K^3M_3/(\sqrt\lambda V(u)^{3/2}) \ll_\epsilon \lambda^{-1/4}; in particular T_* < T_0 for
large
\lambda. The quadratic bound (67) of Lemma 5.3.22 on |T| \le T_0 yields (equation
(73))
\sup_{|T|\le T_*}|\mathcal{L}_u(T) + \tfrac{\lambda V(u)}{2}T^2| \ll_\epsilon \lambda^{-1/4} and
\sqrt{\lambda V(u)}\int_{T_*\le|T|\le T_0}(1+|T|^3)e^{-D_u(T)}\,dT
\ll_\epsilon e^{-c_\epsilon K^2}.
For T_0 \le |T| \le \eta, the variance bound (64) (Lemma 5.3.20)
and the damping estimate (68) give
(equation (74))
\sqrt{\lambda V(u)}\int_{T_0\le|T|\le\eta}(1+|T|^3)e^{-D_u(T)}\,dT
\ll_\epsilon \sqrt\lambda\,e^{\Phi(\delta)},
\Phi(\delta) = \dfrac{B+1}{2}\delta + 4\log(2+\delta) - c_\epsilon\lambda Qe^{B\delta}, which is
o_\epsilon(1). The exponent \Phi decreases in \delta \ge \epsilon/2, since its derivative
(B+1)/2 + 4/(2+\delta) - c_\epsilon\lambda BQe^{B\delta} is negative for large \lambda; at
\delta = \epsilon/2 it equals -c_\epsilon'\lambda + O_\epsilon(1). Thus the middle-frequency
contribution tends to zero uniformly even as u \to \infty. Finally, for |T| \ge \eta, (69)
supplies the positive-shell damping and a linear gamma tail, so (equation (75))
\sqrt{\lambda V(u)}\int_{|T|\ge\eta}(1+|T|^3)e^{-D_u(T)}\,dT \ll_\epsilon e^{-c_\epsilon\lambda}
uniformly in \delta: as in (74), the damping -c_\epsilon\lambda Qe^{B\delta} absorbs the
growth
of \sqrt{V(u)}. Equations (73)–(75) prove the saddle formula on every u \ge U.
For every fixed 0 < \epsilon < \epsilon_0 there is d_\epsilon such that, for every integer
d \ge d_\epsilon, with v from Definition 5.3.2 (equation (76)):
f_+(r) > 0 at every saddle radius r = e^{v(u)}, u \ge u_*, and f_+(r) \ge 0 for all
r \ge r_* = e^{v(u_*)}; f_-(r) < 0 for r \ge R_{\epsilon,d} = e^{v(u_0)}; and
f_0(r) > 0 for r \ge R_{\epsilon,d}.
Lean code for Theorem5.4.2●5 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/UpperBound/Signs.leancomplete
theorem CohnElkies.eventually_fPlus_re_pos_firstBranch : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (u : ℝ), CohnElkies.u_star ε d ≤ u → u ≤ 1 + ε / 2 → 0 < (CohnElkies.fPlus ε (↑d / 2) (Real.exp (CohnElkies.logRadius ε d u))).re
theorem CohnElkies.eventually_fPlus_re_pos_firstBranch : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (u : ℝ), CohnElkies.u_star ε d ≤ u → u ≤ 1 + ε / 2 → 0 < (CohnElkies.fPlus ε (↑d / 2) (Real.exp (CohnElkies.logRadius ε d u))).re
`Re f₊ > 0` at the saddles of the first branch `u_* ≤ u ≤ 1 + ε/2`.
-
theoremdefined in CohnElkies/UpperBound/Signs.leancomplete
theorem CohnElkies.eventually_fPlus_re_pos_secondBranch : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (u : ℝ), 1 + ε / 2 ≤ u → 0 < (CohnElkies.fPlus ε (↑d / 2) (Real.exp (CohnElkies.logRadius ε d u))).re
theorem CohnElkies.eventually_fPlus_re_pos_secondBranch : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (u : ℝ), 1 + ε / 2 ≤ u → 0 < (CohnElkies.fPlus ε (↑d / 2) (Real.exp (CohnElkies.logRadius ε d u))).re
`Re f₊ > 0` at the saddles of the second branch `1 + ε/2 ≤ u`.
-
theoremdefined in CohnElkies/UpperBound/Signs.leancomplete
theorem CohnElkies.eventually_fPlus_nonneg_of_star : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (r : ℝ), CohnElkies.r_star ε d ≤ r → 0 ≤ (CohnElkies.fPlus ε (↑d / 2) r).re
theorem CohnElkies.eventually_fPlus_nonneg_of_star : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (r : ℝ), CohnElkies.r_star ε d ≤ r → 0 ≤ (CohnElkies.fPlus ε (↑d / 2) r).re
`Re f₊ ≥ 0` beyond the small radius `r_*`, covering both saddle branches.
-
theoremdefined in CohnElkies/UpperBound/Signs.leancomplete
theorem CohnElkies.eventually_fMinus_re_neg_of_radius : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (r : ℝ), CohnElkies.R_ε ε d ≤ r → (CohnElkies.fMinus ε (↑d / 2) r).re < 0
theorem CohnElkies.eventually_fMinus_re_neg_of_radius : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (r : ℝ), CohnElkies.R_ε ε d ≤ r → (CohnElkies.fMinus ε (↑d / 2) r).re < 0
Report §4.3: `Re f₋ < 0` beyond the source radius `R_ε`, covering both saddle branches.
-
theoremdefined in CohnElkies/UpperBound/SelfFourier.leancomplete
theorem CohnElkies.eventually_fZero_re_pos_of_radius : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (r : ℝ), CohnElkies.R_ε ε d ≤ r → 0 < (CohnElkies.fZero ε (↑d / 2) r).re
theorem CohnElkies.eventually_fZero_re_pos_of_radius : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (r : ℝ), CohnElkies.R_ε ε d ≤ r → 0 < (CohnElkies.fZero ε (↑d / 2) r).re
Report §4.3 and Corollary 4.9 for `P₀`: for every sufficiently small `ε > 0` and all large `d`, `Re f₀(r) > 0` for all `r ≥ R_{ε,d}`.
For u > -1 the prefactor of I_{\lambda,P_j}(u) in (71) is positive, so (70) of
Lemma 5.4.1 identifies the sign of f_j(e^{v(u)}) with that of P_j(iu) for all
sufficiently large d, uniformly on the stated ranges of u. Equations (56) and (63) of
Lemma 5.3.16 and Lemma 5.3.21 give
v'(u) = V(u) > 0 on [u_*,\infty), and (44) with the positive shell w_B gives
v(u) \to \infty as u \to \infty. Thus [u_*,\infty) parametrizes every radius
r \ge e^{v(u_*)} and [u_0,\infty) every radius r \ge e^{v(u_0)}
(Lemma 5.4.3). The signs in Lemma 5.2.16 now
give (76).
For every sufficiently small \epsilon, every d \ge 1 and every u_0 > -1, the map
u \mapsto v(u) of Definition 5.3.2 is continuous on [u_0, \infty) and
every radius r \ge e^{v(u_0)} is attained: r = e^{v(u)} for some u \ge u_0.
Lean code for Lemma5.4.3●2 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/UpperBound/Coverage.leancomplete
theorem CohnElkies.eventually_saddleLogRadius_covers_Ici : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (d : ℕ), 0 < d → ∀ (u₀ : ℝ), -1 < u₀ → ∀ (r : ℝ), Real.exp (CohnElkies.logRadius ε d u₀) ≤ r → ∃ u, u₀ ≤ u ∧ CohnElkies.logRadius ε d u = Real.log r
theorem CohnElkies.eventually_saddleLogRadius_covers_Ici : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (d : ℕ), 0 < d → ∀ (u₀ : ℝ), -1 < u₀ → ∀ (r : ℝ), Real.exp (CohnElkies.logRadius ε d u₀) ≤ r → ∃ u, u₀ ≤ u ∧ CohnElkies.logRadius ε d u = Real.log r
Report Corollary 4.9: every radius above `e^{v(u₀)}` is attained by some `u ≥ u₀`. -
theoremdefined in CohnElkies/UpperBound/Coverage.leancomplete
theorem CohnElkies.logRadius_continuousOn_Ici {ε : ℝ} (hε : 0 < ε) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε) {d : ℕ} (hd : 0 < d) {u₀ : ℝ} (hu₀ : -1 < u₀) : ContinuousOn (CohnElkies.logRadius ε d) (Set.Ici u₀)
theorem CohnElkies.logRadius_continuousOn_Ici {ε : ℝ} (hε : 0 < ε) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε) {d : ℕ} (hd : 0 < d) {u₀ : ℝ} (hu₀ : -1 < u₀) : ContinuousOn (CohnElkies.logRadius ε d) (Set.Ici u₀)
Continuity of the digamma function on (0, \infty) (Definition 3.1.4) and of the shell
integral, and v(u) \to \infty as u \to \infty (the positive shell makes
\int w(a)a\sinh(ua)\,da \to +\infty, and \psi(\lambda(1+u)/2) \to \infty); the intermediate
value theorem does the rest. The formalization only uses continuity of v and its divergence,
not the strict monotonicity.