findNotPowerCertificateCore

Mathlib.Tactic.NormNum.Irrational

URI: https://scilib.ai/kg/mathlib#Tactic.NormNum.findNotPowerCertificateCore

Lean4

/-- Finds `k` such that `k ^ n < m < (k + 1) ^ n` using bisection method. It assumes `n > 0`. -/
def findNotPowerCertificateCore (m n : ℕ) : Option ℕ :=
  Id.run
    (do
      let mut left := 0
      let mut right := m + 1
      while right - left > 1 do
        let middle := (left + right) / 2
        if middle ^ n ≤ m then
          left := middle
        else
          right := middle
      if left ^ n < m then
        return some left
      return none)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru