# Re: [isabelle] Matrix-Vector operation

• To: isabelle-users <isabelle-users at cl.cam.ac.uk>
• Subject: Re: [isabelle] Matrix-Vector operation
• From: Fabian Immler <immler at in.tum.de>
• Date: Mon, 26 Feb 2018 09:02:40 +0100
• Cc: Omar Jasim <oajasim1 at sheffield.ac.uk>
• References: <CAAi=gesys_f_DXD2k=+t-jCXpCqA2OR_ZYq9Hvs48bpHWJkwaA@mail.gmail.com>

```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

```

Attachment: smime.p7s
Description: S/MIME cryptographic signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.