Re: Struggling to prove simple triangle inequality

*To*: mathgroup at smc.vnet.net*Subject*: [mg126327] Re: Struggling to prove simple triangle inequality*From*: Andrzej Kozlowski <akozlowski at gmail.com>*Date*: Tue, 1 May 2012 05:23:29 -0400 (EDT)*Delivered-to*: l-mathgroup@mail-archive0.wolfram.com*References*: <201204300842.EAA23670@smc.vnet.net>

On 30 Apr 2012, at 10:42, Vladimir M wrote: > Greetings! > > 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]; > > This is famous, well-known and quite obvious: triangle side is shorter > than the sum of other sides, straight line is shorter than non- > straight, etc. However, proving it formally is hard. > > This fails: > > assum = Element[ax | ay | az | bx | by | bz, Reals]; > FullSimplify[inequality, assum] > > > This takes ages on a high-end PC with unknown result: > > vars = {ax, ay, az, bx, by, bz}; > Reduce[inequality, vars, Reals] > > Anyone can help? I think Reduce should somehow make it because it > actually succeeds at least with 2D vectors. > > > -- > All the best, > Vladimir > 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.). So the fact that it works in a reasonable time for 4 variables (two dimensional case) is not a good reason to expect it will work for 6 variables (three dimensional case), e.g. see here http://en.wikipedia.org/wiki/Double_exponential_function Andrzej Kozlowski