seeking lemma about an archimedean thing

Stream: new members

[Jean Lo]

Attempting to do some analysis stuff in Lean and finding myself in need of the lemma that (with the appropriate hypotheses) would allow me to find, for given $a$ and $b$, the integer $n$ such that

$a ^ n < b$ and $b \le a ^ {n+1}$

Fiddled around a little with nat.find, then began to suspect that it is important enough a fact to be in mathlib somewhere. Though I don't have a very good idea of what the greatest generality is in which this is true, and so was unsure if I'm looking in the right place in mathlib. The closest thing I found so far was pow_unbounded_of_gt_one in algebra/archimedean. Could someone please point me in the right direction on this?

[Kevin Buzzard]

Equality is undecidable on the reals so in some sense you'll never find it, but you can prove it exists. I don't know what generality this is true in. An Archimedean ring is one for which the analogous thing is true for addition -- given a,b>0 we can find an integer n with na>b -- but the rationals are an Archimedean ring and they don't have exp and log.

[Kevin Buzzard]

Aah. I guess if a>1 then writing a=1+t we can prove a^n >= 1+nt so it will be true for Archimedean rings

[Kevin Buzzard]

So if a,b>1 in an Archimedean ring then the set of nats n such that a^n < b is non-empty and finite. Now it will be in mathlib that such a set has a largest element so there's a proof strategy. Because this has to do with Archimedean rings I would be tempted to look in Archimedean.lean and if it's not there then add it :-) But others might know better.

[Kevin Buzzard]

(Sorry for lack of formatting by the way, typing one handed on phone)

[Jean Lo]

here's an attempt at implementing what's been described (would need imports to be tested in a scratch file — typed it into archimedean.lean, it compiles there):

-- alagebra/archimedean.lean
lemma pow_approx {x : α} {y : α} (hx : 1 < x) (hy : 1 < y) :
  ∃ n : ℕ, y ^ n ≤ x ∧ x < y ^ (n + 1) :=
have h : ∃ n : ℕ, x < y ^ n, from pow_unbounded_of_gt_one _ hy,
by classical; exact let n := nat.find h in

  have hn  : x < y ^ n, from nat.find_spec h,
  have hnp : 0 < n,     from nat.pos_iff_ne_zero.2 (λ hn0,
    by rw [hn0, pow_zero] at hn; exact (not_lt_of_gt hn hx)),

  have hnsp : nat.pred n + 1 = n,     from nat.succ_pred_eq_of_pos hnp,
  have hltn : nat.pred n < n,         from nat.pred_lt (ne_of_gt hnp),
  have hnpn : ¬ x < y ^ (nat.pred n), from nat.find_min h hltn,

  ⟨nat.pred n, le_of_not_lt hnpn, by rwa hnsp⟩

no idea about what the name should be, and the amount of classical things in the proof worries me a little. Would doing the thing with the non-empty-and-finite-ness remove the requirement for things like decidable lts? I gave up on that and fell back to nat.find after failing to figure out how to work with some fintype-related stuff.