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.

In this post we have an inequality in 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. 

So there is something fundamentally different about this task. 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.

Two things are worth noting about this proof.

First, we probably didn't think too deeply about the step from $a\geq2$ to $a^{2}\geq(2)^{2}$. Without going all the way back to the axioms, we can justify it by the commonly accepted result that if $m\leq n$, then $m^{i}\leq n^{i}$. Here $m,n,i\in\mathbb{N}$.

Second, 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

There's nothing structually different about this proof. The second hypothesis, the proof objective, and one of the lines in the proof body now use an inequality ≥ rather than an equality =.

What is new is the rel tactic, which is used to justify statements about relations, such as “greater than or equal to” $\geq$ . Here the rel tactic is combining a^2 and the hypothesis a ≥ 2 to give a^2 ≥ (2)^2. 


Looking Inside The rel Tactic

The rel tactic is using a lemma about natural numbers from the Lean maths library, Nat.pow_le_pow_left, which encodes the idea that $n\leq m\implies n^{i}\leq m^{i}$, where $m,n,i\in\mathbb{N}$. 

Recall our discussion in the first chapter that a large body of fundamental results have been encoded into the Lean Mathlib library. Larger results are called theorems, and smaller results are called lemmas.

It is interesting to see how this lemma is declared in the Mathlib library.


abbrev Nat.pow_le_pow_left {n : Nat}  {m : Nat}  (h : n ≤ m)  (i : Nat) :
    n ^ i ≤ m ^ i

Even with our nascent familiarity with Lean code, we can recognise the key elements. The start looks like the name of the lemma. The variables m and n are declared as natural numbers. The hypothesis for this lemma is n ≤ m, and the conclusion is n^i ≤ m^i.


Easy Exercise

Write a Lean program to prove $a<c$ if we know $a<b$ and $b\leq c$, where $a,b,c\in\mathbb{N}$. 


at