Documentation

Mathlib.Tactic.NormNum.NatLog

norm_num extensions for Nat.log and Nat.clog #

This module defines norm_num extensions for Nat.log and Nat.clog.

source
theorem Mathlib.Meta.NormNum.nat_log_zero (n : ℕ) :
Nat.log 0 n = 0
source
theorem Mathlib.Meta.NormNum.nat_log_one (n : ℕ) :
Nat.log 1 n = 0
source
theorem Mathlib.Meta.NormNum.nat_log_helper0 (b n : ℕ) (hl : n.blt b = true) :
Nat.log b n = 0
source
theorem Mathlib.Meta.NormNum.nat_log_helper (b n k : ℕ) (hl : (b ^ k).ble n = true) (hh : n.blt (b ^ (k + 1)) = true) :
Nat.log b n = k
source
theorem Mathlib.Meta.NormNum.isNat_log {b nb n nn k : ℕ} :
IsNat b nb → IsNat n nn → Nat.log nb nn = k → IsNat (Nat.log b n) k
source
def Mathlib.Meta.NormNum.proveNatLog (eb en : Q(ℕ)) :
(ek : Q(ℕ)) × Q(Nat.log «$eb» «$en» = «$ek»)

Given the natural number literals eb and en, returns Nat.log eb en as a natural number literal and an equality proof. Panics if ex or en aren't natural number literals.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Mathlib.Meta.NormNum.evalNatLog :
    NormNumExt

    Evaluates the Nat.log function.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Mathlib.Meta.NormNum.nat_clog_zero_left (b n : ℕ) (hb : b.ble 1 = true) :
      Nat.clog b n = 0
      source
      theorem Mathlib.Meta.NormNum.nat_clog_zero_right (b n : ℕ) (hn : n.ble 1 = true) :
      Nat.clog b n = 0
      source
      theorem Mathlib.Meta.NormNum.nat_clog_helper {b m n : ℕ} (hb : Nat.blt 1 b = true) (h₁ : (b ^ m).blt n = true) (h₂ : n.ble (b ^ (m + 1)) = true) :
      Nat.clog b n = m + 1
      source
      theorem Mathlib.Meta.NormNum.isNat_clog {b nb n nn k : ℕ} :
      IsNat b nb → IsNat n nn → Nat.clog nb nn = k → IsNat (Nat.clog b n) k
      source
      def Mathlib.Meta.NormNum.proveNatClog (eb en : Q(ℕ)) :
      (ek : Q(ℕ)) × Q(Nat.clog «$eb» «$en» = «$ek»)

      Given the natural number literals eb and en, returns Nat.clog eb en as a natural number literal and an equality proof. Panics if ex or en aren't natural number literals.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Mathlib.Meta.NormNum.evalNatClog :
        NormNumExt

        Evaluates the Nat.clog function.

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