Rational powers

Lean’s core library has no support for rational or real numbers 😦

They are however in the maths library — or we can just make some fake real numbers and use them instead.


-- let's define the real numbers to be a number system which satisfies
-- the basic properties of the real numbers which we will need.

noncomputable theory
constant real : Type
@[instance] constant real_field : linear_ordered_field real

-- This piece of magic means that "real" now behaves a lot like
-- the real numbers. In particular we now have a bunch
-- of theorems:

example : ∀ x y : real, x * y = y * x := mul_comm

#check mul_assoc


At Imperial I’ve just been talking to the 1st years about taking a rational power of a positive real number. I guess we could set all this up in Lean.


open nat

definition natural_power : real → nat → real
| x 0 := 1
| x (n+1) := (natural_power x n) * x

theorem power_comm : ∀ x:real, ∀ m n:nat, natural_power x (m+n) = natural_power x m *natural_power x n :=
begin
admit
end


That’s a definition (by recursion) of for real and a non-negative integer. It’s also a theorem which needs proving. We can prove that theorem by induction, I suspect. I’ll try it later on.

But what I really want is a rational power. We’re going to need existence of positive th roots.


constant nth_root (x : real) (n : nat) : (x>0) → (n>0) → real

axiom is_nth_root (x : real) (n : nat) (Hx : x>0) (Hn : n>0) : natural_power (nth_root x n Hx Hn) n = x


Now we can consider trying to define rational powers!


constant nth_root (x : real) (n : nat) : (x>0) → (n>0) → real

axiom is_nth_root (x : real) (n : nat) (Hx : x>0) (Hn : n>0) : natural_power (nth_root x n Hx Hn) n = x

definition rational_power_v0 (x : real) (n : nat) (d : nat) (Hx : x > 0) (Hd : d > 0) : real :=
natural_power (nth_root x d Hx Hd) n


This code is now up on xena’s github:

link to rational power stuff

Let’s see what we can do with it!

Advertisement