prefixEval append
ProvedFreiman.prefixEval_appendcontinued-fractionshall-raynumber-theory
The prefix map of a concatenation of two finite words is the composition of their prefix maps, for every real tail parameter.
Preamble
import Definitions.Def_Freiman_prefixEval
Formal statement
namespace Freiman
theorem prefixEval_append (w v : List ℕ+) (x : ℝ) :
prefixEval (w ++ v) x = prefixEval w (prefixEval v x) := by
sorry
end FreimanSource
Freiman's Hall ray: Proof report and corrected English text, 8 September 2026, §1.1, printed p.7, definition of the finite prefix map T_w and its composition order.