Lemma 10.28: the global minus-envelope first crossing

This file isolates the topological first-crossing step on pp. 55--58. It does not assume the desired derivative sign and it does not take a common-majorant record as input. The only frozen source boundary is the stationary-point exclusion obtained from the pairing calculation and the unit-interval estimate (10.53). This is the earliest presently unformalized analytic estimate.

noncomputable def Section10Lemma1028FirstCrossing.normalizedMinusBase (R ξ : ℝ → ℝ) (s : ℝ) : ℝ

The normalized part of (10.44), before subtracting c₋.

Equations

• Section10Lemma1028FirstCrossing.normalizedMinusBase R ξ s = -R (s - 1) / (s * R s) + ξ s - 2 / s

structure Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus (R : ℝ → ℝ) (β : ℝ) : Type

Minimal DDE/pairing data. In particular this has no derivative-sign or common-majorant field.

• adjoint : ℝ → ℝ
• beta_ge_one : 1 ≤ β
• continuous : ContinuousOn R (Set.Ioi (β - 1))
• positive (s : ℝ) : β - 1 < s → 0 < R s
• original_dde (s : ℝ) : β < s → HasDerivAt R (-(2 * R s + R (s - 1)) / s) s
• adjoint_positive (s : ℝ) : β ≤ s → 0 < self.adjoint s
• adjoint_dde (s : ℝ) : 0 < s → HasDerivAt (fun (u : ℝ) => u * self.adjoint u) (2 * self.adjoint s + self.adjoint (s + 1)) s
• pairing_zero (s : ℝ) : β < s → s * self.adjoint s * R s = ∫ (t : ℝ) in s - 1..s, self.adjoint (t + 1) * R t

structure Section10Lemma1028FirstCrossing.CanonicalXiTheorem (ξ : ℝ → ℝ) : Prop

Canonical facts about Suzuki's ξ, separated from Lemma 10.28. The final field is the standard eventual comparison ξ(s)-c-2/s ≫ log(es) from Proposition 10.20.

• continuous : Continuous ξ
• positive (s : ℝ) : 1 < s → 0 < ξ s
• equation (s : ℝ) : 1 < s → Real.exp (ξ s) - 1 = s * ξ s
• eventual_log_lower (c : ℝ) : ∃ (S : ℝ) (A : ℝ), 3 ≤ S ∧ 1 ≤ A ∧ ∀ (s : ℝ), S ≤ s → 1 / A * Real.log (Real.exp 1 * s) ≤ ξ s - c - 2 / s

def Section10Lemma1028FirstCrossing.Equation1053MinusExclusion (R ξ : ℝ → ℝ) (s₀ C : ℝ) : Prop

Frozen boundary at (10.53): pairing-zero plus the unit-interval expansion exclude a stationary point of the minus envelope once both s and c₋ are large. Unlike the old residual API, this is neither a derivative-sign premise nor a common-majorant premise.

Equations

• Section10Lemma1028FirstCrossing.Equation1053MinusExclusion R ξ s₀ C = ∀ (c : ℝ), C ≤ c → ∀ (s : ℝ), s₀ ≤ s → Section10Lemma1028FirstCrossing.normalizedMinusBase R ξ s ≠ c

theorem Section10Lemma1028FirstCrossing.global_nonpos_of_equation1053 {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Ici 4)) {s₀ C : ℝ} (hs₀ : 4 ≤ s₀) (hC : 1 ≤ C) (h1053 : ∀ (c : ℝ), C ≤ c → ∀ (s : ℝ), s₀ ≤ s → f s ≠ c) : ∃ (c : ℝ), 1 ≤ c ∧ ∀ (s : ℝ), 4 ≤ s → f s - c ≤ 0

Pure first-crossing lemma. Compactness chooses c large enough on the initial interval. If positivity occurred later, IVT would produce the stationary point excluded by (10.53).

theorem Section10Lemma1028FirstCrossing.normalizedMinusBase_continuousOn {R ξ : ℝ → ℝ} {β : ℝ} (h : FirstCrossingDDEApparatus R β) (hξ : CanonicalXiTheorem ξ) (hβ : β ≤ 3) : ContinuousOn (normalizedMinusBase R ξ) (Set.Ici 4)

The explicit normalized slope is continuous on the legal half-line.

theorem Section10Lemma1028FirstCrossing.lemma1028_global_minus_slope {R ξ : ℝ → ℝ} {β s₀ C : ℝ} (h : FirstCrossingDDEApparatus R β) (hξ : CanonicalXiTheorem ξ) (hβ : β ≤ 3) (hs₀ : 4 ≤ s₀) (hC : 1 ≤ C) (h1053 : Equation1053MinusExclusion R ξ s₀ C) : ∃ (c : ℝ), 1 ≤ c ∧ ∀ (s : ℝ), 4 ≤ s → -R (s - 1) / (s * R s) + ξ s - c - 2 / s ≤ 0

Global nonpositive normalized (10.44), obtained rather than assumed.

structure Section10Lemma1028FirstCrossing.Section10CommonMajorant (R : ℝ → ℝ) : Type

Sanitized output contract: it records a cutoff, so the source's eventual ξ-c₋ lower bound is not incorrectly asserted on the fixed interval [3,S]. The slope conclusion is populated by the constructor below, never supplied as an input to it.

• xi : ℝ → ℝ
• cMinus : ℝ
• cutoff : ℝ
• A : ℝ
• four_le_cutoff : 4 ≤ self.cutoff
• one_le_A : 1 ≤ self.A
• majorizes_log (s : ℝ) : self.cutoff ≤ s → 1 / self.A * Real.log (Real.exp 1 * s) ≤ self.xi s - self.cMinus - 2 / s
• envelope_slope_nonpos (s : ℝ) : self.cutoff ≤ s → -R (s - 1) + s * (self.xi s - self.cMinus - 2 / s) * R s ≤ 0

noncomputable def Section10Lemma1028FirstCrossing.section10_lemma1028_commonMajorant {R ξ : ℝ → ℝ} {β s₀ C : ℝ} (h : FirstCrossingDDEApparatus R β) (hξ : CanonicalXiTheorem ξ) (hβ : β ≤ 3) (hs₀ : 4 ≤ s₀) (hC : 1 ≤ C) (h1053 : Equation1053MinusExclusion R ξ s₀ C) : Section10CommonMajorant R

Lemma 10.28 constructor, conditional only on the canonical ξ theorem and the explicitly frozen (10.53) stationary-point exclusion.

Equations

• Section10Lemma1028FirstCrossing.section10_lemma1028_commonMajorant h hξ hβ hs₀ hC h1053 = { xi := ξ, cMinus := Classical.choose ⋯, cutoff := max 4 (Classical.choose ⋯), A := Classical.choose ⋯, four_le_cutoff := ⋯, one_le_A := ⋯, majorizes_log := ⋯, envelope_slope_nonpos := ⋯ }