The plus first-crossing half of Suzuki Lemma 10.28

This file treats the plus branch directly. In particular, it does not obtain it by changing signs in the minus first-crossing theorem: the first-crossing set, window order, and pairing inequality all have the opposite orientation.

noncomputable def Section10Lemma1028PlusAssembly.phiPlus (ξ : ℝ → ℝ) (c s : ℝ) : ℝ

The plus phase φ₊(s)=∫₁ˢ ξ(t)dt+cs.

Equations

• Section10Lemma1028PlusAssembly.phiPlus ξ c s = Section10Lemma1028.xiPhase ξ s + c * s

noncomputable def Section10Lemma1028PlusAssembly.psiPlus (r ξ : ℝ → ℝ) (c s : ℝ) : ℝ

The plus exponent ψ₊(s)=φ₊(s)-log r(s+1).

Equations

• Section10Lemma1028PlusAssembly.psiPlus r ξ c s = Section10Lemma1028PlusAssembly.phiPlus ξ c s - Real.log (r (s + 1))

noncomputable def Section10Lemma1028PlusAssembly.envelopePlus (R ξ : ℝ → ℝ) (c s : ℝ) : ℝ

Suzuki's weighted plus envelope.

Equations

• Section10Lemma1028PlusAssembly.envelopePlus R ξ c s = R s * Real.exp (Section10Lemma1028PlusAssembly.phiPlus ξ c s)

noncomputable def Section10Lemma1028PlusAssembly.logEnvelopePlus (R ξ : ℝ → ℝ) (c s : ℝ) : ℝ

Its logarithm, used to state the first-crossing history.

Equations

• Section10Lemma1028PlusAssembly.logEnvelopePlus R ξ c s = Real.log (R s) + Section10Lemma1028.xiPhase ξ s + c * s

@[simp]

theorem Section10Lemma1028PlusAssembly.exp_neg_psiPlus {r ξ : ℝ → ℝ} {c t : ℝ} (hr : 0 < r (t + 1)) : Real.exp (-psiPlus r ξ c t) = r (t + 1) * Real.exp (-phiPlus ξ c t)

theorem Section10Lemma1028PlusAssembly.logEnvelopePlus_hasDerivAt {R ξ : ℝ → ℝ} (hξ : Section10Lemma1028.Proposition1020Xi ξ) {c s : ℝ} (hs : 0 < s) (hR : 0 < R s) (hDDE : HasDerivAt R (-(2 * R s + R (s - 1)) / s) s) : HasDerivAt (logEnvelopePlus R ξ c) (-R (s - 1) / (s * R s) + ξ s + c - 2 / s) s

Direct plus version of (10.44).

structure Section10Lemma1028PlusAssembly.PlusFirstCrossing (R ξ : ℝ → ℝ) (c β s₀ : ℝ) : Type

A genuine plus first crossing: the logarithmic slope starts positive and s is the first point after s₀ at which it is nonpositive.

• s : ℝ
• slope : ℝ → ℝ
• beta_lt_s₀ : β < s₀
• s₀_lt_s : s₀ < self.s
• beta_add_one_le_s : β + 1 ≤ self.s
• slope_continuousOn : ContinuousOn self.slope (Set.Ioc β self.s)
• logEnvelope_continuousOn : ContinuousOn (logEnvelopePlus R ξ c) (Set.Icc β self.s)
• hasDeriv (u : ℝ) : u ∈ Set.Ioc β self.s → HasDerivAt (logEnvelopePlus R ξ c) (self.slope u) u
• initial_pos (u : ℝ) : u ∈ Set.Icc β s₀ → 0 < self.slope u
• before_crossing_pos (u : ℝ) : s₀ < u → u < self.s → 0 < self.slope u
• crossing_nonpos : self.slope self.s ≤ 0

theorem Section10Lemma1028PlusAssembly.PlusFirstCrossing.slope_pos_before {R ξ : ℝ → ℝ} {c β s₀ : ℝ} (w : PlusFirstCrossing R ξ c β s₀) {u : ℝ} (hβu : β ≤ u) (hus : u < w.s) : 0 < w.slope u

theorem Section10Lemma1028PlusAssembly.PlusFirstCrossing.isLeast_nonpositive {R ξ : ℝ → ℝ} {c β s₀ : ℝ} (w : PlusFirstCrossing R ξ c β s₀) : IsLeast {u : ℝ | s₀ ≤ u ∧ w.slope u ≤ 0} w.s

The witness really records the least point in the closed nonpositive set.

theorem Section10Lemma1028PlusAssembly.PlusFirstCrossing.slope_at_crossing_eq_zero {R ξ : ℝ → ℝ} {c β s₀ : ℝ} (w : PlusFirstCrossing R ξ c β s₀) : w.slope w.s = 0

