The lower bound of Proposition 3(i): the asymptotics

This file proves the last step of the lower bound in Proposition 3(i) of the paper (Section S1.6, 'Proof of Proposition 3(i), lower bound'): from the lower bound (S9) of Lemma S6 for fixed K, the choices c' = s(2 log K + 4 log log K)^{1/2}, c = (c' + r^{-1/2})/(1 − r^{-1/2}), and K = ⌊log T/log r⌋ give liminf_{T→∞} Γ_T/log log T ≥ 1 − s²/(1 − r^{-1/2})², and letting r → ∞ gives 1 − s². The bound (S9) enters as a hypothesis on a sequence Γ_T, so that the results hold for every ρ > 0 and any numéraires of Q, as in the proof of Proposition S5.

The paper states the asymptotics with O and o terms. We make them explicit: for K ≥ 3 and r ≥ 4, with L = log K and δ = 1 − r^{-1/2}, the right-hand side of (S9) is at least (1 − s²/δ²)L − 28L^{1/2} − C₀ for a constant C₀ that depends only on s and ρ (fixedKBound_lbLevel_ge), and log log T − log(2 log r) ≤ L ≤ log log T. The case of a coefficient 1 − s²/δ² that is not positive does not occur, since we choose r with 1 − s²/δ² above the target rate.

• fixedKBound s ρ r K c: the right-hand side of (S9);
• lbLevel s r K: the level c of the paper, with lbCPrime_lbLevel (c − (c + 1)r^{-1/2} = c') and mul_exp_lbCPrime_lbLevel (K exp{−c'²/(2s²)} = (log K)^{-2});
• lbBeta_lbLevel_ge, lbBeta_le, fixedK_tail_le: bounds on β and on the last term of (S9);
• fixedKBound_lbLevel_ge: the lower bound on the right-hand side of (S9);
• eventually_lt_of_fixedKBound: for every a < 1 − s², eventually a log log T < Γ_T.

The right-hand side of (S9) and the choice of c

noncomputable def LogOptimal.fixedKBound (s ρ : ℝ) (r K : ℕ) (c : ℝ) : ℝ

The right-hand side of eq. (S9) of Lemma S6, β − (β − β')K exp{−c'²/(2s²)} − {2(c + 1)/γ + 2(c + 1)²/(3γ²)}/(K + 1), with β = lbBeta s ρ K c, β' = lbBetaPrime s ρ, c' = lbCPrime r c, and γ = (ρ² + s²)^{1/2}.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LogOptimal.lbLevel (s : ℝ) (r K : ℕ) : ℝ

The level c = (c' + r^{-1/2})/(1 − r^{-1/2}) of the proof of Proposition 3(i), lower bound, with c' = s(2 log K + 4 log log K)^{1/2}.

Equations

• LogOptimal.lbLevel s r K = (s * √(2 * Real.log ↑K + 4 * Real.log (Real.log ↑K)) + (√↑r)⁻¹) / (1 - (√↑r)⁻¹)

theorem LogOptimal.lbCPrime_lbLevel (s : ℝ) {r : ℕ} (hr : 4 ≤ r) (K : ℕ) : lbCPrime r (lbLevel s r K) = s * √(2 * Real.log ↑K + 4 * Real.log (Real.log ↑K))

c − (c + 1)r^{-1/2} = c' for the level c of the paper.

theorem LogOptimal.lbLevel_add_one (s : ℝ) {r : ℕ} (hr : 4 ≤ r) (K : ℕ) : lbLevel s r K + 1 = (s * √(2 * Real.log ↑K + 4 * Real.log (Real.log ↑K)) + 1) / (1 - (√↑r)⁻¹)

c + 1 = (c' + 1)/(1 − r^{-1/2}) for the level c of the paper.

theorem LogOptimal.mul_exp_lbCPrime_lbLevel {s : ℝ} (hs : 0 < s) {r : ℕ} (hr : 4 ≤ r) {K : ℕ} (hK : 3 ≤ K) : ↑K * Real.exp (-lbCPrime r (lbLevel s r K) ^ 2 / (2 * s ^ 2)) = 1 / Real.log ↑K ^ 2

K exp{−c'²/(2s²)} = (log K)^{-2} for the level c of the paper and K ≥ 3.

Bounds on β and on the last term of (S9)

theorem LogOptimal.lbBeta_lbLevel_ge {s ρ : ℝ} {r K : ℕ} (hs0 : 0 < s) (hs1 : s < 1) (hr : 4 ≤ r) (hK : 3 ≤ K) : (1 - s ^ 2 / (1 - (√↑r)⁻¹) ^ 2) * Real.log ↑K - 28 * √(Real.log ↑K) - (2 + Real.log √(2 * Real.pi) - Real.log (ρ / √(ρ ^ 2 + s ^ 2))) ≤ lbBeta s ρ K (lbLevel s r K)

For K ≥ 3, r ≥ 4, and the level c of the paper, with L = log K and δ = 1 − r^{-1/2}, β ≥ (1 − s²/δ²)L − 28L^{1/2} − {2 + log(2π)^{1/2} − log(ρ/γ)}.

noncomputable def LogOptimal.fixedKConst (s ρ : ℝ) : ℝ

The constant C₀ = 2 + log(2π)^{1/2} − log(ρ/γ) + 2 − β' + 12/γ + 32/γ² of the lower bound on the right-hand side of (S9).

Equations

• LogOptimal.fixedKConst s ρ = 2 + Real.log √(2 * Real.pi) - Real.log (ρ / √(ρ ^ 2 + s ^ 2)) + (2 - LogOptimal.lbBetaPrime s ρ) + (12 / √(ρ ^ 2 + s ^ 2) + 32 / √(ρ ^ 2 + s ^ 2) ^ 2)

theorem LogOptimal.fixedKBound_lbLevel_ge {s ρ : ℝ} {r K : ℕ} (hs0 : 0 < s) (hs1 : s < 1) (hρ : 0 < ρ) (hr : 4 ≤ r) (hK : 3 ≤ K) : (1 - s ^ 2 / (1 - (√↑r)⁻¹) ^ 2) * Real.log ↑K - 28 * √(Real.log ↑K) - fixedKConst s ρ ≤ fixedKBound s ρ r K (lbLevel s r K)

For K ≥ 3, r ≥ 4, and the level c of the paper, the right-hand side of (S9) is at least (1 − s²/δ²)L − 28L^{1/2} − C₀, with L = log K and δ = 1 − r^{-1/2}.

The asymptotics in T

theorem LogOptimal.eventually_lt_of_fixedKBound {s ρ : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hρ : 0 < ρ) {Γ : ℕ → EReal} (hS9 : ∀ (r K T : ℕ) (c : ℝ), 4 ≤ r → 1 ≤ K → r ^ K ≤ T → 0 < c → 0 < lbCPrime r c → lbBetaPrime s ρ ≤ lbBeta s ρ K c → ↑(fixedKBound s ρ r K c) ≤ Γ T) {a : ℝ} (ha : a < 1 - s ^ 2) : ∀ᶠ (T : ℕ) in Filter.atTop, ↑(a * Real.log (Real.log ↑T)) < Γ T

The asymptotics of the lower bound in Proposition 3(i): if a sequence Γ_T is at least the right-hand side of (S9) whenever Lemma S6 applies, then, for every a < 1 − s², eventually a log log T < Γ_T. The parameters are K = ⌊log T/log r⌋, the level c of the paper, and an r ≥ 4 with 1 − s²/(1 − r^{-1/2})² > max(a, 0).