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

noncomputable def AVenhance.lIdx (β : ℝ) (Λ m : ℕ) (k : ℤ) : ℤ

e.lk.def (1173-1177): l_k := ⌈(k τ_m + (τ''_m - τ_m)/2) / τ''_m⌉, k ∈ ℤ.

Equations

• AVenhance.lIdx β Λ m k = ⌊(↑k * AVenhance.tau β Λ m + 1 / 2 * (AVenhance.tauPP β Λ m - AVenhance.tau β Λ m)) / AVenhance.tauPP β Λ m⌋