Monday, July 8, 2024

05 - Inequalities

In the first post, we only used inequalities at the final step of each proof, to establish $4>1$ and $4<10$. These were simple numerical comparisons.

Here we have inequalities as the hypotheses of the theorem we want to prove. 


Task

Given the facts

$$\begin{align}b & = a^{2} \\ a & \geq 2 \end{align}$$

our task is to show

$$b\geq4$$

where $a$ and $b$ are natural numbers.


Maths

Let's pause and consider what's different about this task compared to the first chapter. 

Here the conclusion holds for any $a \geq 2$. In the first chapter a was very specifically constrained to $a=4$. So this theorem is much broader in scope. 

The first post's proof concluded with $4>1$, justified by a simple numerical comparison. We can't do that here because $b$ in $b \geq 4$ could be any one of an infinity of natural numbers. 

Let's write out a proof.

$$\begin{align} b&=a^{2}&&\text{given fact}\tag{1}\label{5.1}\\a&\geq2&&\text{given fact}\tag{2}\label{5.2}\\&&&\\b&=a^{2}&&\text{using fact }(\ref{5.1})\\&\geq(2)^{2}&&\text{using fact }(\ref{5.2})\\&=4&&\text{using arithmetic}\tag*{\(\Box\)} \end{align}$$

Let's break it down:

  • We first list the given facts, $b=a^{2}$ and $a\geq2$.
  • We start with the expression we want to prove something about, $b$. We say this is $a^{2}$ justified by the first given fact.
  • Our aim is to express $b$ as a comparison to $4$, so we want to resolve $a$.
  • The second fact $a\geq2$ gives us $a^{2}\geq(2)^{2}$.
  • Finally, we say $(2)^{2}=4$, giving us the desired conclusion.

It is easy to misread the proof as stating $b=4$. The correct reading is that $b=a^{2}$, and $a^{2}\geq(2)^{2}$, and finally $(2)^{2}=4$. We can tie this chain of inequalities together, and summarise them as $b\geq4$. 


Code

The following Lean program proves $b\geq4$ given $b=a^{2}$ and $a\geq2$.


-- 05 - Simple Inequality

import Mathlib.Tactic

example {a b : ℕ} (h1 : b = a^2) (h2: a ≥ 2) : b ≥ 4 := by
  calc
    b = a^2 := by rw [h1]
    _ ≥ (2)^2 := by rel [h2]
    _ = 4 := by norm_num

The second hypothesis, the proof objective, and one of the lines in the proof body uses an inequality ≥ rather than an equality =. Aside from that, there's nothing structurally different about this proof. 

The rel tactic is new. It is used to justify statements about relations, such as “greater than or equal to”. 

Here the rel tactic is combining a^2 and the hypothesis a ≥ 2 to give a^2 ≥ (2)^2. 


Easy Exercise

Write a Lean program to prove $a<c$ if we know $a<b$ and $b\leq c$, where $a$, $b$ and $c$ are natural numbers.


at