*To*: Fabian Immler <immler at in.tum.de>*Subject*: Re: [isabelle] Matrix-Vector operation*From*: Omar Jasim <oajasim1 at sheffield.ac.uk>*Date*: Mon, 26 Feb 2018 11:40:21 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <C945C068-3512-467B-9A07-E0E815911E74@in.tum.de>*References*: <CAAi=gesys_f_DXD2k=+t-jCXpCqA2OR_ZYq9Hvs48bpHWJkwaA@mail.gmail.com> <C945C068-3512-467B-9A07-E0E815911E74@in.tum.de>

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

**Follow-Ups**:**Re: [isabelle] Matrix-Vector operation***From:*Lawrence Paulson

**References**:**[isabelle] Matrix-Vector operation***From:*Omar Jasim

**Re: [isabelle] Matrix-Vector operation***From:*Fabian Immler

- Previous by Date: Re: [isabelle] Matrix-Vector operation
- Next by Date: Re: [isabelle] Matrix-Vector operation
- Previous by Thread: Re: [isabelle] Matrix-Vector operation
- Next by Thread: Re: [isabelle] Matrix-Vector operation
- Cl-isabelle-users February 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list