The famous CS inequality states

$$ \left| \left< x , y \right>\right| \le \left\| x \right\| \cdot \left\| y \right\| $$

for $x,y$ in an inner product space $X$ over $\mathbb{K}$. Every proof I found involves some kind of case distinction; namely one may use w.l.o.g $\Vert x \Vert, \Vert y \Vert > 0$ since the inequality is trivial otherwise. However, I was looking for a constructive proof (i.e. without using the law of excluded middle) for the inequality.

I will add some remarks to the question.

1) Law of excluded middle: This axiom states that $A \vee \neg A$ is true. This is not considered an axiom in constructive mathematics. One might interpret this in the following way: Indirect proofs are not allowed. However, I find this not completely accurate. Precisely the implication $A \rightarrow \neg \neg A$ is true in constructive mathematics; the implication $ \neg \neg A \rightarrow A$ not in gerneral.

2) The definition of an inner product is the same as in "classical" mathematics.

3) The norm $\Vert \cdot \Vert$ is given by $\Vert x \Vert = \sqrt{\langle x, x\rangle }$.

  • 1
    $\begingroup$ What do you mean by 'constructive' here? Cauchy-Schwarz doesn't assert the existence of anything, so there's nothing to construct. $\endgroup$ – dbx Sep 4 '18 at 18:22
  • $\begingroup$ It's actually for $x,y$ in an inner product space. $\endgroup$ – zhw. Sep 4 '18 at 18:42
  • $\begingroup$ I feel a bit sorry for Diamir. Every time Diamir posts a question to constructive-mathematics, someone either gives a non-constructive proof or asks what "constructive" means despite Diamir asking for a constructive proof in the title, body, and via tags and explicitly specifying what "constructive" means in this case. On the other hand, Diamir's questions are often ambiguous since they don't provide definitions for the concepts being used. Since classically equivalent definitions are not necessarily constructively equivalent, this really matters. $\endgroup$ – Derek Elkins Sep 4 '18 at 20:31
  • 1
    $\begingroup$ @Diamir Your question isn't unclear (to me) because of your definition of "constructive". Short of specifying a specific constructive logic, I'm really not sure what more you could do to communicate what you mean by "constructive". People seem to consistently ignore either that you said "constructive" at all or that you and the tag give a definition of "constructive". The unclarity is that traditional definitions of particular concepts, e.g. the real numbers, are often bad or ambiguous definitions constructively, e.g. Dedekind reals and Cauchy reals are not the same thing constructively. $\endgroup$ – Derek Elkins Sep 5 '18 at 18:42
  • 1
    $\begingroup$ @Diamir Here's an idea that I just thought of that might help. Maybe say something like "a proof in intuitionistic logic" rather than "a constructive proof". Sure, someone might think you intend to allow some of the anti-classical axioms of Intuitionism, but at least that person would be somewhat knowledgeable about non-classical logics and would understand if you clarified that you wanted to restrict to Bishop-style constructivism. $\endgroup$ – Derek Elkins Sep 5 '18 at 18:42

The following is well known. Let $a,b$ be scalars. Then in the given Hilbert space, with the given notations: $$ \begin{aligned} 0 &\le \|ax+by\|^2 \\ &=\langle ax+by, ax+by\rangle \\ & = \langle ax, ax\rangle +\langle ax, by\rangle +\langle by, ay\rangle +\langle by, by\rangle \\ & =a^2\|x\|^2 + 2a\text{Real}(b\langle x, y\rangle) + |b|^2\|y\|^2 \ . \end{aligned} $$ Now we make the choice $b=c\langle y,x\rangle=c \overline{\langle x, y\rangle}$, $c$ real.

The above is then a quadratic form in $a,c\in\Bbb R$: $$ (a,c)\to a^2\|x\|^2 + 2ac|\langle x, y\rangle|^2 + c^2|\langle x, y\rangle|^2\|y\|^2\ . $$ (Later edit, it is above correctly $\|y\|^2$, not $\|by\|^2$ as survived till i put the glasses.)

It is possibly semidefinite, but it is non-negative. A necessary condition for this is the one on its discriminant: $$ |\langle x, y\rangle|^4-|\langle x, y\rangle|^2\;\|x\|^2\;\|y\|^2 \le 0\ , $$ which is equivalent to CS. This proof (or versions of it) hides in the used results the case chase ramification (condition of having the one or the other coefficient not equal zero), but i think this can be done. (It is not a "constructive proof", only one that avoids studying cases.) For instance, if from the last inequality above we do not "see" the CS inequality without case separation, than take above instead of $b=c\langle y,x\rangle$ a corresponding $b=c\; e^{-i\phi}$ where $\phi$ is the argument of $\langle y,x\rangle$. (Well, if not zero, if zero take anything. You see here why cases make such proofs simpler, at least simpler to write, when one of the cases can be called trivial. But, OK, a proof "in a breath" was wanted!)

  • $\begingroup$ Why is the last inequality equivalent to CS? For the equivalence you need $\vert \langle x , y \rangle \vert > 0$ in my opinion. $\endgroup$ – user397268 Sep 5 '18 at 10:42
  • $\begingroup$ If the scalar product of $x$ and $y$ is zero, then CS is obviously satisfied.(Well, in the solution it is not allowed to separate cases, but question on this separation are allowed. How can i answer such questions without going into cases?) $\endgroup$ – dan_fulea Sep 6 '18 at 4:58
  • $\begingroup$ Well, thats what my question is about. I wonder wether one can show CS without this case distinction. $\endgroup$ – user397268 Sep 6 '18 at 13:23
  • $\begingroup$ So we need a proof for [ Let $a,B\in\Bbb R$, with $B\ge 0$, then $a^2(a^2-B)\le 0$ implies $a^2-B\le 0$ ] only? Ok, here is one without cases. Assume the contrary, namely $a^2-B>0$. Then we have $a^2\le 0$, we also have $-B\le 0$ (given), add and get $a^2-B\le 0$, contradiction. The assumption is false... $\endgroup$ – dan_fulea Sep 6 '18 at 21:14
  • 1
    $\begingroup$ @Diamir The quadratic form takes only values $\ge 0$ because - with the introduced notations - we have in one breath $$0\le \|ax+by\|^2= a^2\|x\|^2 + 2a\text{Real}(b\langle x, y\rangle) + |b|^2\|y\|^2=a^2\|x\|^2 + 2ac|\langle x, y\rangle|^2 + c^2|\langle x, y\rangle|^2\|y\|^2\ .$$ (A copy+paste typo was also corrected in the initial post.) $\endgroup$ – dan_fulea Sep 17 '18 at 16:15

