English
For a>1 and any b,c there exists a unique integer m such that b/a^m ∈ [c, c a).
Русский
Для a>1 и любых b,c существует уникальный целочисленный m such, что b/a^m ∈ [c, c a).
LaTeX
$$$\\exists! m\\in \\mathbb{Z},\\ b/a^{m} \\in [c, c a).$$$
Lean4
/-- An archimedean decidable linearly ordered `CommGroup` has a version of the floor: for
`a > 1`, any `g` in the group lies between some two consecutive powers of `a`. -/
@[to_additive /-- An archimedean decidable linearly ordered `AddCommGroup` has a version of the
floor: for `a > 0`, any `g` in the group lies between some two consecutive multiples of `a`. -/
]
theorem existsUnique_zpow_near_of_one_lt {a : G} (ha : 1 < a) (g : G) : ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1) :=
by
let s : Set ℤ := {n : ℤ | a ^ n ≤ g}
obtain ⟨k, hk : g⁻¹ ≤ a ^ k⟩ := MulArchimedean.arch g⁻¹ ha
have h_ne : s.Nonempty := ⟨-k, by simpa [s] using inv_le_inv' hk⟩
obtain ⟨k, hk⟩ := MulArchimedean.arch g ha
have h_bdd : ∀ n ∈ s, n ≤ (k : ℤ) := by
intro n hn
apply (zpow_le_zpow_iff_right ha).mp
rw [← zpow_natCast] at hk
exact le_trans hn hk
obtain ⟨m, hm, hm'⟩ := Int.exists_greatest_of_bdd ⟨k, h_bdd⟩ h_ne
have hm'' : g < a ^ (m + 1) := by
contrapose! hm'
exact ⟨m + 1, hm', lt_add_one _⟩
refine ⟨m, ⟨hm, hm''⟩, fun n hn => (hm' n hn.1).antisymm <| Int.le_of_lt_add_one ?_⟩
rw [← zpow_lt_zpow_iff_right ha]
exact lt_of_le_of_lt hm hn.2
