Verify positive definiteness using random numbers

Question

I wish to verify whether T'T - IdentityMatrix[2] is always positive definite for a certain choice of elements of T'T.

T'T = {{t11^2, t11*t12},{t11*t12, t12^2+t22^2}};

Now, I have written the following program to check my assumptions on t11 etc which are: t11^2 > 1 t22^2 > 1 and t12 completely free.

co = 0;
Do[{t11s = RandomReal[{1, 10^12}], 
  If[RandomReal[{0, 1}] >= 0.5, t11 = Sqrt[t11s], t11 = -Sqrt[t11s]],
        t22s = RandomReal[{1, 10^12}], 
  If[RandomReal[{0, 1}] >= 0.5, t22 = Sqrt[t22s], t22 = -Sqrt[t22s]],
        t12 = RandomReal[{-10^12, 10^12}], 
  ttm = {{t11s, t11*t12}, {t11*t12, t12^2 + t22s}},
  If[Transpose[ve].(ttm-IdentityMatrix[2]).ve > 0, co++]}, {10^5}]
co

However, my program, based on random draws, generates odd results. For fixed ve as well as for random draws.

Thank you so much!

Answer 1

The eigenvalues are

Eigenvalues[{{t11^2, t11*t12}, {t11*t12, t12^2 + t22^2}} - IdentityMatrix[2]]

giving

{1/2 (-2 + t11^2 + t12^2 + t22^2 - Sqrt[ t11^4 + 2 t11^2 t12^2 + t12^4 - 2 t11^2 t22^2 + 2 t12^2 t22^2 + t22^4]), 1/2 (-2 + t11^2 + t12^2 + t22^2 + Sqrt[ t11^4 + 2 t11^2 t12^2 + t12^4 - 2 t11^2 t22^2 + 2 t12^2 t22^2 + t22^4])}

Assuming that the radicand is real-valued, one then notes that positive-definiteness is equivalent to

(-2 + t11^2 + t12^2 + t22^2)^2 > 
 t11^4 + 2 t11^2 t12^2 + t12^4 - 2 t11^2 t22^2 + 2 t12^2 t22^2 + t22^4

which simplifies to

$$1 + t11^2 (-1 + t22^2) > t12^2 + t22^2$$

which can be false when t12 becomes arbitrarily large. Thus the matrix is not always positive definite; Daniel Lichtblau's answer shows a way to construct explicit counterexamples.

Answer 2

Could look for a counterexample using FindInstance.

tmat = {{t11^2, t11*t12}, {t11*t12, t12^2 + t22^2}} - 
   IdentityMatrix[2];
evals = Eigenvalues[tmat];

FindInstance[(evals[[1]] <= 0 || evals[[2]] <= 0) && 
  t11^2 >= 1 && t22^2 >= 1, Variables[tmat], Reals]

(* Out[237]= {{t11 -> Sqrt[2], t12 -> 1, t22 -> Sqrt[3/2]}} *)

To get conditions on positive definiteness one could use Reduce with a setup similar to that above.