Reference · Matrices

rainbow.math.linear.matrix.affine-half-iterate-rate

Matricessrc/rainbow/math/linear/matrix/affine_half_iterate_rate.clj1 definitions, 5 theorems

Finite-horizon geometric rate for half-row signed affine iteration. `signed/half-power-scale n d` is the native recurrence d, (1/2)d, (1/2)((1/2)d), ... . Its zero/successor equations, nonnegativity, and monotonicity are proof data. Induction over the one-step affine contraction then gives the explicit all-horizon bound sup-distance(F^n x, F^n y) <= half-power-scale n (sup-distance x y). Native, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-half-iterate-contraction

signed/half-power-scale :
  (x₁ : ℕ) (x₂ : ℚ)
  → ℚ

signed/half-power-scale-zero :
  (value : ℚ)
  → signed/half-power-scale 0 value = value

signed/half-power-scale-successor :
  (steps : ℕ) (value : ℚ)
  → signed/half-power-scale (data/succ steps) value = signed/from-nnrat nnrat/half · signed/half-power-scale steps value

signed/half-power-scale-nonnegative :
  (value : ℚ)
  (value-nonnegative : 0 ≤ value)
  (steps : ℕ)
  → 0 ≤ signed/half-power-scale steps value

signed/half-power-scale-monotone :
  (left right : ℚ)
  (ordered : left ≤ right)
  (steps : ℕ)
  → signed/half-power-scale steps left ≤ signed/half-power-scale steps right

matrix/affine-half-iterate-sup-distance-rate :
  (rows : List (List ℚ)) (offset left right : List ℚ)
  (initial-shape : vector/same-shape left right)
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows left))
  (positive-rows : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/at-most (vector/zero-like row) row)
  (bounded-sums : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/sum row ≤ signed/from-nnrat nnrat/half)
  (steps : ℕ)
  → vector/sup-distance (iterate₁) (iterate) ≤ signed/half-power-scale steps (vector/sup-distance left right)
  where iterate := matrix/affine-iterate rows offset steps right
  where iterate₁ := matrix/affine-iterate rows offset steps left