Sequences of rapidly growing value for a Northcott function

If h is Northcott, an infinite set contains elements of arbitrarily large h-value, because each sublevel set {a | h a ≤ b} is finite. Iterating this, one chooses a sequence in the set whose values exceed a given bound and grow at least as fast as any prescribed rule b ↦ f b.

For a height on a number field, such as Height.logHeight₁ on ℚ, this is how the proof of Roth's theorem selects good rational approximations of rapidly increasing heights from an infinite set of them: one takes f b = M * b.

Main results

• Northcott.exists_mem_lt: an infinite set contains elements of arbitrarily large h-value.
• Northcott.exists_seq_mem_lt: an infinite set contains a sequence with b < h (x 0) and f (h (x k)) < h (x (k + 1)) for every k.

References

• L. Pottmeyer, Diophantine Approximation (2022), §3.5.

theorem Northcott.exists_mem_lt {α : Type u_1} {β : Type u_2} [LinearOrder β] (h : α → β) [Northcott h] {s : Set α} (hs : s.Infinite) (b : β) : ∃ a ∈ s, b < h a

An infinite set contains elements of arbitrarily large value under a Northcott function.

theorem Northcott.exists_seq_mem_lt {α : Type u_1} {β : Type u_2} [LinearOrder β] (h : α → β) [Northcott h] (f : β → β) {s : Set α} (hs : s.Infinite) (b : β) : ∃ (x : ℕ → α), (∀ (k : ℕ), x k ∈ s) ∧ b < h (x 0) ∧ ∀ (k : ℕ), f (h (x k)) < h (x (k + 1))

An infinite set contains a sequence whose first value under a Northcott function h exceeds b, and each of whose values exceeds f applied to the previous one.