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.

theorem Tactic.NormNum.irrational_rpow_rat_rat_of_num {x y : ℝ} {x_num x_den y_num y_den k_num : ℕ} (hx_isNNRat : Mathlib.Meta.NormNum.IsNNRat x x_num x_den) (hy_isNNRat : Mathlib.Meta.NormNum.IsNNRat y y_num y_den) (hx_coprime : x_num.Coprime x_den) (hy_coprime : y_num.Coprime y_den) (hn1 : k_num ^ y_den < x_num) (hn2 : x_num < (k_num + 1) ^ y_den) : Irrational (x ^ y)

theorem Tactic.NormNum.irrational_rpow_rat_rat_of_den {x y : ℝ} {x_num x_den y_num y_den k_den : ℕ} (hx_isNNRat : Mathlib.Meta.NormNum.IsNNRat x x_num x_den) (hy_isNNRat : Mathlib.Meta.NormNum.IsNNRat y y_num y_den) (hx_coprime : x_num.Coprime x_den) (hy_coprime : y_num.Coprime y_den) (hd1 : k_den ^ y_den < x_den) (hd2 : x_den < (k_den + 1) ^ y_den) : Irrational (x ^ y)

theorem Tactic.NormNum.irrational_rpow_nat_rat {x y : ℝ} {x_num y_num y_den k : ℕ} (hx_isNat : Mathlib.Meta.NormNum.IsNat x x_num) (hy_isNNRat : Mathlib.Meta.NormNum.IsNNRat y y_num y_den) (hy_coprime : y_num.Coprime y_den) (hn1 : k ^ y_den < x_num) (hn2 : x_num < (k + 1) ^ y_den) : Irrational (x ^ y)

theorem Tactic.NormNum.irrational_sqrt_rat_of_num {x : ℝ} {num den num_k : ℕ} (hx_isNNRat : Mathlib.Meta.NormNum.IsNNRat x num den) (hx_coprime : num.Coprime den) (hn1 : num_k ^ 2 < num) (hn2 : num < (num_k + 1) ^ 2) : Irrational √x

theorem Tactic.NormNum.irrational_sqrt_rat_of_den {x : ℝ} {num den den_k : ℕ} (hx_isNNRat : Mathlib.Meta.NormNum.IsNNRat x num den) (hx_coprime : num.Coprime den) (hd1 : den_k ^ 2 < den) (hd2 : den < (den_k + 1) ^ 2) : Irrational √x

theorem Tactic.NormNum.irrational_sqrt_nat {x : ℝ} {n k : ℕ} (hx_isNat : Mathlib.Meta.NormNum.IsNat x n) (hn1 : k ^ 2 < n) (hn2 : n < (k + 1) ^ 2) : Irrational √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.

Equations

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

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.