The nth Number Satisfying a Predicate

This file defines a function for "what is the nth number that satisfies a given predicate p", and provides lemmas that deal with this function and its connection to Nat.count.

Main definitions

• Nat.nth p n: The n-th natural k (zero-indexed) such that p k. If there is no such natural (that is, p is true for at most n naturals), then Nat.nth p n = 0.

Main results

• Nat.nth_eq_orderEmbOfFin: For a finitely-often true p, gives the cardinality of the set of numbers satisfying p above particular values of nth p
• Nat.gc_count_nth: Establishes a Galois connection between Nat.nth p and Nat.count p.
• Nat.nth_eq_orderIsoOfNat: For an infinitely-often true predicate, nth agrees with the order-isomorphism of the subtype to the natural numbers.

There has been some discussion on the subject of whether both of nth and Nat.Subtype.orderIsoOfNat should exist. See discussion here. Future work should address how lemmas that use these should be written.

noncomputable def Nat.nth (p : ℕ → Prop) (n : ℕ) : ℕ

Find the n-th natural number satisfying p (indexed from 0, so nth p 0 is the first natural number satisfying p), or 0 if there is no such number. See also Subtype.orderIsoOfNat for the order isomorphism with ℕ when p is infinitely often true.

Equations

• Nat.nth p n = if h : (setOf p).Finite then (Finset.sort (fun (x1 x2 : ℕ) => x1 ≤ x2) h.toFinset).getD n 0 else ↑((Nat.Subtype.orderIsoOfNat (setOf p)) n)

Lemmas about Nat.nth on a finite set

theorem Nat.nth_of_card_le {p : ℕ → Prop} (hf : (setOf p).Finite) {n : ℕ} (hn : hf.toFinset.card ≤ n) : Nat.nth p n = 0

theorem Nat.nth_eq_getD_sort {p : ℕ → Prop} (h : (setOf p).Finite) (n : ℕ) : Nat.nth p n = (Finset.sort (fun (x1 x2 : ℕ) => x1 ≤ x2) h.toFinset).getD n 0

theorem Nat.nth_eq_orderEmbOfFin {p : ℕ → Prop} (hf : (setOf p).Finite) {n : ℕ} (hn : n < hf.toFinset.card) : Nat.nth p n = (hf.toFinset.orderEmbOfFin ⋯) ⟨n, hn⟩

theorem Nat.nth_strictMonoOn {p : ℕ → Prop} (hf : (setOf p).Finite) : StrictMonoOn (Nat.nth p) (Set.Iio hf.toFinset.card)

theorem Nat.nth_lt_nth_of_lt_card {p : ℕ → Prop} (hf : (setOf p).Finite) {m n : ℕ} (h : m < n) (hn : n < hf.toFinset.card) : Nat.nth p m < Nat.nth p n

theorem Nat.nth_le_nth_of_lt_card {p : ℕ → Prop} (hf : (setOf p).Finite) {m n : ℕ} (h : m ≤ n) (hn : n < hf.toFinset.card) : Nat.nth p m ≤ Nat.nth p n

theorem Nat.lt_of_nth_lt_nth_of_lt_card {p : ℕ → Prop} (hf : (setOf p).Finite) {m n : ℕ} (h : Nat.nth p m < Nat.nth p n) (hm : m < hf.toFinset.card) : m < n

theorem Nat.le_of_nth_le_nth_of_lt_card {p : ℕ → Prop} (hf : (setOf p).Finite) {m n : ℕ} (h : Nat.nth p m ≤ Nat.nth p n) (hm : m < hf.toFinset.card) : m ≤ n

theorem Nat.nth_injOn {p : ℕ → Prop} (hf : (setOf p).Finite) : Set.InjOn (Nat.nth p) (Set.Iio hf.toFinset.card)

theorem Nat.range_nth_of_finite {p : ℕ → Prop} (hf : (setOf p).Finite) : Set.range (Nat.nth p) = insert 0 (setOf p)

@[simp]

theorem Nat.image_nth_Iio_card {p : ℕ → Prop} (hf : (setOf p).Finite) : Nat.nth p '' Set.Iio hf.toFinset.card = setOf p

