theorem Section10Lemma1022.weighted_strict_growth {b E c s L : ℝ} {f : ℝ → ℝ} (hb : 0 < b) (hden : 0 < s + E) (hs : 0 ≤ s - 1) (hfcont : ContinuousOn f (Set.Icc (s - 1) s)) (hlocal : (s + E) * f s ≥ b * ∫ (t : ℝ) in s - 1..s, f t) (hkernel : 1 < lowerKernel b E c s) (hfloor : ∀ t ∈ Set.Icc (s - 1) s, L ≤ lowerWeighted f b c t) (hL : 0 < L) : L < lowerWeighted f b c s

Conjugating the local integral inequality (10.33) by the canonical phase turns the canonical-kernel estimate into the strict local growth used at the least downward crossing.

theorem Section10Lemma1022.lemma10_22_lower_barrier_eventually_of_kernel {b E s₀ : ℝ} {f : ℝ → ℝ} (hb : 0 < b) (_hE : 1 ≤ E) (hcanonical : CanonicalKernelGrowth b E) (hs₀ : 0 ≤ s₀) (hcont : ContinuousOn f (Set.Ici s₀)) (hpos : ∀ (s : ℝ), s₀ ≤ s → 0 < f s) (hlocal : ∀ᶠ (s : ℝ) in Filter.atTop, (s + E) * f s ≥ b * ∫ (t : ℝ) in s - 1..s, f t) : ∃ (c : ℝ), 1 ≤ c ∧ ∀ᶠ (s : ℝ) in Filter.atTop, Real.exp ((-∫ (t : ℝ) in b..s, Section10CanonicalXi.xi (t / b)) - c * Real.log (s + Real.exp 1)) < f s

Source-faithful topological half of Suzuki Lemma 10.22. The canonical kernel estimate is obtained from canonicalKernel_growth; neither the desired barrier nor first-crossing exclusion is a premise. One common eventual threshold is fixed before the least-crossing argument, so every later point has both the local inequality and the strict kernel estimate.

theorem Section10Lemma1022.lemma10_22_lower_barrier_one {E s₀ : ℝ} {f : ℝ → ℝ} (hE : 1 ≤ E) (hs₀ : 0 ≤ s₀) (hcont : ContinuousOn f (Set.Ici s₀)) (hpos : ∀ (s : ℝ), s₀ ≤ s → 0 < f s) (hlocal : ∀ᶠ (s : ℝ) in Filter.atTop, (s + E) * f s ≥ ∫ (t : ℝ) in s - 1..s, f t) : ∃ (c : ℝ), 1 ≤ c ∧ ∀ᶠ (s : ℝ) in Filter.atTop, Real.exp ((-∫ (t : ℝ) in 1..s, Section10CanonicalXi.xi t) - c * Real.log (s + Real.exp 1)) < f s

Suzuki Lemma 10.22 specialized to the κ=b=1 application used in Section 13.