Conditional comparison of the diffusivity chain with its auxiliary κ′ chain. The explicit one-step relative error is kept as a hypothesis; the cutoff averaging estimate that supplies it is a separate analytic task.

def AVenhance.Infra.Section3.kappaAtPrimeErrorEnvelope (η : ℕ → ℝ) : ℕ → ℕ → ℝ

The product loss in comparing recurrences with relative one-step errors.

Equations

• AVenhance.Infra.Section3.kappaAtPrimeErrorEnvelope η x✝ 0 = 1
• AVenhance.Infra.Section3.kappaAtPrimeErrorEnvelope η x✝ d.succ = (1 - η (x✝ + 1))⁻¹ * AVenhance.Infra.Section3.kappaAtPrimeErrorEnvelope η (x✝ + 1) d

theorem AVenhance.Infra.Section3.positive_recurrence_ratio_step {u v B η x R : ℝ} (hu : 0 < u) (hv : 0 < v) (hB : 0 < B) (hη0 : 0 ≤ η) (hη1 : η < 1) (hR : 0 < R) (hruLo : 1 / R ≤ u / v) (hruHi : u / v ≤ R) (hrvHi : v / u ≤ R) (hstep : |x - (u + B / u)| ≤ η * (B / u)) : max (x / (v + B / v)) ((v + B / v) / x) ≤ R / (1 - η)

Stability of one positive recurrence step under a relative increment error.

theorem AVenhance.Infra.Section3.KappaPrimeComparison.kappaAtPrimeErrorEnvelope_pos (η : ℕ → ℝ) (hη : ∀ (j : ℕ), 1 ≤ j → η j < 1) (m d : ℕ) : 0 < kappaAtPrimeErrorEnvelope η m d