Here is a proof from Pugh, Real Mathematical Analysis. I don't know if this proof can be modified for a complex vector space, but in case you're working over $\Bbb{R}$ it may be what you're looking for.

Let $x$ and $y$ be arbitrary and let $w = x + ty$ for a scalar $t$. Define $Q(t) = \langle w, w \rangle=\langle x + ty, x + ty \rangle$.

Then $Q(t)$ is nonnegative, being the value of an inner product. By the bilinearity of $\langle \cdot, \cdot \rangle$, we have: $$ Q(t) = \langle x,x\rangle + 2t\langle x,y \rangle + t^2\langle y,y\rangle = c + bt + at^2$$

Interpret $Q$ as a parabola; since it is nonnegative its discriminant $b^2 - 4ac$ must be nonpositive (else there would be two real roots, thus a segment of the parabola below the real axis). This gives: $$ 4\langle x,y\rangle^2-4\langle x, x\rangle \langle y,y\rangle \leq 0,$$ or rewriting: $$ \langle x,y \rangle^2 \leq \langle x,x\rangle \langle y,y \rangle. $$ Taking the square root of both sides gives the result.

  • $\begingroup$ Just to be super-picky: when you say "interpret $Q$ as a parabola" you are assuming $\langle y,y\rangle\neq 0$. Well, unless you allow degenerate parabolas but then you shouldn't mention two roots later and it is just moving the dreaded "case distinction" elsewhere. Just saying... :)) $\endgroup$ – Michal Adamaszek Sep 4 '18 at 18:37
  • $\begingroup$ Yes, I suppose that's true. Pugh completely ignores the possibility; in the case that $\langle y,y\rangle=0$, then actually $y=0$ so $Q$ is a constant function. Is this what the original question is trying to avoid, then? $\endgroup$ – dbx Sep 4 '18 at 18:42
  • $\begingroup$ I'm not sure. It is a bit of an academic discussion. $\endgroup$ – Michal Adamaszek Sep 4 '18 at 19:13
  • $\begingroup$ This case distinction is unfortunately not allowed. This would only work when one allows the law of excluded middle. $\endgroup$ – user397268 Sep 5 '18 at 10:44

Breaking into cases doesn't necessarily rely on the law of excluded middle. It is true in a Hilbert space that either $x = 0$ or $x \neq 0$, we don't need to appeal to excluded middle for this fact. This constructively/intuitionistically reduces the problem to finding a proof for both the case $x=0$ and the case $x \neq 0$.

In other words, I agree that a case analysis uses excluded middle in some sense, but if you can constructively prove excluded middle for the cases you are considering, then you don't need to assume it in general.

  • $\begingroup$ Wikipedia seems to suggest that according to the 'intuitionist' (constructivist) point of view, one cannot accept the assertion that every element in an inner product space is either zero or nonzero, if said space is infinite. But what the heck else could it be?? $\endgroup$ – dbx Sep 4 '18 at 19:23
  • $\begingroup$ @dbx The point is that in constructive mathematics saying $P\lor Q$ means you have a witness for $P$ or you have a witness for $Q$ and you know which you have. At an intuitive level, if someone gives me a real number which I think might be $0$, I can never convince myself of it. No matter how many digits I check, it could always be the case that a non-$0$ digit could occur. Of course, if I know how that number was produced, I might be able to convince myself that it must produce $0$. $\endgroup$ – Derek Elkins Sep 4 '18 at 20:19
  • $\begingroup$ @dbx More formally, for any Turing machine it is easy to make a real number that is $0$ if and only if the Turing machine halts. Therefore, being able to know whether or not a real number is $0$ is equivalent to being able to solve the Halting Problem. It is compatible with constructive logic to assume that all witnesses are computable, so $\forall x\in\mathbb R.x=0\lor\neg(x=0)$ has no witness since it would be uncomputable. For other, anti-classical systems such as synthetic differential geometry, there really is "extra" stuff. In SDG, $\{x\in\mathbb R\mid x^2=0\}$ is distinct from $\{0\}$. $\endgroup$ – Derek Elkins Sep 4 '18 at 20:19
  • $\begingroup$ Thanks for the details. I'm hesitant to continue the discussion, because I think that's not what comments are for. But I would point out that in this case our setting is an arbitrary Hilbert space rather than $\Bbb{R}$. I think that once we accept the abstraction of working in a general space, practical considerations such as decimal expansions go by the wayside, and an insistence on particular witnesses seems contradictory. $\endgroup$ – dbx Sep 4 '18 at 23:19
  • $\begingroup$ @dbx I was simply providing examples of how its possible for $\forall x.x=0\lor x\neq 0$ can fail constructively. That said, if the theorem fails for a particular example, it's certainly not going to provable in general. $\endgroup$ – Derek Elkins Sep 5 '18 at 0:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy