noncomputable def Section10Lemma1022.lowerKernel (b E c s : ℝ) : ℝ

The conjugated one-step kernel in (10.37).

Equations

• Section10Lemma1022.lowerKernel b E c s = b / (s + E) * ∫ (t : ℝ) in s - 1..s, Real.exp (Section10Lemma1022.lowerPhase b c s - Section10Lemma1022.lowerPhase b c t)

def Section10Lemma1022.CanonicalKernelGrowth (b E : ℝ) : Prop

The canonical analytic input required by the downward-crossing core.

Equations

• Section10Lemma1022.CanonicalKernelGrowth b E = ∃ (c : ℝ), 1 ≤ c ∧ ∀ᶠ (s : ℝ) in Filter.atTop, 0 < s + E ∧ 1 < Section10Lemma1022.lowerKernel b E c s

theorem Section10Lemma1022.log_sub_log_ge_endpoint_slope {t s : ℝ} (ht : 0 < t + Real.exp 1) (hts : t ≤ s) : (s - t) / (s + Real.exp 1) ≤ Real.log (s + Real.exp 1) - Real.log (t + Real.exp 1)

Concavity of log, in the endpoint form used in (10.34)--(10.36).

theorem Section10Lemma1022.integral_exp_endpoint (A s : ℝ) (hA : A ≠ 0) : ∫ (t : ℝ) in s - 1..s, Real.exp (A * (s - t)) = (Real.exp A - 1) / A

Exact elementary integral underlying the passage from (10.36) to (10.37).

theorem Section10Lemma1022.lowerPhase_increment_ge {c s t : ℝ} (hc : 0 ≤ c) (hs : Real.exp 1 + 2 ≤ s) (ht : t ∈ Set.Icc (s - 1) s) : Section10CanonicalXi.xi (s - 1) * (s - t) + c / (s + Real.exp 1) * (s - t) ≤ lowerPhase 1 c s - lowerPhase 1 c t

Pointwise canonical phase increment. This is the rigorous endpoint-slope version of (10.34)--(10.36), with no phase-expansion premise.

theorem Section10Lemma1022.canonicalKernelGrowth_one {E : ℝ} (hE : 1 ≤ E) : CanonicalKernelGrowth 1 E

Direct formalization of the canonical-kernel growth in (10.34)--(10.38) for κ = b = 1. The constant is explicit and depends only on E; no kernel growth or phase expansion is assumed.