theorem Nat.nth_mem_of_lt_card {p : ℕ → Prop} {n : ℕ} (hf : (setOf p).Finite) (hlt : n < hf.toFinset.card) : p (Nat.nth p n)

theorem Nat.exists_lt_card_finite_nth_eq {p : ℕ → Prop} (hf : (setOf p).Finite) {x : ℕ} (h : p x) : ∃ n < hf.toFinset.card, Nat.nth p n = x

Lemmas about Nat.nth on an infinite set

theorem Nat.nth_apply_eq_orderIsoOfNat {p : ℕ → Prop} (hf : (setOf p).Infinite) (n : ℕ) : Nat.nth p n = ↑((Nat.Subtype.orderIsoOfNat (setOf p)) n)

When s is an infinite set, nth agrees with Nat.Subtype.orderIsoOfNat.

theorem Nat.nth_eq_orderIsoOfNat {p : ℕ → Prop} (hf : (setOf p).Infinite) : Nat.nth p = Subtype.val ∘ ⇑(Nat.Subtype.orderIsoOfNat (setOf p))

When s is an infinite set, nth agrees with Nat.Subtype.orderIsoOfNat.

theorem Nat.nth_strictMono {p : ℕ → Prop} (hf : (setOf p).Infinite) : StrictMono (Nat.nth p)

theorem Nat.nth_injective {p : ℕ → Prop} (hf : (setOf p).Infinite) : Function.Injective (Nat.nth p)

theorem Nat.nth_monotone {p : ℕ → Prop} (hf : (setOf p).Infinite) : Monotone (Nat.nth p)

theorem Nat.nth_lt_nth {p : ℕ → Prop} (hf : (setOf p).Infinite) {k n : ℕ} : Nat.nth p k < Nat.nth p n ↔ k < n

theorem Nat.nth_le_nth {p : ℕ → Prop} (hf : (setOf p).Infinite) {k n : ℕ} : Nat.nth p k ≤ Nat.nth p n ↔ k ≤ n

theorem Nat.range_nth_of_infinite {p : ℕ → Prop} (hf : (setOf p).Infinite) : Set.range (Nat.nth p) = setOf p

theorem Nat.nth_mem_of_infinite {p : ℕ → Prop} (hf : (setOf p).Infinite) (n : ℕ) : p (Nat.nth p n)

Lemmas that work for finite and infinite sets

theorem Nat.exists_lt_card_nth_eq {p : ℕ → Prop} {x : ℕ} (h : p x) : ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < hf.toFinset.card) ∧ Nat.nth p n = x

theorem Nat.subset_range_nth {p : ℕ → Prop} : setOf p ⊆ Set.range (Nat.nth p)

theorem Nat.range_nth_subset {p : ℕ → Prop} : Set.range (Nat.nth p) ⊆ insert 0 (setOf p)

theorem Nat.nth_mem {p : ℕ → Prop} (n : ℕ) (h : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card) : p (Nat.nth p n)

theorem Nat.nth_lt_nth' {p : ℕ → Prop} {m n : ℕ} (hlt : m < n) (h : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card) : Nat.nth p m < Nat.nth p n

theorem Nat.nth_le_nth' {p : ℕ → Prop} {m n : ℕ} (hle : m ≤ n) (h : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card) : Nat.nth p m ≤ Nat.nth p n

theorem Nat.le_nth {p : ℕ → Prop} {n : ℕ} (h : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card) : n ≤ Nat.nth p n

theorem Nat.isLeast_nth {p : ℕ → Prop} {n : ℕ} (h : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card) : IsLeast {i : ℕ | p i ∧ ∀ k < n, Nat.nth p k < i} (Nat.nth p n)

theorem Nat.isLeast_nth_of_lt_card {p : ℕ → Prop} {n : ℕ} (hf : (setOf p).Finite) (hn : n < hf.toFinset.card) : IsLeast {i : ℕ | p i ∧ ∀ k < n, Nat.nth p k < i} (Nat.nth p n)

