Source-correct minus first crossing and window order for (10.53)

Unlike the withdrawn right-endpoint-maximum model, the source chooses the first point where (log W₋)' becomes nonnegative. The resulting history makes W₋ antitone up to the crossing. Thus the upper endpoint consumed by the pairing integral is the left endpoint s - 1, not s.

structure Section10Equation1053MinusFirstCrossing.MinusFirstCrossing (R ξ : ℝ → ℝ) (c β s₀ : ℝ) : Type

Source-facing data for the first minus crossing. slope is the actual logarithmic derivative. The first two sign fields say it is negative on the initial interval and remains negative after s₀ until the least crossing s; crossing_nonneg records membership of s in the closed failure set.

• s : ℝ
• slope : ℝ → ℝ
• beta_lt_s₀ : β < s₀
• s₀_lt_s : s₀ < self.s
• beta_add_one_le_s : β + 1 ≤ self.s
• slope_continuousAt : ContinuousAt self.slope self.s
• log_continuousOn : ContinuousOn (Section10Lemma1028.logEnvelopeMinus R ξ c) (Set.Icc β self.s)
• hasDeriv (u : ℝ) : u ∈ Set.Ioc β self.s → HasDerivAt (Section10Lemma1028.logEnvelopeMinus R ξ c) (self.slope u) u
• initial_neg (u : ℝ) : u ∈ Set.Icc β s₀ → self.slope u < 0
• before_crossing_neg (u : ℝ) : s₀ < u → u < self.s → self.slope u < 0
• crossing_nonneg : 0 ≤ self.slope self.s

theorem Section10Equation1053MinusFirstCrossing.MinusFirstCrossing.slope_neg_before {R ξ : ℝ → ℝ} {c β s₀ : ℝ} (w : MinusFirstCrossing R ξ c β s₀) {u : ℝ} (hβu : β ≤ u) (hus : u < w.s) : w.slope u < 0

theorem Section10Equation1053MinusFirstCrossing.MinusFirstCrossing.isLeast_nonnegative {R ξ : ℝ → ℝ} {c β s₀ : ℝ} (w : MinusFirstCrossing R ξ c β s₀) : IsLeast {u : ℝ | s₀ ≤ u ∧ 0 ≤ w.slope u} w.s

s really is the least point at or after s₀ where the logarithmic derivative is nonnegative.

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

Continuity of the logarithmic derivative turns the weak sign at the least crossing into equality.

theorem Section10Equation1053MinusFirstCrossing.MinusFirstCrossing.stationary {R ξ : ℝ → ℝ} {c β s₀ : ℝ} (w : MinusFirstCrossing R ξ c β s₀) : HasDerivAt (Section10Lemma1028.logEnvelopeMinus R ξ c) 0 w.s

The least crossing is a stationary point of log W₋.

theorem Section10Equation1053MinusFirstCrossing.MinusFirstCrossing.normalizedMinusBase_eq {R ξ : ℝ → ℝ} {c β s₀ : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hξ : Section10Lemma1028.Proposition1020Xi ξ) (w : MinusFirstCrossing R ξ c β s₀) : Section10Lemma1028FirstCrossing.normalizedMinusBase R ξ w.s = c

In the specialized a=2,b=1 DDE, the stationary conclusion is exactly Suzuki's algebraic stationary equation.

theorem Section10Equation1053MinusFirstCrossing.MinusFirstCrossing.log_antitoneOn {R ξ : ℝ → ℝ} {c β s₀ : ℝ} (w : MinusFirstCrossing R ξ c β s₀) : AntitoneOn (Section10Lemma1028.logEnvelopeMinus R ξ c) (Set.Icc β w.s)

First-crossing history forces log W₋ to decrease on the complete prefix.

theorem Section10Equation1053MinusFirstCrossing.envelopeMinus_eq_exp_logEnvelopeMinus_of_pos {R ξ : ℝ → ℝ} {c t : ℝ} (hRt : 0 < R t) : Section10Equation1053.envelopeMinus R ξ c t = Real.exp (Section10Lemma1028.logEnvelopeMinus R ξ c t)

theorem Section10Equation1053MinusFirstCrossing.MinusFirstCrossing.envelope_antitoneOn {R ξ : ℝ → ℝ} {c β s₀ : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (w : MinusFirstCrossing R ξ c β s₀) : AntitoneOn (Section10Equation1053.envelopeMinus R ξ c) (Set.Icc β w.s)

Since the exponential is increasing, the logarithmic first-crossing history makes the weighted envelope itself antitone on [β,s].

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

The source's full minus-window order: W₋(s-1) ≥ W₋(t) ≥ W₋(s) for t ∈ [s-1,s].

theorem Section10Equation1053MinusFirstCrossing.pairing_le_leftEndpoint_kernel {R ξ : ℝ → ℝ} {c β s₀ : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hadj : h.adjoint = Section10Equation1053NonCircular.explicitKappaOneAdjointPlus) (w : MinusFirstCrossing R ξ c β s₀) (hs2 : 2 ≤ w.s) (hprodInt : IntervalIntegrable (fun (t : ℝ) => Section10Equation1053.envelopeMinus R ξ c t * Real.exp (-Section10Equation1053.psiMinus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus ξ c t)) MeasureTheory.volume (w.s - 1) w.s) (hkernelInt : IntervalIntegrable (fun (t : ℝ) => Real.exp (-Section10Equation1053.psiMinus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus ξ c t)) MeasureTheory.volume (w.s - 1) w.s) : w.s * Section10Equation1053NonCircular.explicitKappaOneAdjointPlus w.s * R w.s ≤ Section10Equation1053.envelopeMinus R ξ c (w.s - 1) * ∫ (t : ℝ) in w.s - 1..w.s, Real.exp (-Section10Equation1053.psiMinus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus ξ c t)

Source-correct pairing comparison. The upper bound is W₋(s-1). Using W₋(s) here would reverse the first inequality in window_order.