Nuprl Lemma : weighted-sum-split
∀[p,q:ℚ List]. ∀[F:ℕ||p @ q|| ─→ ℚ].
(weighted-sum(p @ q;F) = (weighted-sum(p;F) + weighted-sum(q;λi.(F (i + ||p||)))) ∈ ℚ)
Proof
Definitions occuring in Statement :
weighted-sum: weighted-sum(p;F),
length: ||as||,
append: as @ bs,
list: T List,
int_seg: {i..j-},
uall: ∀[x:A]. B[x],
apply: f a,
lambda: λx.A[x],
function: x:A ─→ B[x],
add: n + m,
natural_number: $n,
equal: s = t ∈ T,
qadd: r + s,
rationals: ℚ
Lemmas :
length-append,
Error :sum_split_q,
length_wf,
non_neg_length,
length_wf_nat,
qmul_wf,
length_append,
subtype_rel_list,
top_wf,
lelt_wf,
select_wf,
int_seg_wf,
qadd_wf,
squash_wf,
true_wf,
rationals_wf,
Error :qsum_wf,
select_append_front,
sq_stable__le,
iff_weakening_equal,
equal_wf,
append_wf,
list_wf,
Error :sum_shift_q,
select_append_back,
subtract_wf,
add-associates,
minus-one-mul,
add-commutes,
add-mul-special,
zero-mul,
add-zero
\mforall{}[p,q:\mBbbQ{} List]. \mforall{}[F:\mBbbN{}||p @ q|| {}\mrightarrow{} \mBbbQ{}].
(weighted-sum(p @ q;F) = (weighted-sum(p;F) + weighted-sum(q;\mlambda{}i.(F (i + ||p||)))))
Date html generated:
2015_07_17-AM-07_58_14
Last ObjectModification:
2015_02_03-PM-09_44_22
Home
Index