theorem Nat.isLeast_nth_of_infinite {p : ℕ → Prop} (hf : (setOf p).Infinite) (n : ℕ) : IsLeast {i : ℕ | p i ∧ ∀ k < n, Nat.nth p k < i} (Nat.nth p n)

theorem Nat.nth_eq_sInf (p : ℕ → Prop) (n : ℕ) : Nat.nth p n = sInf {x : ℕ | p x ∧ ∀ k < n, Nat.nth p k < x}

An alternative recursive definition of Nat.nth: Nat.nth s n is the infimum of x ∈ s such that Nat.nth s k < x for all k < n, if this set is nonempty. We do not assume that the set is nonempty because we use the same "garbage value" 0 both for sInf on ℕ and for Nat.nth s n for n ≥ #s.

theorem Nat.nth_zero {p : ℕ → Prop} : Nat.nth p 0 = sInf (setOf p)

@[simp]

theorem Nat.nth_zero_of_zero {p : ℕ → Prop} (h : p 0) : Nat.nth p 0 = 0

theorem Nat.nth_zero_of_exists {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) : Nat.nth p 0 = Nat.find h

theorem Nat.nth_eq_zero {p : ℕ → Prop} {n : ℕ} : Nat.nth p n = 0 ↔ p 0 ∧ n = 0 ∨ ∃ (hf : (setOf p).Finite), hf.toFinset.card ≤ n

theorem Nat.nth_eq_zero_mono {p : ℕ → Prop} (h₀ : ¬p 0) {a b : ℕ} (hab : a ≤ b) (ha : Nat.nth p a = 0) : Nat.nth p b = 0

theorem Nat.le_nth_of_lt_nth_succ {p : ℕ → Prop} {k a : ℕ} (h : a < Nat.nth p (k + 1)) (ha : p a) : a ≤ Nat.nth p k

theorem Nat.nth_mem_anti {p : ℕ → Prop} {a b : ℕ} (hab : a ≤ b) (h : p (Nat.nth p b)) : p (Nat.nth p a)

@[simp]

theorem Nat.count_nth_zero (p : ℕ → Prop) [DecidablePred p] : Nat.count p (Nat.nth p 0) = 0

theorem Nat.filter_range_nth_subset_insert (p : ℕ → Prop) [DecidablePred p] (k : ℕ) : Finset.filter (fun (n : ℕ) => p n) (Finset.range (Nat.nth p (k + 1))) ⊆ insert (Nat.nth p k) (Finset.filter (fun (n : ℕ) => p n) (Finset.range (Nat.nth p k)))

theorem Nat.filter_range_nth_eq_insert {p : ℕ → Prop} [DecidablePred p] {k : ℕ} (hlt : ∀ (hf : (setOf p).Finite), k + 1 < hf.toFinset.card) : Finset.filter (fun (n : ℕ) => p n) (Finset.range (Nat.nth p (k + 1))) = insert (Nat.nth p k) (Finset.filter (fun (n : ℕ) => p n) (Finset.range (Nat.nth p k)))

theorem Nat.filter_range_nth_eq_insert_of_finite {p : ℕ → Prop} [DecidablePred p] (hf : (setOf p).Finite) {k : ℕ} (hlt : k + 1 < hf.toFinset.card) : Finset.filter (fun (n : ℕ) => p n) (Finset.range (Nat.nth p (k + 1))) = insert (Nat.nth p k) (Finset.filter (fun (n : ℕ) => p n) (Finset.range (Nat.nth p k)))

theorem Nat.filter_range_nth_eq_insert_of_infinite {p : ℕ → Prop} [DecidablePred p] (hp : (setOf p).Infinite) (k : ℕ) : Finset.filter (fun (n : ℕ) => p n) (Finset.range (Nat.nth p (k + 1))) = insert (Nat.nth p k) (Finset.filter (fun (n : ℕ) => p n) (Finset.range (Nat.nth p k)))

theorem Nat.count_nth {p : ℕ → Prop} [DecidablePred p] {n : ℕ} (hn : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card) : Nat.count p (Nat.nth p n) = n

