## 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 $n$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!