pith. machine review for the scientific record. sign in
structure definition def or abbrev

LocalBinaryRecurrence

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 162structure LocalBinaryRecurrence where
 163  ladder : UniformScaleLadder
 164  coeff_a : ℕ
 165  coeff_b : ℕ
 166  coeff_a_pos : 1 ≤ coeff_a
 167  coeff_b_pos : 1 ≤ coeff_b
 168  local_recurrence :
 169    ladder.levels 2 = (coeff_a : ℝ) * ladder.levels 1 +
 170      (coeff_b : ℝ) * ladder.levels 0
 171
 172/-- The zero-parameter posture requires minimal descriptional complexity
 173for the recurrence coefficients. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.