Segments defined by a strictly monotonic function on Nat

Given a strictly monotonic function f : ℕ → ℕ and k : ℕ with k ≥ f 0, Nat.segment f k is the unique m : ℕ such that f m ≤ k < f (k + 1). Nat.segment f k is defined to be 0 for k < f 0. This file defines Nat.segment and proves various properties aboout it.

noncomputable def Nat.segment (f : ℕ → ℕ) (k : ℕ) : ℕ

The f-segment of k, where f : ℕ → ℕ will be assumed to be at least StrictMono.

Equations

• Nat.segment f k = Nat.count (fun (x : ℕ) => x ∈ Set.range f) (k + 1) - 1

theorem Nat.strictMono_infinite {f : ℕ → ℕ} (hm : StrictMono f) : (Set.range f).Infinite

Any strictly monotonic function f : ℕ → ℕ has an infinite range.

theorem Nat.infinite_strictMono {ns : Set ℕ} (h : ns.Infinite) : ∃ (f : ℕ → ℕ), StrictMono f ∧ Set.range f = ns

Any infinite subset of ℕ is the range of a strictly monotonic function.

theorem Nat.nth_succ_gap {p : ℕ → Prop} (hf : (setOf p).Infinite) (n k : ℕ) : k < nth p (n + 1) - nth p n → k > 0 → ¬p (k + nth p n)

There is a gap between two successive occurrences of a predicate p : ℕ → Prop, assuming p (as a set) is infinite.

theorem Nat.nth_of_strictMono {f : ℕ → ℕ} (hm : StrictMono f) (n : ℕ) : f n = nth (fun (x : ℕ) => x ∈ Set.range f) n

For a strictly monotonic function f : ℕ → ℕ, f n is exactly the n-th element of the range of f.

theorem Nat.count_notMem_range_pos {f : ℕ → ℕ} (h0 : f 0 = 0) (n : ℕ) (hn : n ∉ Set.range f) : count (fun (x : ℕ) => x ∈ Set.range f) n > 0

If f 0 = 0, then 0 is below any n not in the range of f.

theorem Nat.strictMono_range_gap {f : ℕ → ℕ} (hm : StrictMono f) {m k : ℕ} (hl : f m < k) (hu : k < f (m + 1)) : k ∉ Set.range f

For a strictly monotonic function f : ℕ → ℕ, no number (strictly) between f m and f (m + 1) is in the range of f.

@[simp]

theorem Nat.segment_idem {f : ℕ → ℕ} (hm : StrictMono f) (k : ℕ) : segment f (f k) = k

For a strictly monotonic function f : ℕ → ℕ, the segment of f k is k.

theorem Nat.segment_pre_zero {f : ℕ → ℕ} (hm : StrictMono f) {k : ℕ} (h : k < f 0) : segment f k = 0

For a strictly monotonic function f : ℕ → ℕ, segment f k = 0 for all k < f 0.

theorem Nat.segment_zero {f : ℕ → ℕ} (hm : StrictMono f) (h0 : f 0 = 0) : segment f 0 = 0

For a strictly monotonic function f : ℕ → ℕ with f 0 = 0, segment f 0 = 0.

theorem Nat.segment_plus_one {f : ℕ → ℕ} (h0 : f 0 = 0) (k : ℕ) : segment f k + 1 = count (fun (x : ℕ) => x ∈ Set.range f) (k + 1)

A slight restatement of the definition of segment which has proven useful.

theorem Nat.segment_upper_bound {f : ℕ → ℕ} (hm : StrictMono f) (h0 : f 0 = 0) (k : ℕ) : k < f (segment f k + 1)

For a strictly monotonic function f : ℕ → ℕ with f 0 = 0, k < f (segment f k + 1) for all k : ℕ.

theorem Nat.segment_lower_bound {f : ℕ → ℕ} (hm : StrictMono f) (h0 : f 0 = 0) (k : ℕ) : f (segment f k) ≤ k

For a strictly monotonic function f : ℕ → ℕ with f 0 = 0, f (segment f k) ≤ k for all k : ℕ.

theorem Nat.segment_range_val {f : ℕ → ℕ} (hm : StrictMono f) {m k : ℕ} (hl : f m ≤ k) (hu : k < f (m + 1)) : segment f k = m

For a strictly monotonic function f : ℕ → ℕ, all k satisfying f m ≤ k < f (m + 1) has segment f k = m.

theorem Nat.segment_galois_connection {f : ℕ → ℕ} (hm : StrictMono f) (h0 : f 0 = 0) : GaloisConnection f (segment f)

For a strictly monotonic function f : ℕ → ℕ with f 0 = 0, f and segment f form a Galois connection.

noncomputable def Nat.segment' (f : ℕ → ℕ) (k : ℕ) : ℕ

segment' is a helper function that will be proved to be equal to segment. It facilitates the proofs of some theorems below.

Equations

• Nat.segment' f k = Nat.segment (fun (x : ℕ) => f x - f 0) (k - f 0)

theorem Nat.segment'_eq_segment {f : ℕ → ℕ} (hm : StrictMono f) : segment' f = segment f

For a strictly monotonic function f : ℕ → ℕ, segment' f and segment f are actually equal.

theorem Nat.segment_zero' {f : ℕ → ℕ} (hm : StrictMono f) {k : ℕ} (h : k ≤ f 0) : segment f k = 0

For a strictly monotonic function f : ℕ → ℕ, segment f k = 0 for all k ≤ f 0.

theorem Nat.segment_upper_bound' {f : ℕ → ℕ} (hm : StrictMono f) {k : ℕ} (h : f 0 ≤ k) : k < f (segment f k + 1)

For a strictly monotonic function f : ℕ → ℕ, k < f (segment f k + 1) for all k ≥ f 0.

theorem Nat.segment_lower_bound' {f : ℕ → ℕ} (hm : StrictMono f) {k : ℕ} (h : f 0 ≤ k) : f (segment f k) ≤ k

For a strictly monotonic function f : ℕ → ℕ, f (segment f k) ≤ k for all k ≥ f 0.