# Re: [isabelle] Matrix-Vector operation

```I believe also this lemma doesn't exist:

lemma
fixes y :: "real^3"
and X :: "real^3^3"
shows "norm(X *v y) ≤ norm (X) * norm (y)"

Omar Jasim
PhD Student
Automatic Control and Systems Engineering - ACSE
University of Sheffield
UK

On 26 February 2018 at 11:49, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> I have recently been adding some results involving matrices to the
> repository and they will be available in the next release.
> Larry Paulson
>
>
>
> > On 26 Feb 2018, at 11:40, Omar Jasim <oajasim1 at sheffield.ac.uk> wrote:
> >
> > Dear Fabian,
> >
> > That's obvious now. I thought I couldn't find them. Many thanks for
> sending
> > these through. I also realized that I  previously proved one of them as
> > below:
> >
> > lemma mat_vec_add_dis:  "A *v g + B *v g = (A + B) *v g"
> >  apply (vector  matrix_vector_mult_def)
> >  apply (smt Cartesian_Euclidean_Space.sum_cong_aux distrib_right
> > sum.distrib)
> >  done
> >
> > Thanks
> > Omar
> >
> > On 26 February 2018 at 08:02, Fabian Immler <immler at in.tum.de> wrote:
> >
> >> 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
> >>
> >>
>
>

```

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