Reference · Matrices

rainbow.math.linear.matrix.affine-approximate-fixed-point

Matricessrc/rainbow/math/linear/matrix/affine_approximate_fixed_point.clj0 definitions, 4 theorems

Constructive approximate fixed points from affine residual convergence. Exact signed-rational affine contraction need not be accompanied by a supplied fixed point. The exact-envelope residual-null theorem nevertheless produces an explicit approximate one: at every reciprocal tolerance index k, the kth iterate has residual at most `from-nnrat(harmonic k)`, and every later iterate satisfies the same bound. The existential theorem packages that iterate as proof data rather than merely asserting asymptotic behavior. Native, kernel-checked, and axiom-free on D63.

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

analysis/signed-rate-null-at-modulus :
  (sequence : ℕ → ℚ) (modulus : ℕ → ℕ)
  (null : analysis/signed-rate-null sequence modulus) (index : ℕ)
  → proposition/conjunction (0 ≤ sequence (modulus index)) (sequence (modulus index) ≤ signed/from-nnrat (nnrat/harmonic index))

matrix/affine-nnrat-eventually-approximate-fixed-point :
  (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)
  (index steps : ℕ)
  (large-enough : index ≤ steps)
  → vector/sup-distance (matrix/affine-iterate rows offset steps initial) (action) ≤ signed/from-nnrat (nnrat/harmonic index)
  where action := matrix/affine-action rows offset (matrix/affine-iterate rows offset steps initial)
  where action₁ := matrix/affine-action rows offset initial

matrix/affine-nnrat-approximate-fixed-point-at-horizon :
  (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)
  (index : ℕ)
  → vector/sup-distance (matrix/affine-iterate rows offset index initial) (action) ≤ signed/from-nnrat (nnrat/harmonic index)
  where action := matrix/affine-action rows offset (matrix/affine-iterate rows offset index initial)
  where action₁ := matrix/affine-action rows offset initial

matrix/affine-nnrat-approximate-fixed-point-exists :
  (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)
  (index : ℕ)
  → proposition/existence (List ℚ) (fun approximate => vector/sup-distance approximate (matrix/affine-action rows offset approximate) ≤ signed/from-nnrat (nnrat/harmonic index))
  where action := matrix/affine-action rows offset initial