noncomputable def Section10Lemma1022.lowerPhase (b c s : ℝ) : ℝ

Suzuki's phase in Lemma 10.22, with the harmless s + exp 1 normalization already built in.

Equations

• Section10Lemma1022.lowerPhase b c s = (∫ (t : ℝ) in b..s, Section10CanonicalXi.xi (t / b)) + c * Real.log (s + Real.exp 1)

theorem Section10Lemma1022.lowerPhase_continuousOn {s₀ b c : ℝ} (hs₀ : 0 ≤ s₀) : ContinuousOn (lowerPhase b c) (Set.Ici s₀)

noncomputable def Section10Lemma1022.lowerWeighted (f : ℝ → ℝ) (b c s : ℝ) : ℝ

The weighted function used in the least-downward-crossing argument.

Equations

• Section10Lemma1022.lowerWeighted f b c s = f s * Real.exp (Section10Lemma1022.lowerPhase b c s)

theorem Section10Lemma1022.lowerWeighted_continuousOn {f : ℝ → ℝ} {s₀ b c : ℝ} (hs₀ : 0 ≤ s₀) (hf : ContinuousOn f (Set.Ici s₀)) : ContinuousOn (lowerWeighted f b c) (Set.Ici s₀)

theorem Section10Lemma1022.least_downward_crossing {g : ℝ → ℝ} {S L : ℝ} (hcont : ContinuousOn g (Set.Ici (S - 1))) (hinit : ∀ t ∈ Set.Icc (S - 1) S, L ≤ g t) (hboost : ∀ (s : ℝ), S ≤ s → (∀ t ∈ Set.Icc (s - 1) s, L ≤ g t) → L < g s) (s : ℝ) : S ≤ s → L < g s

Abstract topological core of Suzuki's least-downward-crossing argument. The hboost premise is the strict one-step estimate (10.38), not a barrier conclusion or a pre-packaged first-crossing exclusion.