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 x^n for x real and n 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 nth 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!

Advertisements

About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College trained in the art of formalising mathematics on a computer.
This entry was posted in Learning Lean, M1F. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s