[isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

[Lawrence Paulson]

Is there a case for moving some material from this file into the Analysis directory?

https://www.isa-afp.org/browser_info/current/AFP/Perron_Frobenius/HMA_Connect.html <https://www.isa-afp.org/browser_info/current/AFP/Perron_Frobenius/HMA_Connect.html>

Many of the results proved at the end of this file are quite straightforward anyway. As somebody with a lifting-and-transfer phobia, I don't feel qualified to make this decision. Possibly these techniques are overkill. I have already proved some of these results quite straightforwardly using linearity, and installed them not long ago.

Larry

> Begin forwarded message:
> 
> From: Fabian Immler <immler at in.tum.de>
> Subject: Re: [isabelle] Matrix-Vector operation
> Date: 26 February 2018 at 08:02:40 GMT
> To: isabelle-users <isabelle-users at cl.cam.ac.uk>
> Cc: Omar Jasim <oajasim1 at sheffield.ac.uk>
> 
> Dear Omar,
> 
> Unfortunately, there are no lemmas on distributivity of *v in the distribution.
> Some are currently in the AFP-entry Perron_Frobenius:
> https://www.isa-afp.org/browser_info/current/AFP/Perron_Frobenius/HMA_Connect.html
> 
> You can prove them (in HOL-Analysis) as follows:
> 
> lemma matrix_diff_vect_distrib: "(A - B) *v v = A *v v - B *v (v :: 'a :: ring_1 ^ 'n)"
>  unfolding matrix_vector_mult_def
>  by vector (simp add: sum_subtractf left_diff_distrib)
> 
> lemma matrix_add_vect_distrib: "(A + B) *v v = A *v v + B *v v"
>  unfolding matrix_vector_mult_def
>  by vector (simp add: sum.distrib distrib_right)
> 
> lemma matrix_vector_right_distrib: "M *v (v + w) = M *v v + M *v w"
>  unfolding matrix_vector_mult_def
>  by vector (simp add: sum.distrib distrib_left)
> 
> lemma matrix_vector_right_distrib_diff: "(M :: 'a :: ring_1 ^ 'nr ^ 'nc) *v (v - w) = M *v v - M *v w"
>  unfolding matrix_vector_mult_def
>  by vector (simp add: sum_subtractf right_diff_distrib)
> 
> Those should probably be included in the next Isabelle release.
> 
> Hope this helps,
> Fabian
> 
> 
>> Am 25.02.2018 um 19:27 schrieb Omar Jasim <oajasim1 at sheffield.ac.uk>:
>> 
>> Hi,
>> 
>> This may be trivial but I have a difficulty proving the following lemma:
>> 
>> lemma
>> fixes  A :: "real^3^3"
>>   and x::"real^3"
>> assumes "A>0"
>> shows " (A *v x) - (mat 1 *v x)  = (A - mat 1) *v x "
>> 
>> where A is a positive definite diagonal matrix. Is there a lemma predefined
>> related to this?
>> 
>> Cheers
>> Omar
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180226/8c29bf54/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180226/8c29bf54/attachment.asc>