Zulip Chat Archive

Stream: new members

Topic: seeking lemma about an archimedean thing

view this post on Zulip Jean Lo (Mar 03 2019 at 00:24):

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 aa and bb, the integer nn such that

an<ba ^ n < b and ban+1b \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?

view this post on Zulip Kevin Buzzard (Mar 03 2019 at 09:38):

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.

view this post on Zulip Kevin Buzzard (Mar 03 2019 at 09:39):

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

view this post on Zulip Kevin Buzzard (Mar 03 2019 at 09:42):

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.

view this post on Zulip Kevin Buzzard (Mar 03 2019 at 09:43):

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

view this post on Zulip Jean Lo (Mar 03 2019 at 14:43):

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.

Last updated: May 11 2021 at 13:22 UTC