Statement file: kappaAt (Section3). This file contains exactly one declaration of the formalization's public statement surface.

def AVenhance.Ingredients.kappaAt {β : ℝ} (I : Ingredients β) (κ : ℝ) : ℕ → ℕ → ℝ

e.kappa.sequence (label 3533). kappaAt I κ m d is κ_m for the chain topped at M = m + d (so κ_M = κ, κ_{m-1} = KBar_m^{κ_m}): κ_m = kappaAt I κ m (M - m), m ≤ M.

Equations

• I.kappaAt κ x✝ 0 = κ
• I.kappaAt κ x✝ d.succ = I.KhomScalar (I.kappaAt κ (x✝ + 1) d) (x✝ + 1)