Reference · Matrices

rainbow.math.linear.matrix.affine-nnrat-exact-rate-null

Matricessrc/rainbow/math/linear/matrix/affine_nnrat_exact_rate_null.clj0 definitions, 5 theorems

Null-sequence bridges for exact NNRAT contraction envelopes. For nonnegative values, `gamma^n value` is monotone in gamma. Therefore an exact envelope with gamma <= 1/2 is pointwise below the established half-power envelope and inherits its identity-modulus signed rate-null certificate. Exact paired-trajectory and successive-residual bounds can then be promoted directly to rate-null results without discarding the sharper finite-horizon estimates. Native, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-nnrat-exact-rate

signed/nnrat-power-scale-rate-monotone :
  (gamma delta : ℚ≥0)
  (gamma-at-most-delta : gamma ≤ delta)
  (value : ℚ)
  (value-nonnegative : 0 ≤ value)
  (steps : ℕ)
  → signed/nnrat-power-scale gamma steps value ≤ signed/nnrat-power-scale delta steps value

signed/nnrat-power-scale-at-most-half-power :
  (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (value : ℚ)
  (value-nonnegative : 0 ≤ value)
  (steps : ℕ)
  → signed/nnrat-power-scale gamma steps value ≤ signed/half-power-scale steps value

analysis/signed-nnrat-power-rate-null-of-at-most-half :
  (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (value : ℚ)
  (value-nonnegative : 0 ≤ value)
  (value-at-most-one : value ≤ 1)
  → analysis/signed-rate-null (fun n => signed/nnrat-power-scale gamma n value) (fun k => k)

matrix/affine-nnrat-iterate-sup-distance-rate-null-exact-envelope :
  (rows : List (List ℚ)) (offset left right : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (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 gamma)
  (initial-distance-at-most-one : vector/sup-distance left right ≤ 1)
  → analysis/signed-rate-null (fun n => vector/sup-distance (matrix/affine-iterate rows offset n left) (matrix/affine-iterate rows offset n right)) (fun k => k)

matrix/affine-nnrat-successive-residual-rate-null-exact-envelope :
  (rows : List (List ℚ)) (offset initial : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (step-shape : vector/same-shape initial (action))
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows initial))
  (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 gamma)
  (initial-residual-at-most-one : vector/sup-distance initial (action) ≤ 1)
  → analysis/signed-rate-null (fun n => vector/sup-distance (matrix/affine-iterate rows offset n initial) (matrix/affine-iterate rows offset (data/succ n) initial)) (fun k => k)
  where action := matrix/affine-action rows offset initial