Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-signed-operator-fixed-point-convergence

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_signed_operator_fixed_point_convergence.clj0 definitions, 4 theorems

Fixed-point convergence of the low-arity signed operator iterator. Any pointwise two-sided additively contractive operator transports closeness to an assumed fixed point. Structural induction gives the exact recursive error radius for every finite iterate; the existing general harmonic theorem then packages a rate-null convergence certificate for every canonical positive rational discount (a+1)/(a+g+2). No fixed point is constructed. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.bellman-signed-transition-operator

value/signed-operator-iterate-zero.{u} :
  (S : Type u) (operator : (S → ℚ) → S → ℚ) (initial : S → ℚ)
  → value/signed-operator-iterate S operator 0 initial = initial

value/signed-contractive-operator-fixed-point-additive-advance.{u} :
  (S : Type u) (operator : (S → ℚ) → S → ℚ) (discount : ℚ) (fixed-value : S → ℚ)
  (fixed-point : ∀ (state : S), operator fixed-value state = fixed-value state)
  (candidate : S → ℚ) (epsilon : ℚ)
  (candidate-close : ∀ (state : S), proposition/conjunction (candidate state ≤ fixed-value state + epsilon) (fixed-value state ≤ candidate state + epsilon))
  (advance : ∀ (left : S → ℚ), ∀ (right : S → ℚ), ∀ (radius : ℚ), ∀ (close : ∀ (state : S), proposition/conjunction (left state ≤ right state + radius) (right state ≤ left state + radius)), ∀ (state : S), proposition/conjunction (operator left state ≤ operator right state + discount · radius) (operator right state ≤ operator left state + discount · radius))
  (state : S)
  → proposition/conjunction (operator candidate state ≤ fixed-value state + discount · epsilon) (fixed-value state ≤ operator candidate state + discount · epsilon)

value/signed-contractive-operator-iterate-fixed-point-additive-radius.{u} :
  (S : Type u) (operator : (S → ℚ) → S → ℚ) (discount : ℚ) (fixed-value : S → ℚ)
  (fixed-point : ∀ (state : S), operator fixed-value state = fixed-value state)
  (initial : S → ℚ) (initial-error : ℚ)
  (initial-close : ∀ (state : S), proposition/conjunction (initial state ≤ fixed-value state + initial-error) (fixed-value state ≤ initial state + initial-error))
  (advance : ∀ (left : S → ℚ), ∀ (right : S → ℚ), ∀ (epsilon : ℚ), ∀ (close : ∀ (state : S), proposition/conjunction (left state ≤ right state + epsilon) (right state ≤ left state + epsilon)), ∀ (state : S), proposition/conjunction (operator left state ≤ operator right state + discount · epsilon) (operator right state ≤ operator left state + discount · epsilon))
  (steps : ℕ) (state : S)
  → proposition/conjunction (iterate ≤ fixed-value state + radius) (fixed-value state ≤ iterate + radius)
  where iterate := value/signed-operator-iterate S operator steps initial state
  where radius := value/signed-vi-error-radius discount initial-error steps

value/signed-contractive-operator-iterate-fixed-point-converges-general-rate.{u} :
  (ap gp : ℕ) (S : Type u) (operator : (S → ℚ) → S → ℚ) (fixed-value : S → ℚ)
  (fixed-point : ∀ (state : S), operator fixed-value state = fixed-value state)
  (initial : S → ℚ) (initial-error : ℚ)
  (initial-error-nonnegative : 0 ≤ initial-error)
  (initial-bound : initial-error ≤ signed/from-nnrat (nnrat/general-harmonic ap gp 0))
  (initial-close : ∀ (state : S), proposition/conjunction (initial state ≤ fixed-value state + initial-error) (fixed-value state ≤ initial state + initial-error))
  (advance : ∀ (left : S → ℚ), ∀ (right : S → ℚ), ∀ (epsilon : ℚ), ∀ (close : ∀ (state : S), proposition/conjunction (left state ≤ right state + epsilon) (right state ≤ left state + epsilon)), ∀ (state : S), proposition/conjunction (operator left state ≤ operator right state + signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) · epsilon) (operator right state ≤ operator left state + signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) · epsilon))
  → proposition/conjunction (null) (∀ (steps : ℕ), ∀ (state : S), proposition/conjunction ((fun steps₁ => iterate steps₁ initial) steps state ≤ fixed-value state + (fun steps₁ => value/signed-vi-error-radius (signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp)))) initial-error steps₁) steps) (fixed-value state ≤ (fun steps₁ => iterate steps₁ initial) steps state + (fun steps₁ => value/signed-vi-error-radius (signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp)))) initial-error steps₁) steps))
  where iterate := value/signed-operator-iterate S operator
  where null := analysis/signed-rate-null (fun steps => value/signed-vi-error-radius (signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp)))) initial-error steps) (fun index => nat/multiply (data/succ ap) index)