A positive auxiliary diffusivity sequence for the §3.3 recurrence.

def AVenhance.Infra.Section3.kappaPrimeAt (β : ℝ) (Λ : ℕ) (κ : ℝ) : ℕ → ℕ → ℝ

The auxiliary sequence κ' from e.kappa.prime.sequence, indexed by its current scale and the distance from its terminal value.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section3.kappaPrimeAt β Λ κ x✝ 0 = κ

theorem AVenhance.Infra.Section3.kappaPrimeAt_pos {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {κ : ℝ} (hκ : 0 < κ) (m d : ℕ) : 0 < kappaPrimeAt β Λ κ m d