### Nuprl Lemma : linearization-value

`∀[L:ℤ List List]. ∀[p:iPolynomial()].`
`  ∀f:ℤ ⟶ ℤ`
`    (int_term_value(f;ipolynomial-term(p))`
`    = linearization(p;L) ⋅ map(λvs.accumulate (with value x and list item v):`
`                                    x * (f v)`
`                                   over list:`
`                                     vs`
`                                   with starting value:`
`                                    1);L)`
`    ∈ ℤ) `
`  supposing (∀m∈p.(snd(m) ∈ L)) ∧ no_repeats(ℤ List;L)`

Proof

Definitions occuring in Statement :  linearization: `linearization(p;L)` ipolynomial-term: `ipolynomial-term(p)` iPolynomial: `iPolynomial()` int_term_value: `int_term_value(f;t)` integer-dot-product: `as ⋅ bs` l_all: `(∀x∈L.P[x])` no_repeats: `no_repeats(T;l)` l_member: `(x ∈ l)` map: `map(f;as)` list_accum: list_accum list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` pi2: `snd(t)` all: `∀x:A. B[x]` and: `P ∧ Q` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` multiply: `n * m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` guard: `{T}` uimplies: `b supposing a` prop: `ℙ` or: `P ∨ Q` top: `Top` cons: `[a / b]` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` not: `¬A` colength: `colength(L)` nil: `[]` it: `⋅` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sq_type: `SQType(T)` less_than: `a < b` squash: `↓T` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` sq_stable: `SqStable(P)` subtract: `n - m` subtype_rel: `A ⊆r B` iPolynomial: `iPolynomial()` linearization: `linearization(p;L)` ipolynomial-term: `ipolynomial-term(p)` int_term_value: `int_term_value(f;t)` ifthenelse: `if b then t else f fi ` btrue: `tt` itermConstant: `"const"` int_term_ind: int_term_ind iMonomial: `iMonomial()` pi2: `snd(t)` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` bool: `𝔹` unit: `Unit` bfalse: `ff` exists: `∃x:A. B[x]` bnot: `¬bb` assert: `↑b` bor: `p ∨bq` deq: `EqDecider(T)` int_nzero: `ℤ-o` istype: `istype(T)` select: `L[n]` int_seg: `{i..j-}` lelt: `i ≤ j < k` poly-coeff-of: `poly-coeff-of(vs;p)` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` nat_plus: `ℕ+` decidable: `Dec(P)` l_all: `(∀x∈L.P[x])` imonomial-less: `imonomial-less(m1;m2)` imonomial-term: `imonomial-term(m)` cand: `A c∧ B` nequal: `a ≠ b ∈ T ` list_ind: list_ind imonomial-le: `imonomial-le(m1;m2)` l_member: `(x ∈ l)`
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction thin Error :lambdaFormation_alt,  extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis setElimination rename intWeakElimination natural_numberEquality independent_isectElimination independent_functionElimination voidElimination Error :universeIsType,  sqequalRule Error :lambdaEquality_alt,  dependent_functionElimination Error :isect_memberEquality_alt,  axiomEquality Error :functionIsTypeImplies,  Error :inhabitedIsType,  intEquality equalityTransitivity equalitySymmetry unionElimination Error :functionIsType,  because_Cache promote_hyp hypothesis_subsumption productElimination Error :equalityIsType1,  Error :dependent_set_memberEquality_alt,  independent_pairFormation instantiate cumulativity imageElimination imageMemberEquality baseClosed applyLambdaEquality applyEquality minusEquality Error :equalityIsType4,  addEquality functionExtensionality Error :setIsType,  multiplyEquality universeEquality equalityElimination Error :dependent_pairFormation_alt,  independent_pairEquality setEquality sqequalIntensionalEquality Error :productIsType,  hyp_replacement productEquality

Latex:
\mforall{}[L:\mBbbZ{}  List  List].  \mforall{}[p:iPolynomial()].
\mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
(int\_term\_value(f;ipolynomial-term(p))
=  linearization(p;L)  \mcdot{}  map(\mlambda{}vs.accumulate  (with  value  x  and  list  item  v):
x  *  (f  v)
over  list:
vs
with  starting  value:
1);L))
supposing  (\mforall{}m\mmember{}p.(snd(m)  \mmember{}  L))  \mwedge{}  no\_repeats(\mBbbZ{}  List;L)

Date html generated: 2019_06_20-PM-00_47_26
Last ObjectModification: 2018_10_04-PM-02_39_59

Theory : omega

Home Index