If I understand correctly, your LMP is the dot product. In that case, a
simple counter-example to your goal: [1,1] * [-1,1] = 0
On Fri, Mar 22, 2013 at 4:46 AM, Yuntao Peng <[email protected]>wrote:
> I want to prove a property of linear space. Property description as
> follows:
>
> If exist unique β, and β = p1α1+p2α2+…+pnαn , then α1,α2, … , αn linearly
> independent.
>
> Where β, α1,α2, … , αn are the elements of linearly space, and p1,p2, …
> , pn are complex.
>
>
>
> Derivation：
>
> β = p1α1+p2α2+…+pnαn (1)
>
> 0 = k1α1+k2α2+…+knαn (2)
>
> (1)+ (2) ==> β = p1α1+p2α2+…+pnαn = (k1+p1)α1+(k2+p2)α2+…+(kn+pn)αn
>
> ==> k1=0, k2=0,…, kn=0 ==> α1,α2, … , αn linearly independent
>
>
>
>
>
> Now, I have proved a goal, and save it as a theorem.
>
> g `!k:complex x:'a. (k LM x = ls0) /\ (x <> ls0) ==> (k = 0)`
>
> Where “LM” is multiplication sign of linear space, “ls0” is zero of linear
> space.
>
> My question is how to prove the goal as follows?
>
> g `!l1:complex list l2:'a list. (LENGTH l1 = LENGTH l2) /\ (LMP(l1,l2) =
> ls0) /\ (EVERY P l2) ==> (EVERY Q l1)`;
>
> Where“LN” is plus of linear space.
>
> val ls_mult_add = Define
>
>
> `(LMP ([],l2:'a list) = ls0) /\
>
> (LMP ((h1::t1):complex list,l2:'a list) = if (l2 = []) then ls0
>
> else (h1 LM HD l2)
> LP (LMP (t1,TL l2)))`;
>
> if l1=(p1,p2,…,pn), l2=(α1,α2,…,αn) , then LMP(l1,l2) = p1α1+p2α2+…+pnαn
>
> val Q_def = Define `!x:complex. Q x = (x = 0c)`;
>
> val P_def = Define `!x:'a. P x = (x <> ls0)`;
>
>
>
>
>
> I am looking forward your advice.
>
> Thanks.
> Peng.
>
> ------------------------------------------------------------------------------
> Everyone hates slow websites. So do we.
> Make your web apps faster with AppDynamics
> Download AppDynamics Lite for free today:
> http://p.sf.net/sfu/appdyn_d2d_mar
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_d2d_mar
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