Continuity turns the weak sign at the first point into stationarity.

theorem Section10Lemma1028PlusAssembly.PlusFirstCrossing.stationary {R ξ : ℝ → ℝ} {c β s₀ : ℝ} (w : PlusFirstCrossing R ξ c β s₀) : HasDerivAt (logEnvelopePlus R ξ c) 0 w.s

theorem Section10Lemma1028PlusAssembly.PlusFirstCrossing.stationary_equation {R ξ : ℝ → ℝ} {c β s₀ : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hξ : Section10Lemma1028.Proposition1020Xi ξ) (w : PlusFirstCrossing R ξ c β s₀) : ξ w.s + c - 2 / w.s = R (w.s - 1) / (w.s * R w.s)

At the plus crossing, (10.44) is exactly (10.45) with the plus sign.

theorem Section10Lemma1028PlusAssembly.PlusFirstCrossing.log_monotoneOn {R ξ : ℝ → ℝ} {c β s₀ : ℝ} (w : PlusFirstCrossing R ξ c β s₀) : MonotoneOn (logEnvelopePlus R ξ c) (Set.Icc β w.s)

Before the first nonpositive crossing, log W₊ is monotone.

theorem Section10Lemma1028PlusAssembly.envelopePlus_eq_exp_logEnvelopePlus_of_pos {R ξ : ℝ → ℝ} {c t : ℝ} (hRt : 0 < R t) : envelopePlus R ξ c t = Real.exp (logEnvelopePlus R ξ c t)

