Using numbers, real numbers, in Lean

Having a calculation with real numbers in Lean is not as straightforward as it seems. I’m sure I’ll learn better ways to do it in the future, but for now, I want to share how I solved this problem.

As part of the formalization project I’m working on, I had to prove the following theorem:

The length function \(l\) of a code \(C: A \mapsto B^*\) satisfies: \(\sum_{a \in A} 2^{l(C(a))} \leq \log_2 |A|\)

When the code function satisfies the Kraft inequality, we can upper-bound the right-hand side by 1, but this is more general.

As part of the proof, we need to show that for any integer \(m \geq 1\), the inequality \(2^{-(m+1)} \leq \log_2(2 - 2^{-m})\) holds.

This can be proved by showing the inequality holds for \(m = 1\), that is, that \(\frac{1}{4} \leq \log_2\Bigl(\frac{3}{2}\Bigr).\)

My first attempt was to use norm_num to compute the logarithm, but it didn’t work as expected. The problem is that norm_num does not handle logarithms directly.
Instead, I had to transform the inequality into an equivalent comparison between rational numbers:

This final inequality can be proved by norm_num since it’s just a rational number comparison.

import Mathlib
open Real

notation "log₂" => logb 2

example : 4⁻¹ ≤ log₂ (3/2) := by
  have h : (0 : ℝ) < 4 := by norm_num
  have h' : (0 : ℝ) < 3/2 := by norm_num
  rw [← mul_le_mul_left h]
  simp
  show 1 ≤ 4 * log₂ (3/2)
  rw [← logb_rpow_eq_mul_logb_of_pos h']
  show 1 ≤ log₂ ((3/2) ^ 4)
  rw [le_logb_iff_rpow_le (by norm_num) (by norm_num)]
  show 2 ^ 1 ≤ (3/2) ^ 4
  norm_num

This is a side of formalization that feels more fragile than I expected, and I wonder if I’ll run into more situations like this in the future. I promise to update this post if I find a better way to do it.