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.

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.

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.

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.

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.

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

norm_num extension that proves Irrational √x for rational x.