theorem Section10Lemma1028PlusAssembly.PlusFirstCrossing.envelope_monotoneOn {R ξ : ℝ → ℝ} {c β s₀ : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (w : PlusFirstCrossing R ξ c β s₀) : MonotoneOn (envelopePlus R ξ c) (Set.Icc β w.s)

theorem Section10Lemma1028PlusAssembly.PlusFirstCrossing.window_order {R ξ : ℝ → ℝ} {c β s₀ : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (w : PlusFirstCrossing R ξ c β s₀) {t : ℝ} (ht : t ∈ Set.Icc (w.s - 1) w.s) : envelopePlus R ξ c (w.s - 1) ≤ envelopePlus R ξ c t ∧ envelopePlus R ξ c t ≤ envelopePlus R ξ c w.s

Correct plus window order: W₊(s) ≥ W₊(t) ≥ W₊(s-1).

theorem Section10Lemma1028PlusAssembly.plus_pairing_weighted_identity {R ξ : ℝ → ℝ} {β c s : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hadj : h.adjoint = Section10Equation1053NonCircular.explicitKappaOneAdjointPlus) (hβs : β < s) (hs2 : 2 ≤ s) : s * Section10Equation1053NonCircular.explicitKappaOneAdjointPlus s * R s = ∫ (t : ℝ) in s - 1..s, envelopePlus R ξ c t * Real.exp (-psiPlus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus ξ c t)

Pairing-zero rewritten directly in plus variables.

theorem Section10Lemma1028PlusAssembly.plus_pairing_ge_leftEndpoint_kernel {R ξ : ℝ → ℝ} {c β s₀ : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hadj : h.adjoint = Section10Equation1053NonCircular.explicitKappaOneAdjointPlus) (w : PlusFirstCrossing R ξ c β s₀) (hs2 : 2 ≤ w.s) (hprodInt : IntervalIntegrable (fun (t : ℝ) => envelopePlus R ξ c t * Real.exp (-psiPlus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus ξ c t)) MeasureTheory.volume (w.s - 1) w.s) (hkernelInt : IntervalIntegrable (fun (t : ℝ) => Real.exp (-psiPlus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus ξ c t)) MeasureTheory.volume (w.s - 1) w.s) : envelopePlus R ξ c (w.s - 1) * ∫ (t : ℝ) in w.s - 1..w.s, Real.exp (-psiPlus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus ξ c t) ≤ w.s * Section10Equation1053NonCircular.explicitKappaOneAdjointPlus w.s * R w.s

Equation (10.54): increasing plus history gives a lower pairing bound.

noncomputable def Section10Lemma1028PlusAssembly.plusPairingScalarRatio (ξ : ℝ → ℝ) (c s : ℝ) : ℝ

The scalar expression on the right of source (10.55).

Equations

• Section10Lemma1028PlusAssembly.plusPairingScalarRatio ξ c s = ((ξ s + c - 2 / s) * ∫ (t : ℝ) in s - 1..s, Real.exp (-Section10Lemma1028PlusAssembly.psiPlus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus ξ c t)) / Real.exp (-Section10Lemma1028PlusAssembly.psiPlus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus ξ c (s - 1))

def Section10Lemma1028PlusAssembly.PlusPairingScalarInequality (ξ : ℝ → ℝ) (c s : ℝ) : Prop

The strict scalar conclusion of (10.55), separated from the topological and pairing argument rather than hidden in a final exclusion field.

Equations

• Section10Lemma1028PlusAssembly.PlusPairingScalarInequality ξ c s = (1 < Section10Lemma1028PlusAssembly.plusPairingScalarRatio ξ c s)

theorem Section10Lemma1028PlusAssembly.plusFirstCrossing_scalarRatio_le_one {R : ℝ → ℝ} {β c s₀ : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hadj : h.adjoint = Section10Equation1053NonCircular.explicitKappaOneAdjointPlus) (w : PlusFirstCrossing R Section10CanonicalXi.xi c β s₀) : plusPairingScalarRatio Section10CanonicalXi.xi c w.s ≤ 1

Equations (10.54)--(10.55), lower half: pairing and stationarity force the plus scalar ratio to be at most one.

def Section10Lemma1028PlusAssembly.ProducesPlusFirstCrossing (R : ℝ → ℝ) (β c S : ℝ) : Prop

Source-facing producer of a genuine plus first crossing. It is a theorem premise about the least crossing, not an arbitrary-stationary exclusion.

Equations

• Section10Lemma1028PlusAssembly.ProducesPlusFirstCrossing R β c S = ∀ (v : ℝ), S ≤ v → Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi v + c ≤ 0 → ∃ (w : Section10Lemma1028PlusAssembly.PlusFirstCrossing R Section10CanonicalXi.xi c β S), S ≤ w.s

theorem Section10Lemma1028PlusAssembly.normalizedMinusBase_continuousAt {R : ℝ → ℝ} {β s : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hβs : β < s) : ContinuousAt (Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi) s

Continuity of the normalized slope on the full legal half-line, including β; only differentiability uses the open left endpoint.

theorem Section10Lemma1028PlusAssembly.plusFirstCrossing_of_reaches {R : ℝ → ℝ} {β c S v : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hβS : β < S) (hβoneS : β + 1 ≤ S) (hinitial : ∀ u ∈ Set.Icc β S, 0 < Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi u + c) (hSv : S ≤ v) (hv : Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi v + c ≤ 0) : ∃ (w : PlusFirstCrossing R Section10CanonicalXi.xi c β S), S ≤ w.s

Compactness constructs the least plus crossing. No derivative at the apparatus endpoint β is requested.

theorem Section10Lemma1028PlusAssembly.producesPlusFirstCrossing {R : ℝ → ℝ} {β c S : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hβS : β < S) (hβoneS : β + 1 ≤ S) (hinitial : ∀ u ∈ Set.Icc β S, 0 < Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi u + c) : ProducesPlusFirstCrossing R β c S

The topological producer, now proved rather than assumed.

structure Section10Lemma1028PlusAssembly.Section10PlusCommonMajorant (R : ℝ → ℝ) : Type

Plus half of the common-majorant conclusion. This is an output type; no input apparatus contains the final slope conclusion.

• cPlus : ℝ
• cutoff : ℝ
• one_le_cPlus : 1 ≤ self.cPlus
• four_le_cutoff : 4 ≤ self.cutoff
• envelope_slope_nonneg (s : ℝ) : self.cutoff ≤ s → 0 ≤ -R (s - 1) + s * (Section10CanonicalXi.xi s + self.cPlus - 2 / s) * R s

Source-faithful stationary closure of the plus case of (10.55)

plusPairingScalarRatio above is the exact ratio before the source expansion. It was previously called equation1055PlusScalarRatio; that attribution is withdrawn: the printed (10.55) contains the positive λ / (s A) prefactor. The definitions below record that prefactor literally and use the expansion only at stationary candidates, exactly as in the source proof.

noncomputable def Section10Equation1055UniformStationary.equation1055PlusDenominator (lam c s : ℝ) : ℝ

The denominator A = ξ(s) + c - λ/s in the first factor of (10.55).

Equations

• Section10Equation1055UniformStationary.equation1055PlusDenominator lam c s = Section10CanonicalXi.xi s + c - lam / s

noncomputable def Section10Equation1055UniformStationary.equation1055PlusExponentialTerm (lam c s : ℝ) : ℝ

The exponentially small negative term displayed in the plus case of (10.55).

Equations

• Section10Equation1055UniformStationary.equation1055PlusExponentialTerm lam c s = lam * Real.exp (-c / 2) / (s * Section10CanonicalXi.xi s)

noncomputable def Section10Equation1055UniformStationary.equation1055PlusScalarRatio (lam c s remainder : ℝ) : ℝ

The literal two-factor scalar on the right of source (10.55). In particular, its positive correction is λ / (s A), not merely 1/A.

Equations

• Section10Equation1055UniformStationary.equation1055PlusScalarRatio lam c s remainder = (1 + lam / (s * Section10Equation1055UniformStationary.equation1055PlusDenominator lam c s)) * (1 - Section10Equation1055UniformStationary.equation1055PlusExponentialTerm lam c s + remainder)

structure Section10Equation1055UniformStationary.PlusStationaryCandidate (R : ℝ → ℝ) (c S₀ : ℝ) : Type

A candidate is required to be stationary and to lie beyond the fixed source cutoff S₀; no unconditional assertion over all points at infinity is used.

• s : ℝ
• cutoff_le : S₀ ≤ self.s
• stationary : Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi self.s + c = 0

structure Section10Equation1055UniformStationary.Equation1055StationarySource (R : ℝ → ℝ) (β S₀ : ℝ) : Type

The source inputs used after (10.45)--(10.46). The fields are the stationary expansion (10.55), its two quantitative remainder estimates, and a bounded fixed initial segment. There is deliberately no final strict inequality and no first-crossing producer field.

• lam : ℝ
• C : ℝ
• remainder : ℝ → ℝ → ℝ
• lambda_pos : 0 < self.lam
• one_le_C : 1 ≤ self.C
• cutoff_pos : 0 < S₀
• initial_bounded : ∃ (B : ℝ), ∀ u ∈ Set.Icc β S₀, -Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi u ≤ B
• denominator_pos (c : ℝ) : self.C ≤ c → ∀ (w : PlusStationaryCandidate R c S₀), 0 < equation1055PlusDenominator self.lam c w.s
• correction_lt_one (c : ℝ) : self.C ≤ c → ∀ (w : PlusStationaryCandidate R c S₀), self.lam / (w.s * equation1055PlusDenominator self.lam c w.s) < 1
• exponential_dominated (c : ℝ) : self.C ≤ c → ∀ (w : PlusStationaryCandidate R c S₀), equation1055PlusExponentialTerm self.lam c w.s ≤ 1 / 4 * (self.lam / (w.s * equation1055PlusDenominator self.lam c w.s))
• remainder_control (c : ℝ) : self.C ≤ c → ∀ (w : PlusStationaryCandidate R c S₀), |self.remainder c w.s| ≤ 1 / 4 * (self.lam / (w.s * equation1055PlusDenominator self.lam c w.s))
• expansion (c : ℝ) : self.C ≤ c → ∀ (w : PlusStationaryCandidate R c S₀), Section10Lemma1028PlusAssembly.plusPairingScalarRatio Section10CanonicalXi.xi c w.s = equation1055PlusScalarRatio self.lam c w.s (self.remainder c w.s)

theorem Section10Equation1055UniformStationary.equation1055_strict_at_stationary {R : ℝ → ℝ} {β S₀ c : ℝ} (src : Equation1055StationarySource R β S₀) (hc : src.C ≤ c) (w : PlusStationaryCandidate R c S₀) : 1 < Section10Lemma1028PlusAssembly.plusPairingScalarRatio Section10CanonicalXi.xi c w.s

The source (10.55) scalar is strictly greater than one at every stationary candidate, uniformly for all c ≥ C. The positive λ/(sA) correction absorbs both the exponentially small term and the signed remainder.

theorem Section10Equation1055UniformStationary.equation1055_uniform_stationary {R : ℝ → ℝ} {β S₀ : ℝ} (src : Equation1055StationarySource R β S₀) (c : ℝ) : src.C ≤ c → ∀ (w : PlusStationaryCandidate R c S₀), 1 < Section10Lemma1028PlusAssembly.plusPairingScalarRatio Section10CanonicalXi.xi c w.s

Uniform stationary formulation: for the fixed S₀, every c beyond the single source threshold excludes every stationary candidate by strict (10.55).

noncomputable def Section10Equation1055UniformStationary.section10_plus_commonMajorant_of_stationary_source {R : ℝ → ℝ} {β S₀ : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hadj : h.adjoint = Section10Equation1053NonCircular.explicitKappaOneAdjointPlus) (hβ : β ≤ 3) (hβS : β < S₀) (hβoneS : β + 1 ≤ S₀) (src : Equation1055StationarySource R β S₀) : Section10Lemma1028PlusAssembly.Section10PlusCommonMajorant R

Plus common majorant with both former residual premises removed. The already-proved topological producer is invoked internally, and strict (10.55) is needed only for the stationary crossing it produces.

Equations

• Section10Equation1055UniformStationary.section10_plus_commonMajorant_of_stationary_source h hadj hβ hβS hβoneS src = { cPlus := max src.C (max 1 (Classical.choose ⋯ + 1)), cutoff := 4, one_le_cPlus := ⋯, four_le_cutoff := Section10Equation1055UniformStationary.section10_plus_commonMajorant_of_stationary_source._proof_9, envelope_slope_nonneg := ⋯ }