Re: Struggling to prove simple triangle inequality

*To*: mathgroup at smc.vnet.net*Subject*: [mg126331] Re: Struggling to prove simple triangle inequality*From*: Vladimir M <vladimir7523 at gmail.com>*Date*: Tue, 1 May 2012 14:57:32 -0400 (EDT)*Delivered-to*: l-mathgroup@mail-archive0.wolfram.com*References*: <201204300842.EAA23670@smc.vnet.net> <jnoa64$54o$1@smc.vnet.net>

On May 1, 12:25 pm, Andrzej Kozlowski <akozlow... at gmail.com> wrote: > > Given two 3D vectors A and B, I want to prove that length of their sum > > is less or equal than the sum of their lengths: > > > length[v_] := Sqrt[v.v]; > > a = {ax, ay, az}; > > b = {bx, by, bz}; > > inequality = length[a + b] <= length[a] + length[b]; > > > vars = {ax, ay, az, bx, by, bz}; > > Reduce[inequality, vars, Reals] > > Not really. To solve this sort of problem Reduce uses the algorithm > called cylindrical algebraic decomposition, which is implemented in > Mathematica as CylindricalDecomposition. This algorithm's complexity is > double exponential (i.e. 2^n^n where n is the number of variables.). Thanks for explanation. Meanwhile, Reduce has run for a few days at 3 GHz, taking gigabytes of memory and finally crashed the kernel. Looks like besides checking many combinations, a huge memory is needed for something (list-based methods instead of iteration-based?) Anyway, if not Reduce, maybe something else could help to automatically prove this seemingly simple problem? -- All the best, Vladimir