theorem Nat.count_nth_of_lt_card_finite {p : ℕ → Prop} [DecidablePred p] {n : ℕ} (hp : (setOf p).Finite) (hlt : n < hp.toFinset.card) : Nat.count p (Nat.nth p n) = n

theorem Nat.count_nth_of_infinite {p : ℕ → Prop} [DecidablePred p] (hp : (setOf p).Infinite) (n : ℕ) : Nat.count p (Nat.nth p n) = n

theorem Nat.surjective_count_of_infinite_setOf {p : ℕ → Prop} [DecidablePred p] (h : {n : ℕ | p n}.Infinite) : Function.Surjective (Nat.count p)

theorem Nat.count_nth_succ {p : ℕ → Prop} [DecidablePred p] {n : ℕ} (hn : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card) : Nat.count p (Nat.nth p n + 1) = n + 1

theorem Nat.count_nth_succ_of_infinite {p : ℕ → Prop} [DecidablePred p] (hp : (setOf p).Infinite) (n : ℕ) : Nat.count p (Nat.nth p n + 1) = n + 1

@[simp]

theorem Nat.nth_count {p : ℕ → Prop} [DecidablePred p] {n : ℕ} (hpn : p n) : Nat.nth p (Nat.count p n) = n

theorem Nat.nth_lt_of_lt_count {p : ℕ → Prop} [DecidablePred p] {n k : ℕ} (h : k < Nat.count p n) : Nat.nth p k < n

theorem Nat.le_nth_of_count_le {p : ℕ → Prop} [DecidablePred p] {n k : ℕ} (h : n ≤ Nat.nth p k) : Nat.count p n ≤ k

theorem Nat.count_eq_zero {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) {n : ℕ} : Nat.count p n = 0 ↔ n ≤ Nat.nth p 0

theorem Nat.nth_count_eq_sInf (p : ℕ → Prop) [DecidablePred p] (n : ℕ) : Nat.nth p (Nat.count p n) = sInf {i : ℕ | p i ∧ n ≤ i}

theorem Nat.le_nth_count' {p : ℕ → Prop} [DecidablePred p] {n : ℕ} (hpn : ∃ (k : ℕ), p k ∧ n ≤ k) : n ≤ Nat.nth p (Nat.count p n)

theorem Nat.le_nth_count {p : ℕ → Prop} [DecidablePred p] (hp : (setOf p).Infinite) (n : ℕ) : n ≤ Nat.nth p (Nat.count p n)

noncomputable def Nat.giCountNth {p : ℕ → Prop} [DecidablePred p] (hp : (setOf p).Infinite) : GaloisInsertion (Nat.count p) (Nat.nth p)

If a predicate p : ℕ → Prop is true for infinitely many numbers, then Nat.count p and Nat.nth p form a Galois insertion.

Equations

• Nat.giCountNth hp = GaloisInsertion.monotoneIntro ⋯ ⋯ ⋯ ⋯

theorem Nat.gc_count_nth {p : ℕ → Prop} [DecidablePred p] (hp : (setOf p).Infinite) : GaloisConnection (Nat.count p) (Nat.nth p)

theorem Nat.count_le_iff_le_nth {p : ℕ → Prop} [DecidablePred p] (hp : (setOf p).Infinite) {a b : ℕ} : Nat.count p a ≤ b ↔ a ≤ Nat.nth p b

theorem Nat.lt_nth_iff_count_lt {p : ℕ → Prop} [DecidablePred p] (hp : (setOf p).Infinite) {a b : ℕ} : a < Nat.count p b ↔ Nat.nth p a < b

theorem Nat.nth_of_forall {p : ℕ → Prop} {n : ℕ} (hp : ∀ n' ≤ n, p n') : Nat.nth p n = n

@[simp]

theorem Nat.nth_true (n : ℕ) : Nat.nth (fun (x : ℕ) => True) n = n

theorem Nat.nth_of_forall_not {p : ℕ → Prop} {n : ℕ} (hp : ∀ n' ≥ n, ¬p n') : Nat.nth p n = 0

@[simp]

theorem Nat.nth_false (n : ℕ) : Nat.nth (fun (x : ℕ) => False) n = 0