# `norm_num` extension for `Irrational` #

This module defines a `norm_num` extension for `Irrational x ^ y` for rational `x` and `y`. It also supports `Irrational √x` expressions.

## Implementation details #

To prove that `(a / b) ^ (p / q)` is irrational, we reduce the problem to showing that `(a / b) ^ p` is not a `q`-th power of any rational number. This, in turn, reduces to proving that either `a` or `b` is not a `q`-th power of a natural number, assuming `p` and `q` are coprime. To show that a given `n : ℕ` is not a `q`-th power, we find a natural number `k` such that `k ^ q < n < (k + 1) ^ q`, using binary search.

## TODO #

Disprove `Irrational x` for rational `x`.

source
structure Tactic.NormNum.NotPowerCertificate (m n : Q(ℕ)) :
Type

To prove that `m` is not `n`-power (and thus `m ^ (1/n)` is irrational), we find `k` such that `k ^ n < m < (k + 1) ^ n`.

- k : Q(ℕ)

  Natural `k` such that `k ^ n < m < (k + 1) ^ n`.

- pf_left : Q(unknown_1 ^ «$n» < «$m»)

  Proof of `k ^ n < m`.

- pf_right : Q(«$m» < (unknown_1 + 1) ^ «$n»)

  Proof of `m < (k + 1) ^ n`.

Instances For

source
def Tactic.NormNum.findNotPowerCertificateCore (m n : ℕ) :
Option ℕ

Finds `k` such that `k ^ n < m < (k + 1) ^ n` using bisection method. It assumes `n > 0`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Tactic.NormNum.findNotPowerCertificate (m n : Q(ℕ)) :
Lean.MetaM (NotPowerCertificate m n)

Finds `NotPowerCertificate` showing that `m` is not `n`-power.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Tactic.NormNum.evalIrrationalRpow :
Mathlib.Meta.NormNum.NormNumExt

`norm_num` extension that proves `Irrational x ^ y` for rational `y`. `x` may be natural or rational.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Tactic.NormNum.evalIrrationalSqrt :
Mathlib.Meta.NormNum.NormNumExt

`norm_num` extension that proves `Irrational √x` for rational `x`.

Equations

- One or more equations did not get rendered due to their size.

Instances For