exists_rat_pow_btwn_rat without reals

Stream: maths

[Johan Commelin]

(Nerdsnipe alert) Is there a reasonably short proof of

theorem exists_rat_pow_btwn_rat (hn : n ≠ 0) {x y : ℚ} (h : x < y) (hy : 0 < y) :
    ∃ q : ℚ, 0 < q ∧ x < q ^ n ∧ q ^ n < y := by

that does not use $\R$?
Because docs#Real.exists_rat_pow_btwn_rat does go via the reals.
And it's in the dependency chain of file#Mathlib/Algebra/Order/CompleteField.lean which shows that the reals are unique up to unique isomorphism. But I feel like the uniqueness proof should not need to rely on the existence.

[Edward van de Meent]

an idea might be using newton-raphson?

[Edward van de Meent]

i.e. we can iterate q => q - (q^n-(x + y)/2)/(n*q^(n-1)) to find an approximation of (x+y)/2 with \epsilon < (y-x)/2?

[Edward van de Meent]

(i don't know if we have newton-raphson in mathlib tho)

[Edward van de Meent]

(and if it has few enough dependencies to be useful at this point)

[Edward van de Meent]

actually nvm, this still needs reals because q => q ^n - (x + y)/2 doesn't need to have a root in Rat

[Edward van de Meent]

this procedure will still work, but proving it does cannot go through the "classical" way

[Edward van de Meent]

the great bit about this is that the entire calculation doesn't use real numbers

[Junyan Xu]

Assume n > 0. Let's figure out how large the denominator r needs to be in order to find a solution q=p/r. It suffices that the maximal gap in the sequence $((p/r)^n)_{p=1}^\infty$ below y is less than y - x. The maximal gap is bounded by $((p+1)^n-p^n)/r^n$ where $p=ry$ (This is wrong: see below) and using the binomial theorem to expand it, we find that it can be bounded by $2^n p^{n-1}/r^n=2^n y^{n-1}/r$, so taking $r>2^n y^{n-1}/(y-x)$ should work.

[Scott Carnahan]

I suppose we should start by pretending x is 0 when x is negative.

[Daniel Weber]

This works up to the termination proof for exists_rat_pow_btwn_rat_aux, but I hope it should be possible using something along the lines of ⌊(r - l) / (y - x)⌋. Any ideas?

import Mathlib

theorem thing' (hn : n ≠ 0) {x : ℚ} (h : 0 < x) : x < (x + 1) ^ n :=
  calc
    x < x + 1 := by linarith
    _ ≤ (x + 1) ^ n := le_self_pow₀ (by linarith) hn

theorem thing (hn : n ≠ 0) {x y : ℚ} (h : x < y) (hy : 0 < y) : x < (y + 1) ^ n :=
  (thing' hn hy).trans' h

theorem exists_rat_pow_btwn_rat_aux (hn : n ≠ 0) {x y : ℚ} (h : x < y) (hy : 0 < y) (l r : ℚ) (hl : 0 ≤ l) (hlr : l < r) (h1 : l^n < y) (h2 : x < r^n) :
    ∃ q : ℚ, 0 ≤ q ∧ x < q ^ n ∧ q ^ n < y := by
  by_cases hs : r^n - l^n < y - x
  · suffices x < l^n ∨ r^n < y by
      obtain this | this := this
      · use l
      · use r
        split_ands <;> linarith
    by_contra!
    linarith
  · by_cases hm : x < ((l + r) / 2) ^ n
    · exact exists_rat_pow_btwn_rat_aux hn h hy l _ hl (by linarith) h1 hm
    · exact exists_rat_pow_btwn_rat_aux hn h hy ((l + r) / 2) r (by linarith) (by linarith) (by linarith) h2

theorem exists_rat_pow_btwn_rat' (hn : n ≠ 0) {x y : ℚ} (h : x < y) (hy : 0 < y) :
    ∃ q : ℚ, 0 ≤ q ∧ x < q ^ n ∧ q ^ n < y :=
  exists_rat_pow_btwn_rat_aux hn h hy 0 (y + 1) (by linarith) (by linarith) (by simp_all) (thing hn h hy)

theorem exists_rat_pow_btwn_rat (hn : n ≠ 0) {x y : ℚ} (h : x < y) (hy : 0 < y) :
    ∃ q : ℚ, 0 < q ∧ x < q ^ n ∧ q ^ n < y := by
  obtain ⟨q, hq1, hq2, hq3⟩ := exists_rat_pow_btwn_rat' hn (x := max x 0) (by simp [*]) hy
  use q
  simp_all only [ne_eq, sup_lt_iff, and_self, and_true]
  by_contra! hq
  obtain rfl : q = 0 := by linarith
  simp_all

[Johan Commelin]

Thanks for these ideas. I'll have to park them, because I need to grade two exams. But I hope to return to them later.

[Johan Commelin]

I'm working on that termination proof. Need to have breakfast now. This is what I have so far:

theorem exists_rat_pow_btwn_rat_aux' (hn : n ≠ 0) {x y : ℚ} (h : x < y) (hy : 0 < y) (l r : ℚ) (hl : 0 ≤ l) (hlr : l < r) (h1 : l^n < y) (h2 : x < r^n) :
    ∃ q : ℚ, 0 ≤ q ∧ x < q ^ n ∧ q ^ n < y := by
  by_cases hs : r^n - l^n < y - x
  · suffices x < l^n ∨ r^n < y by
      obtain this | this := this
      · use l
      · use r
        split_ands <;> linarith
    by_contra!
    linarith
  · by_cases hm : x < ((l + r) / 2) ^ n
    · exact exists_rat_pow_btwn_rat_aux' hn h hy l _ hl (by linarith) h1 hm
    · exact exists_rat_pow_btwn_rat_aux' hn h hy ((l + r) / 2) r (by linarith) (by linarith) (by linarith) h2
termination_by
  ⌊(r^n - l^n) / (y - x)⌋₊
decreasing_by
  · rename_i i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11; clear i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11
    zify
    have ysx : 0 < y - x := by linarith
    rw [Int.natCast_floor_eq_floor, Int.natCast_floor_eq_floor]
    · rw [Int.floor_lt]
      have aux₁ : ((r ^ n - l ^ n) / 2) / (y - x) < ↑⌊(r ^ n - l ^ n) / (y - x)⌋ := by
        rw [div_div, mul_comm, ← div_div]
        have (a : ℚ) (ha : 1 ≤ a) : a / 2 < ⌊a⌋ := by
          suffices Int.fract a < ⌊a⌋ by linarith [Int.fract_add_floor a]
          apply (Int.fract_lt_one a).trans_le
          have := Int.le_floor (z := 1) (a := a)
          simp only [Int.cast_one] at this
          rw [← this] at ha
          exact_mod_cast ha
        apply this
        rw [le_div_iff₀ ysx, one_mul]
        linarith
      apply lt_trans _ aux₁
      rw [div_lt_div_iff_of_pos_right ysx]
      have aux₂ : ((r ^ n - l ^ n) / 2) = ((l ^ n + r ^ n) / 2) - l ^ n := by field_simp; ring
      rw [aux₂, sub_lt_sub_iff_right]
      sorry
    · apply div_nonneg _ ysx.le
      linarith
    · apply div_nonneg _ ysx.le
      apply sub_nonneg_of_le
      apply pow_le_pow_left₀ hl
      linarith
  · sorry

[Daniel Weber]

I don't think the first sorry is true for n = 1

[Daniel Weber]

I think this should be helpful

theorem rat_pow_convex_pos (l e : ℚ) (hl : 0 ≤ l) (he : 0 ≤ e) :
    (l + e / 2 : ℚ) ^ n ≤ (l^n + (l + e)^n) / 2 := by
  simp only [add_comm l (e / 2), add_pow, div_pow, div_mul_eq_mul_div,
    Finset.sum_range_eq_add_Ico _ (Nat.add_one_pos _), pow_zero, tsub_zero, one_mul,
    Nat.choose_zero_right, Nat.cast_one, mul_one, div_one, add_comm l e, ← add_assoc, ← two_mul,
    add_div, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, mul_div_cancel_left₀, Finset.sum_div,
    add_le_add_iff_left]
  gcongr with i hi
  apply le_self_pow₀ one_le_two
  simp at hi
  omega

[Junyan Xu]

Here's a full proof roughly following my outline; I have to adjust the argument because $p=ry$ should be $p^n = r^n y$ instead.

import Mathlib.Data.Nat.Choose.Sum
import Mathlib.Data.Rat.Floor

theorem one_add_pow_le {m : ℚ} {n : ℕ} (hm : 0 ≤ m) :
    (1 + m) ^ n ≤ m ^ n + 2 ^ n * max 1 m ^ (n - 1) := by
  rw [add_pow, ← Finset.add_sum_erase _ _ (Finset.mem_range_succ_iff.mpr n.zero_le),
    pow_zero, one_mul, Nat.sub_zero, Nat.choose_zero_right, Nat.cast_one, mul_one]
  refine add_le_add_left ((Finset.sum_le_sum (g := fun i ↦ max 1 m ^ (n - 1) * n.choose i) ?_).trans ?_) _
  · rintro i hi
    rw [Finset.mem_erase, Finset.mem_range_succ_iff] at hi
    refine mul_le_mul_of_nonneg_right ?_ (by positivity)
    rw [one_pow, one_mul]
    exact (pow_le_pow_left₀ hm le_sup_right _).trans
      (pow_le_pow_right₀ le_sup_left <| Nat.sub_le_sub_left (Nat.one_le_iff_ne_zero.mpr hi.1) _)
  · rw [← Finset.mul_sum, ← Nat.cast_sum, mul_comm]
    refine mul_le_mul_of_nonneg_right ?_ (by positivity)
    rw [← Nat.cast_two, ← Nat.cast_pow, Nat.cast_le]
    exact (Finset.sum_le_sum_of_subset <| Finset.erase_subset _ _).trans_eq n.sum_range_choose

theorem exists_rat_pow_btwn_rat (hn : n ≠ 0) {x y : ℚ} (h : x < y) (hy : 0 < y) :
    ∃ q : ℚ, 0 < q ∧ x < q ^ n ∧ q ^ n < y := by
  wlog hx : 0 ≤ x generalizing x
  · have ⟨q, q_pos, qn_pos, lt_y⟩ := this hy le_rfl
    exact ⟨q, q_pos, (le_of_not_le hx).trans_lt qn_pos, lt_y⟩
  have yx_pos := sub_pos.mpr h
  obtain rfl | hn1 := (Nat.one_le_iff_ne_zero.mpr hn).eq_or_lt
  · exact ⟨(x + y) / 2, by positivity, by linarith, by linarith⟩
  let d := (2 ^ n * max 1 y) / (y - x)
  have h1d : 1 < d := (one_lt_div yx_pos).mpr <| ((sub_le_self _ hx).trans le_sup_right).trans_lt
    (lt_mul_of_one_lt_left (by positivity) <| one_lt_pow₀ one_lt_two hn)
  have d_pos : 0 < d := zero_lt_one.trans h1d
  have ex : ∃ m : ℕ, y ≤ (m / d) ^ n := by
    refine ⟨⌈y * d + d⌉₊, le_trans ?_ (le_self_pow₀ ?_ hn)⟩
    · rw [le_div_iff₀ d_pos]
      exact ((lt_add_of_pos_right _ d_pos).le.trans <| Nat.le_ceil _)
    · rw [le_div_iff₀ d_pos, one_mul]
      exact (le_add_of_nonneg_left <| by positivity).trans (Nat.le_ceil _)
  let num := Nat.find ex
  have num_pos : 0 < num := (Nat.find_pos _).mpr <| by simpa [zero_pow hn] using hy
  let q := num.pred / d
  have qny : q ^ n < y := lt_of_not_le (Nat.find_min ex <| Nat.pred_lt num_pos.ne')
  have key : max 1 ↑num.pred ^ (n - 1) / d ^ n < max 1 y / d := by
    conv in (d ^ _) => rw [← Nat.sub_one_add_one hn, pow_add, pow_one]
    rw [← div_div, ← div_pow, div_lt_div_iff_of_pos_right d_pos, lt_max_iff, or_iff_not_imp_left,
      not_lt, one_le_pow_iff_of_nonneg (by positivity) (Nat.sub_pos_of_lt hn1).ne']
    refine fun h ↦ (pow_le_pow_right₀ h <| n.sub_le 1).trans_lt ?_
    have : (1 : ℚ) ≤ num.pred := Nat.cast_le.mpr <| Nat.one_le_iff_ne_zero.mpr fun eq ↦ by
      rw [← max_div_div_right d_pos.le, le_max_iff, or_iff_not_imp_left, not_le, one_div,
        inv_lt_one₀ d_pos, eq, Nat.cast_zero, zero_div] at h
      exact zero_lt_one.not_le (h h1d)
    rwa [max_eq_right this]
  have xqn : x < q ^ n :=
    calc x = y - (y - x) := (sub_sub_cancel _ _).symm
      _ ≤ (num / d) ^ n - 2 ^ n * max 1 y / d :=
        sub_le_sub (Nat.find_spec ex) (div_div_cancel₀ <| by positivity).le
      _ = (1 + num.pred) ^ n / d ^ n - _ := by rw [← Nat.cast_one, ← Nat.cast_add,
        Nat.cast_one, ← Nat.succ_eq_one_add, Nat.succ_pred num_pos.ne', div_pow]
      _ ≤ num.pred ^ n / d ^ n + 2 ^ n * (max 1 ↑num.pred ^ (n - 1) / d ^ n - max 1 y / d) :=
        (sub_le_sub_right (div_le_div_of_nonneg_right (one_add_pow_le <| Nat.cast_nonneg _) <|
          by positivity) _).trans <| by simp_rw [add_div, mul_sub, add_sub, mul_div, le_rfl]
      _ = q ^ n + _ := by rw [← div_pow]
      _ < q ^ n := add_lt_of_neg_right _ (mul_neg_of_pos_of_neg (by positivity) <| sub_neg.mpr key)
  refine ⟨q, lt_of_le_of_ne (by positivity) fun hq ↦ hx.not_lt ?_, xqn, qny⟩
  rwa [← hq, zero_pow hn] at xqn

[Johan Commelin]

Very nice!

[Johan Commelin]

@Junyan Xu I took the liberty to include this in #20242, listing you as co-author.

[Johan Commelin]

The main benefit of this PR is the following import reduction:

Mathlib.Algebra.Order.CompleteField 1546 631 -915 (-59.18%)

[Junyan Xu]

Here's a shorter version that makes it clear that the essential fact used is that the power functions are uniformly continuous on bounded intervals (which is also what you need to extend the power functions continuously to the reals):

import Mathlib.Algebra.Order.Floor -- not importing Rat, 593 -> 572 trans_imports
import Mathlib.Data.Nat.Choose.Sum

variable {α : Type*} [LinearOrderedField α]

theorem uniform_continuous_npow_on_bounded (B : α) {ε : α} (hε : 0 < ε) (n : ℕ) :
    ∃ δ > 0, ∀ q r : α, |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε := by
  wlog B_pos : 0 < B generalizing B
  · have ⟨δ, δ_pos, cont⟩ := this 1 zero_lt_one
    exact ⟨δ, δ_pos, fun q r hr ↦ cont q r (hr.trans ((le_of_not_lt B_pos).trans zero_le_one))⟩
  let δ := min B (ε / (2 ^ n * B ^ (n - 1)))
  refine ⟨δ, by positivity, fun q r hr hqr ↦ ?_⟩
  have mem := Finset.mem_range_succ_iff.mpr n.zero_le
  rw [← sub_add_cancel q r, add_pow, ← Finset.add_sum_erase _ _ mem, pow_zero, one_mul,
    Nat.sub_zero, Nat.choose_zero_right, Nat.cast_one, mul_one, add_sub_cancel_left]
  refine (Finset.abs_sum_le_sum_abs _ _).trans_lt ?_
  simp_rw [abs_mul, abs_pow, Nat.abs_cast]
  refine (Finset.sum_le_sum (g := fun i ↦ δ * B ^ (n - 1) * n.choose i) fun i hi ↦ ?_).trans_lt ?_
  · rw [Finset.mem_erase, Finset.mem_range_succ_iff] at hi
    refine mul_le_mul_of_nonneg_right ?_ (by positivity)
    conv in |_ - _| ^ _ => rw [← Nat.sub_one_add_one hi.1, add_comm, pow_add, pow_one]
    refine mul_assoc |q - r| _ _ ▸ mul_le_mul hqr ?_ (by positivity) (by positivity)
    exact (mul_le_mul (pow_le_pow_left₀ (abs_nonneg _) (hqr.trans inf_le_left) _)
      (pow_le_pow_left₀ (abs_nonneg _) hr _) (by positivity) (by positivity)).trans_eq
      ((pow_add ..).symm.trans <| by congr; omega)
  · rw [← Finset.mul_sum, ← lt_div_iff₀' (by positivity)]
    refine (Finset.sum_lt_sum_of_subset (Finset.erase_subset _ _) mem
      (Finset.not_mem_erase _ _) (by simp) fun _ _ _ ↦ Nat.cast_nonneg _).trans_le ?_
    rw [← Nat.cast_sum, n.sum_range_choose, le_div_iff₀' (by positivity),
      Nat.cast_pow, Nat.cast_two, mul_assoc, ← le_div_iff₀ (by positivity), mul_comm]
    exact inf_le_right

theorem exists_npow_btwn [FloorSemiring α] (hn : n ≠ 0) {x y : α} (h : x < y) (hy : 0 < y) :
    ∃ q : α, 0 < q ∧ x < q ^ n ∧ q ^ n < y := by
  have ⟨δ, δ_pos, cont⟩ := uniform_continuous_npow_on_bounded (max 1 y)
    (sub_pos.mpr <| max_lt_iff.mpr ⟨h, hy⟩) n
  have ex : ∃ m : ℕ, y ≤ (m * δ) ^ n := by
    refine ⟨⌈y / δ + 1 / δ⌉₊, le_trans ?_ (le_self_pow₀ ?_ hn)⟩ <;> rw [← div_le_iff₀ δ_pos]
    · exact ((lt_add_of_pos_right _ <| by positivity).le.trans <| Nat.le_ceil _)
    · exact (le_add_of_nonneg_left <| by positivity).trans (Nat.le_ceil _)
  let m := Nat.find ex
  have m_pos : 0 < m := (Nat.find_pos _).mpr <| by simpa [zero_pow hn] using hy
  let q := m.pred * δ
  have qny : q ^ n < y := lt_of_not_le (Nat.find_min ex <| Nat.pred_lt m_pos.ne')
  have q1y : |q| < max 1 y := (abs_eq_self.mpr <| by positivity).trans_lt <| lt_max_iff.mpr
    (or_iff_not_imp_left.mpr fun q1 ↦ (le_self_pow₀ (le_of_not_lt q1) hn).trans_lt qny)
  have xqn : max x 0 < q ^ n :=
    calc _ = y - (y - max x 0) := by rw [sub_sub_cancel]
      _ ≤ (m * δ) ^ n - (y - max x 0) := sub_le_sub_right (Nat.find_spec ex) _
      _ < (m * δ) ^ n - ((m * δ) ^ n - q ^ n) := by
        refine sub_lt_sub_left ((le_abs_self _).trans_lt <| cont _ _ q1y.le ?_) _
        rw [← Nat.succ_pred_eq_of_pos m_pos, Nat.cast_succ, ← sub_mul,
          add_sub_cancel_left, one_mul, abs_eq_self.mpr (by positivity)]
      _ = q ^ n := sub_sub_cancel ..
  exact ⟨q, lt_of_le_of_ne (by positivity) fun q0 ↦
    (le_sup_right.trans_lt xqn).ne <| q0 ▸ (zero_pow hn).symm, le_sup_left.trans_lt xqn, qny⟩

[Junyan Xu]

exists_npow_btwn can fail if the field isn't archimedean, for example in this example on Wikipedia, because there are no rational functions that grows like $x^{1/n}$.
image.png

[Johan Commelin]

Nice! Feel free to push this to the PR.
Do you think you can structure it in such a way that now file has an increase in transitive imports?
(Because import Mathlib.Data.Nat.Choose.Sum is a new import, right?)

[Junyan Xu]

Can you elaborate? import Mathlib.Data.Nat.Choose.Sum is present in both versions of my proof because I'm using the binomial theorem contained in the file. This file is also imported by the file Mathlib.Analysis.SpecialFunctions.Pow.Real that contains the original proof of exists_rat_pow_btwn_rat.

[Johan Commelin]

Right, but that Analysis file is really heavy! In the PR, I cut 915 imports away from Algebra.Order.CompleteField by avoiding importing that file.
I think that file ought to be really low-level. If it costs ~10 extra lines to avoid big operators etc, that might be worth it.

[Junyan Xu]

Oh, I see what you want. Certainly the uniform continuity proof is also amenable to the inductive approach.

[Kevin Buzzard]

Why don't you move the lemma to a later file rather than proving it with fewer imports?

[Ruben Van de Velde]

It's fundamental to the point of that file, no?

[Junyan Xu]

Okay, I got rid of binomial theorem, using a handrolled geometric sum instead:

import Mathlib.Algebra.Order.Ring.Abs
import Mathlib.Tactic.Positivity.Basic
import Mathlib.Tactic.Ring

import Mathlib.Algebra.Order.Field.Defs -- for the last theorem

section

variable {α : Type*} [LinearOrderedCommRing α] (a b : α) (n : ℕ)

private def geomSum : ℕ → α
  | 0 => 1
  | n + 1 => a * geomSum n + b ^ (n + 1)

private theorem abs_geomSum_le : |geomSum a b n| ≤ (n + 1) * max |a| |b| ^ n := by
  induction' n with n ih; · simp [geomSum]
  refine (abs_add_le ..).trans ?_
  rw [abs_mul, abs_pow, Nat.cast_succ, add_one_mul]
  refine add_le_add ?_ (pow_le_pow_left₀ (abs_nonneg _) le_sup_right _)
  rw [pow_succ, ← mul_assoc, mul_comm |a|]
  exact mul_le_mul ih le_sup_left (abs_nonneg _) (by positivity)

private theorem pow_sub_pow_eq_sub_mul_geomSum :
    a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n := by
  induction' n with n ih; · simp [geomSum]
  rw [geomSum, mul_add, mul_comm a, ← mul_assoc, ← ih]
  ring

theorem pow_sub_pow_le : |a ^ n - b ^ n| ≤ |a - b| * n * max |a| |b| ^ (n - 1) := by
  obtain _ | n := n; · simp
  rw [Nat.add_sub_cancel, pow_sub_pow_eq_sub_mul_geomSum, abs_mul, mul_assoc, Nat.cast_succ]
  exact mul_le_mul_of_nonneg_left (abs_geomSum_le ..) (abs_nonneg _)

end

variable {α : Type*} [LinearOrderedField α]

theorem uniform_continuous_npow_on_bounded (B : α) {ε : α} (hε : 0 < ε) (n : ℕ) :
    ∃ δ > 0, ∀ q r : α, |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε := by
  wlog B_pos : 0 < B generalizing B
  · have ⟨δ, δ_pos, cont⟩ := this 1 zero_lt_one
    exact ⟨δ, δ_pos, fun q r hr ↦ cont q r (hr.trans ((le_of_not_lt B_pos).trans zero_le_one))⟩
  refine ⟨min 1 (ε / (1 + n * (B + 1) ^ (n - 1))), lt_min zero_lt_one
    (div_pos hε <| by positivity), fun q r hr hqr ↦ (pow_sub_pow_le ..).trans_lt ?_⟩
  -- `positivity` needs some help
  rw [le_inf_iff, le_div_iff₀ (by positivity), mul_one_add, ← mul_assoc] at hqr
  obtain h | h := (abs_nonneg (q - r)).eq_or_lt
  · simpa only [← h, zero_mul] using hε
  refine (lt_of_le_of_lt ?_ <| lt_add_of_pos_left _ h).trans_le hqr.2
  refine mul_le_mul_of_nonneg_left (pow_le_pow_left₀ (by positivity) ?_ _) (by positivity)
  refine max_le ?_ (hr.trans <| le_add_of_nonneg_right zero_le_one)
  exact add_sub_cancel r q ▸ (abs_add_le ..).trans (add_le_add hr hqr.1)

[Junyan Xu]

It's not hard to get rid of the use of ring and positivity as well; now the section can go into Mathlib.Algebra.Order.Ring.Abs (322 imports) and the last theorem can also if we import Mathlib.Algebra.Order.Field.Defs (+3 imports). If we don't want to add imports to an existing file, a natural home is Mathlib.Algebra.Order.Field.Basic (381 imports).
exists_npow_btwn must and can go into Mathlib.Algebra.Order.Floor (473 imports), and exists_rat_pow_btwn_rat must and can go into Mathlib.Data.Rat.Floor (480 imports).

import Mathlib.Algebra.Order.Field.Basic

section

variable {α : Type*} [LinearOrderedCommRing α] (a b : α) (n : ℕ)

private def geomSum : ℕ → α
  | 0 => 1
  | n + 1 => a * geomSum n + b ^ (n + 1)

private theorem abs_geomSum_le : |geomSum a b n| ≤ (n + 1) * max |a| |b| ^ n := by
  induction' n with n ih; · simp [geomSum]
  refine (abs_add_le ..).trans ?_
  rw [abs_mul, abs_pow, Nat.cast_succ, add_one_mul]
  refine add_le_add ?_ (pow_le_pow_left₀ (abs_nonneg _) le_sup_right _)
  rw [pow_succ, ← mul_assoc, mul_comm |a|]
  exact mul_le_mul ih le_sup_left (abs_nonneg _) (mul_nonneg
    (@Nat.cast_succ α .. ▸ Nat.cast_nonneg _) <| pow_nonneg ((abs_nonneg _).trans le_sup_left) _)

private theorem pow_sub_pow_eq_sub_mul_geomSum :
    a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n := by
  induction' n with n ih; · simp [geomSum]
  rw [geomSum, mul_add, mul_comm a, ← mul_assoc, ← ih,
    sub_mul, sub_mul, ← pow_succ, ← pow_succ', mul_comm, sub_add_sub_cancel]

theorem pow_sub_pow_le : |a ^ n - b ^ n| ≤ |a - b| * n * max |a| |b| ^ (n - 1) := by
  obtain _ | n := n; · simp
  rw [Nat.add_sub_cancel, pow_sub_pow_eq_sub_mul_geomSum, abs_mul, mul_assoc, Nat.cast_succ]
  exact mul_le_mul_of_nonneg_left (abs_geomSum_le ..) (abs_nonneg _)

end

variable {α : Type*} [LinearOrderedField α]

theorem uniform_continuous_npow_on_bounded (B : α) {ε : α} (hε : 0 < ε) (n : ℕ) :
    ∃ δ > 0, ∀ q r : α, |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε := by
  wlog B_pos : 0 < B generalizing B
  · have ⟨δ, δ_pos, cont⟩ := this 1 zero_lt_one
    exact ⟨δ, δ_pos, fun q r hr ↦ cont q r (hr.trans ((le_of_not_lt B_pos).trans zero_le_one))⟩
  have pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1) := zero_lt_one.trans_le <| le_add_of_nonneg_right <|
    mul_nonneg n.cast_nonneg <| (pow_pos (B_pos.trans <| lt_add_of_pos_right _ zero_lt_one) _).le
  refine ⟨min 1 (ε / (1 + n * (B + 1) ^ (n - 1))), lt_min zero_lt_one (div_pos hε pos),
    fun q r hr hqr ↦ (pow_sub_pow_le ..).trans_lt ?_⟩
  rw [le_inf_iff, le_div_iff₀ pos, mul_one_add, ← mul_assoc] at hqr
  obtain h | h := (abs_nonneg (q - r)).eq_or_lt
  · simpa only [← h, zero_mul] using hε
  refine (lt_of_le_of_lt ?_ <| lt_add_of_pos_left _ h).trans_le hqr.2
  refine mul_le_mul_of_nonneg_left (pow_le_pow_left₀ ((abs_nonneg _).trans le_sup_left) ?_ _)
    (mul_nonneg (abs_nonneg _) n.cast_nonneg)
  refine max_le ?_ (hr.trans <| le_add_of_nonneg_right zero_le_one)
  exact add_sub_cancel r q ▸ (abs_add_le ..).trans (add_le_add hr hqr.1)

[Junyan Xu]

I pushed to this branch. I ended up keeping the main results inside Mathlib.Algebra.Order.Archimedean.Basic even though it's higher in the import hierarchy than the two Floor files, because the Prop-valued Archimedean assumption is better than FloorSemiring.

[Johan Commelin]

Thanks! I've merged that into the PR