Northcott Functions

In number theory, the height function h satisfies the Northcott property that the sets {a | h a ≤ b} are finite. This file extracts this notion as a typeclass and provides some API.

Main definitions

• Northcott h: A function h : α → β is Northcott if the sets {a : α | h a ≤ b} are all finite.

Main theorems

• Northcott.exists_min_image h s hs: If h is Northcott to a linear order, then h has an absolute minimum on every nonempty set s.

References

• D. Northcott, An inequality in the theory of arithmetic on algebraic varieties

class Northcott {α : Type u_1} {β : Type u_2} (h : α → β) [LE β] : Prop

A function h : α → β is Northcott if the sets {a : α | h a ≤ b} are all finite.

• finite_le (b : β) : {a : α | h a ≤ b}.Finite

theorem northcott_iff {α : Type u_1} {β : Type u_2} (h : α → β) [LE β] : Northcott h ↔ ∀ (b : β), {a : α | h a ≤ b}.Finite

theorem northcott_iff_tendsto {α : Type u_1} {β : Type u_2} (h : α → β) [LinearOrder β] [NoMaxOrder β] : Northcott h ↔ Filter.Tendsto h Filter.cofinite Filter.atTop

theorem Northcott.exists_min_image {α : Type u_1} {β : Type u_2} (h : α → β) [LinearOrder β] [Northcott h] (s : Set α) (hs : s.Nonempty) : ∃ a ∈ s, ∀ a' ∈ s, h a ≤ h a'