chore: replace phi by f to avoid potential conflict with Euler totient function (#116)

Author: ctchou

Cslib/Foundations/Data/Nat/Segment.lean

@@ -11,26 +11,26 @@ import Mathlib.Tactic
 open Function Set
 
 /-!
-Given a strictly monotonic function `φ : ℕ → ℕ` and `k : ℕ` with `k ≥ ϕ 0`,
-`Nat.segment φ k` is the unique `m : ℕ` such that `φ m ≤ k < φ (k + 1)`.
-`Nat.segment φ k` is defined to be 0 for `k < ϕ 0`.
+Given a strictly monotonic function `f : ℕ → ℕ` and `k : ℕ` with `k ≥ ϕ 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 < ϕ 0`.
 This file defines `Nat.segment` and proves various properties aboout it.
 -/
 @[scoped grind]
-noncomputable def Nat.segment (φ : ℕ → ℕ) (k : ℕ) : ℕ :=
+noncomputable def Nat.segment (f : ℕ → ℕ) (k : ℕ) : ℕ :=
   open scoped Classical in
-  Nat.count (· ∈ range φ) (k + 1) - 1
+  Nat.count (· ∈ range f) (k + 1) - 1
 
-variable {φ : ℕ → ℕ}
+variable {f : ℕ → ℕ}
 
-/-- Any strictly monotonic function `φ : ℕ → ℕ` has an infinite range. -/
-theorem Nat.strict_mono_infinite (hm : StrictMono φ) :
-    (range φ).Infinite :=
+/-- Any strictly monotonic function `f : ℕ → ℕ` has an infinite range. -/
+theorem Nat.strict_mono_infinite (hm : StrictMono f) :
+    (range f).Infinite :=
   infinite_range_of_injective hm.injective
 
 /-- Any infinite suset of `ℕ` is the range of a strictly monotonic function. -/
 theorem Nat.infinite_strict_mono {ns : Set ℕ} (h : ns.Infinite) :
-    ∃ φ : ℕ → ℕ, StrictMono φ ∧ range φ = ns :=
+    ∃ f : ℕ → ℕ, StrictMono f ∧ range f = ns :=
   ⟨Nat.nth (· ∈ ns), Nat.nth_strictMono h, Nat.range_nth_of_infinite h⟩
 
 /-- There is a gap between two successive occurrences of a predicate `p : ℕ → Prop`,
@@ -45,121 +45,121 @@ theorem Nat.nth_succ_gap {p : ℕ → Prop} (hf : (setOf p).Infinite) (n : ℕ)
   have h_m_n : m < n + 1 := by apply (Nat.nth_lt_nth hf).mp ; omega
   omega
 
-/-- For a strictly monotonic function `φ : ℕ → ℕ`, `φ n` is exactly the n-th
-element of the range of `φ`. -/
-theorem Nat.nth_of_strict_mono (hm : StrictMono φ) (n : ℕ) :
-    φ n = Nat.nth (· ∈ range φ) n := by
-  have (hf : (range φ).Finite) : False := hf.not_infinite (strict_mono_infinite hm)
+/-- For a strictly monotonic function `f : ℕ → ℕ`, `f n` is exactly the n-th
+element of the range of `f`. -/
+theorem Nat.nth_of_strict_mono (hm : StrictMono f) (n : ℕ) :
+    f n = Nat.nth (· ∈ range f) n := by
+  have (hf : (range f).Finite) : False := hf.not_infinite (strict_mono_infinite hm)
   rw [←Nat.nth_comp_of_strictMono hm] <;> first | grind | simp
 
 open scoped Classical in
-/-- If `φ 0 = 0`, then `0` is below any `n` not in the range of `φ`. -/
-theorem Nat.count_notin_range_pos (h0 : φ 0 = 0) (n : ℕ) (hn : n ∉ range φ) :
-    Nat.count (· ∈ range φ) n > 0 := by
-  have := Nat.count_monotone (· ∈ range φ) (show 1 ≤ n by grind)
+/-- If `f 0 = 0`, then `0` is below any `n` not in the range of `f`. -/
+theorem Nat.count_notin_range_pos (h0 : f 0 = 0) (n : ℕ) (hn : n ∉ range f) :
+    Nat.count (· ∈ range f) n > 0 := by
+  have := Nat.count_monotone (· ∈ range f) (show 1 ≤ n by grind)
   grind
 
-/-- For a strictly monotonic function `φ : ℕ → ℕ`, no number (strictly) between
-`φ m` and ` φ (m + 1)` is in the range of `φ`. -/
-theorem Nat.strict_mono_range_gap (hm : StrictMono φ) {m k : ℕ}
-    (hl : φ m < k) (hu : k < φ (m + 1)) : k ∉ range φ := by
+/-- For a strictly monotonic function `f : ℕ → ℕ`, no number (strictly) between
+`f m` and ` f (m + 1)` is in the range of `f`. -/
+theorem Nat.strict_mono_range_gap (hm : StrictMono f) {m k : ℕ}
+    (hl : f m < k) (hu : k < f (m + 1)) : k ∉ range f := by
   rw [nth_of_strict_mono hm m] at hl
   rw [nth_of_strict_mono hm (m + 1)] at hu
   have h_inf := strict_mono_infinite hm
-  have h_gap := nth_succ_gap (p := (· ∈ range φ)) h_inf m
-    (k - Nat.nth (· ∈ range φ) m) (by omega) (by omega)
-  rw [(show k - Nat.nth (· ∈ range φ) m + Nat.nth (· ∈ range φ) m = k by omega)] at h_gap
+  have h_gap := nth_succ_gap (p := (· ∈ range f)) h_inf m
+    (k - Nat.nth (· ∈ range f) m) (by omega) (by omega)
+  rw [(show k - Nat.nth (· ∈ range f) m + Nat.nth (· ∈ range f) m = k by omega)] at h_gap
   exact h_gap
 
-/-- For a strictly monotonic function `φ : ℕ → ℕ`, the segment of `φ k` is `k`. -/
+/-- For a strictly monotonic function `f : ℕ → ℕ`, the segment of `f k` is `k`. -/
 @[simp]
-theorem Nat.segment_idem (hm : StrictMono φ) (k : ℕ) :
-    segment φ (φ k) = k := by
+theorem Nat.segment_idem (hm : StrictMono f) (k : ℕ) :
+    segment f (f k) = k := by
   classical
-  have := Nat.count_nth_of_infinite (p := (· ∈ range φ)) <| strict_mono_infinite hm
+  have := Nat.count_nth_of_infinite (p := (· ∈ range f)) <| strict_mono_infinite hm
   have := nth_of_strict_mono hm
   grind [segment]
 
-/-- For a strictly monotonic function `φ : ℕ → ℕ`, `segment φ k = 0` for all `k < φ 0`. -/
+/-- For a strictly monotonic function `f : ℕ → ℕ`, `segment f k = 0` for all `k < f 0`. -/
 @[scoped grind =]
-theorem Nat.segment_pre_zero (hm : StrictMono φ) {k : ℕ} (h : k < φ 0) :
-    segment φ k = 0 := by
+theorem Nat.segment_pre_zero (hm : StrictMono f) {k : ℕ} (h : k < f 0) :
+    segment f k = 0 := by
   classical
-  have h1 : Nat.count (· ∈ range φ) (k + 1) = 0 := by
+  have h1 : Nat.count (· ∈ range f) (k + 1) = 0 := by
     apply Nat.count_of_forall_not
     rintro n h_n ⟨i, rfl⟩
     have := StrictMono.monotone hm <| zero_le i
     omega
   rw [segment, h1]
 
-/-- For a strictly monotonic function `φ : ℕ → ℕ` with `φ 0 = 0`, `segment φ 0 = 0`. -/
+/-- For a strictly monotonic function `f : ℕ → ℕ` with `f 0 = 0`, `segment f 0 = 0`. -/
 @[scoped grind =]
-theorem Nat.segment_zero (hm : StrictMono φ) (h0 : φ 0 = 0) :
-    segment φ 0 = 0 := by
-  calc _ = segment φ (φ 0) := by simp [h0]
+theorem Nat.segment_zero (hm : StrictMono f) (h0 : f 0 = 0) :
+    segment f 0 = 0 := by
+  calc _ = segment f (f 0) := by simp [h0]
        _ = _ := by simp [segment_idem hm]
 
 open scoped Classical in
 /-- A slight restatement of the definition of `segment` which has proven useful. -/
-theorem Nat.segment_plus_one (h0 : φ 0 = 0) (k : ℕ) :
-    segment φ k + 1 = Nat.count (· ∈ range φ) (k + 1) := by
-  suffices _ : Nat.count (· ∈ range φ) (k + 1) ≠ 0 by unfold segment ; omega
+theorem Nat.segment_plus_one (h0 : f 0 = 0) (k : ℕ) :
+    segment f k + 1 = Nat.count (· ∈ range f) (k + 1) := by
+  suffices _ : Nat.count (· ∈ range f) (k + 1) ≠ 0 by unfold segment ; omega
   apply Nat.count_ne_iff_exists.mpr ; use 0 ; grind
 
-/-- For a strictly monotonic function `φ : ℕ → ℕ` with `φ 0 = 0`,
-`k < φ (segment φ k + 1)` for all `k : ℕ`. -/
-theorem Nat.segment_upper_bound (hm : StrictMono φ) (h0 : φ 0 = 0) (k : ℕ) :
-    k < φ (segment φ k + 1) := by
+/-- For a strictly monotonic function `f : ℕ → ℕ` with `f 0 = 0`,
+`k < f (segment f k + 1)` for all `k : ℕ`. -/
+theorem Nat.segment_upper_bound (hm : StrictMono f) (h0 : f 0 = 0) (k : ℕ) :
+    k < f (segment f k + 1) := by
   classical
-  rw [nth_of_strict_mono hm (segment φ k + 1), segment_plus_one h0 k]
-  suffices _ : k + 1 ≤ Nat.nth (· ∈ range φ) (Nat.count (· ∈ range φ) (k + 1)) by omega
+  rw [nth_of_strict_mono hm (segment f k + 1), segment_plus_one h0 k]
+  suffices _ : k + 1 ≤ Nat.nth (· ∈ range f) (Nat.count (· ∈ range f) (k + 1)) by omega
   apply Nat.le_nth_count
   exact strict_mono_infinite hm
 
-/-- For a strictly monotonic function `φ : ℕ → ℕ` with `φ 0 = 0`,
-`φ (segment φ k) ≤ k` for all `k : ℕ`. -/
-theorem Nat.segment_lower_bound (hm : StrictMono φ) (h0 : φ 0 = 0) (k : ℕ) :
-    φ (segment φ k) ≤ k := by
+/-- For a strictly monotonic function `f : ℕ → ℕ` with `f 0 = 0`,
+`f (segment f k) ≤ k` for all `k : ℕ`. -/
+theorem Nat.segment_lower_bound (hm : StrictMono f) (h0 : f 0 = 0) (k : ℕ) :
+    f (segment f k) ≤ k := by
   classical
-  rw [nth_of_strict_mono hm (segment φ k), segment]
-  rcases Classical.em (k ∈ range φ) with h_k | h_k
+  rw [nth_of_strict_mono hm (segment f k), segment]
+  rcases Classical.em (k ∈ range f) with h_k | h_k
   · simp_all [Nat.count_succ_eq_succ_count]
-  · have h1 : Nat.count (· ∈ range φ) k > 0 := count_notin_range_pos h0 k h_k
-    have h2 : Nat.count (· ∈ range φ) (k + 1) = Nat.count (· ∈ range φ) k :=
+  · have h1 : Nat.count (· ∈ range f) k > 0 := count_notin_range_pos h0 k h_k
+    have h2 : Nat.count (· ∈ range f) (k + 1) = Nat.count (· ∈ range f) k :=
       Nat.count_succ_eq_count h_k
     rw [h2]
-    suffices _ : Nat.nth (· ∈ range φ) (Nat.count (· ∈ range φ) k - 1) < k by omega
+    suffices _ : Nat.nth (· ∈ range f) (Nat.count (· ∈ range f) k - 1) < k by omega
     apply Nat.nth_lt_of_lt_count
     omega
 
-/-- For a strictly monotonic function `φ : ℕ → ℕ`, all `k` satisfying `φ m ≤ k < φ (m + 1)`
-has `segment φ k = m`. -/
-theorem Nat.segment_range_val (hm : StrictMono φ) {m k : ℕ}
-    (hl : φ m ≤ k) (hu : k < φ (m + 1)) : segment φ k = m := by
+/-- For a strictly monotonic function `f : ℕ → ℕ`, all `k` satisfying `f m ≤ k < f (m + 1)`
+has `segment f k = m`. -/
+theorem Nat.segment_range_val (hm : StrictMono f) {m k : ℕ}
+    (hl : f m ≤ k) (hu : k < f (m + 1)) : segment f k = m := by
   classical
-  obtain (rfl | hu') := show φ m = k ∨ φ m < k by omega
+  obtain (rfl | hu') := show f m = k ∨ f m < k by omega
   · exact segment_idem hm m
-  · obtain ⟨j, h_j, rfl⟩ : ∃ j < φ (m + 1) - φ m - 1, k = j + φ m + 1 := ⟨k - φ m - 1, by omega⟩
+  · obtain ⟨j, h_j, rfl⟩ : ∃ j < f (m + 1) - f m - 1, k = j + f m + 1 := ⟨k - f m - 1, by omega⟩
     induction j
     case zero =>
-      have : Nat.count (· ∈ range φ) (φ m + 1 + 1) = Nat.count (· ∈ range φ) (φ m + 1) := by
-        have := strict_mono_range_gap hm (show φ m < φ m + 1 by grind)
+      have : Nat.count (· ∈ range f) (f m + 1 + 1) = Nat.count (· ∈ range f) (f m + 1) := by
+        have := strict_mono_range_gap hm (show f m < f m + 1 by grind)
         grind
       have := nth_of_strict_mono hm m
       grind [Nat.count_nth_of_infinite, strict_mono_infinite]
     case succ j _ =>
-      have := strict_mono_range_gap hm (show φ m < j + 1 + φ m     by grind)
-      have := strict_mono_range_gap hm (show φ m < j + 1 + φ m + 1 by grind)
+      have := strict_mono_range_gap hm (show f m < j + 1 + f m     by grind)
+      have := strict_mono_range_gap hm (show f m < j + 1 + f m + 1 by grind)
       grind
 
-/-- For a strictly monotonic function `φ : ℕ → ℕ` with `φ 0 = 0`,
-`φ` and `segment φ` form a Galois connection. -/
-theorem Nat.segment_galois_connection (hm : StrictMono φ) (h0 : φ 0 = 0) :
-    GaloisConnection φ (segment φ) := by
+/-- For a strictly monotonic function `f : ℕ → ℕ` with `f 0 = 0`,
+`f` and `segment f` form a Galois connection. -/
+theorem Nat.segment_galois_connection (hm : StrictMono f) (h0 : f 0 = 0) :
+    GaloisConnection f (segment f) := by
   intro m k ; constructor
   · intro h
     by_contra! h_con
-    have h1 : segment φ k + 1 ≤ m := by omega
+    have h1 : segment f k + 1 ≤ m := by omega
     have := (StrictMono.le_iff_le hm).mpr h1
     have := segment_upper_bound hm h0 k
     omega
@@ -171,38 +171,38 @@ theorem Nat.segment_galois_connection (hm : StrictMono φ) (h0 : φ 0 = 0) :
 
 /-- Nat.segment' is a helper function that will be proved to be equal to `Nat.segment`.
 It facilitates the proofs of some theorems below. -/
-noncomputable def Nat.segment' (φ : ℕ → ℕ) (k : ℕ) : ℕ :=
-  segment (φ · - φ 0) (k - φ 0)
+noncomputable def Nat.segment' (f : ℕ → ℕ) (k : ℕ) : ℕ :=
+  segment (f · - f 0) (k - f 0)
 
-private lemma base_zero_shift (φ : ℕ → ℕ) :
-    (φ · - φ 0) 0 = 0 := by
+private lemma base_zero_shift (f : ℕ → ℕ) :
+    (f · - f 0) 0 = 0 := by
   simp
 
-private lemma base_zero_strict_mono (hm : StrictMono φ) :
-    StrictMono (φ · - φ 0) := by
+private lemma base_zero_strict_mono (hm : StrictMono f) :
+    StrictMono (f · - f 0) := by
   intro m n h_m_n ; simp
   have := hm h_m_n
-  have : φ 0 ≤ φ m := by simp [StrictMono.le_iff_le hm]
-  have : φ 0 ≤ φ n := by simp [StrictMono.le_iff_le hm]
+  have : f 0 ≤ f m := by simp [StrictMono.le_iff_le hm]
+  have : f 0 ≤ f n := by simp [StrictMono.le_iff_le hm]
   omega
 
-/-- For a strictly monotonic function `φ : ℕ → ℕ`,
-`segment' φ` and `segment φ` are actually equal. -/
-theorem Nat.segment'_eq_segment (hm : StrictMono φ) :
-    segment' φ = segment φ := by
+/-- For a strictly monotonic function `f : ℕ → ℕ`,
+`segment' f` and `segment f` are actually equal. -/
+theorem Nat.segment'_eq_segment (hm : StrictMono f) :
+    segment' f = segment f := by
   classical
   ext k ; unfold segment'
-  rcases (show k < φ 0 ∨ k ≥ φ 0 by omega) with h_k | h_k
-  · have : k - φ 0 = 0 := by grind
+  rcases (show k < f 0 ∨ k ≥ f 0 by omega) with h_k | h_k
+  · have : k - f 0 = 0 := by grind
     grind
   unfold segment ; congr 1
   simp only [Nat.count_eq_card_filter_range]
-  suffices h : ∃ f, BijOn f
-      ({x ∈ Finset.range (k - φ 0 + 1) | x ∈ range fun x => φ x - φ 0}).toSet
-      ({x ∈ Finset.range (k + 1) | x ∈ range φ}).toSet by
-    obtain ⟨f, h_bij⟩ := h
-    exact BijOn.finsetCard_eq f h_bij
-  refine ⟨fun n ↦ n + φ 0, ?_, ?_, ?_⟩
+  suffices h : ∃ g, BijOn g
+      ({x ∈ Finset.range (k - f 0 + 1) | x ∈ range fun x => f x - f 0}).toSet
+      ({x ∈ Finset.range (k + 1) | x ∈ range f}).toSet by
+    obtain ⟨g, h_bij⟩ := h
+    exact BijOn.finsetCard_eq g h_bij
+  refine ⟨fun n ↦ n + f 0, ?_, ?_, ?_⟩
   · intro n ; simp only [mem_range, Finset.coe_filter, Finset.mem_range, mem_setOf_eq]
     rintro ⟨h_n, i, rfl⟩
     have := StrictMono.monotone hm <| zero_le i
@@ -211,24 +211,24 @@ theorem Nat.segment'_eq_segment (hm : StrictMono φ) :
   · intro n ; simp only [mem_range, Finset.coe_filter, Finset.mem_range, mem_setOf_eq, mem_image]
     rintro ⟨h_n, i, rfl⟩
     have := StrictMono.monotone hm <| zero_le i
-    refine ⟨φ i - φ 0, ⟨by omega, i, rfl⟩, by omega⟩
+    refine ⟨f i - f 0, ⟨by omega, i, rfl⟩, by omega⟩
 
-/-- For a strictly monotonic function `φ : ℕ → ℕ`, `segment φ k = 0` for all `k ≤ φ 0`. -/
-theorem Nat.segment_zero' (hm : StrictMono φ) {k : ℕ} (h : k ≤ φ 0) :
-    segment φ k = 0 := by
-  rw [← segment'_eq_segment hm, segment', (show k - φ 0 = 0 by omega)]
+/-- For a strictly monotonic function `f : ℕ → ℕ`, `segment f k = 0` for all `k ≤ f 0`. -/
+theorem Nat.segment_zero' (hm : StrictMono f) {k : ℕ} (h : k ≤ f 0) :
+    segment f k = 0 := by
+  rw [← segment'_eq_segment hm, segment', (show k - f 0 = 0 by omega)]
   grind
 
-/-- For a strictly monotonic function `φ : ℕ → ℕ`, `k < φ (segment φ k + 1)` for all `k ≥ φ 0`. -/
-theorem Nat.segment_upper_bound' (hm : StrictMono φ) {k : ℕ} (h : φ 0 ≤ k) :
-    k < φ (segment φ k + 1) := by
+/-- For a strictly monotonic function `f : ℕ → ℕ`, `k < f (segment f k + 1)` for all `k ≥ f 0`. -/
+theorem Nat.segment_upper_bound' (hm : StrictMono f) {k : ℕ} (h : f 0 ≤ k) :
+    k < f (segment f k + 1) := by
   rw [← segment'_eq_segment hm, segment']
-  have := segment_upper_bound (base_zero_strict_mono hm) (base_zero_shift φ) (k - φ 0)
+  have := segment_upper_bound (base_zero_strict_mono hm) (base_zero_shift f) (k - f 0)
   omega
 
-/-- For a strictly monotonic function `φ : ℕ → ℕ`, `φ (segment φ k) ≤ k` for all `k ≥ φ 0`. -/
-theorem Nat.segment_lower_bound' (hm : StrictMono φ) {k : ℕ} (h : φ 0 ≤ k) :
-    φ (segment φ k) ≤ k := by
+/-- For a strictly monotonic function `f : ℕ → ℕ`, `f (segment f k) ≤ k` for all `k ≥ f 0`. -/
+theorem Nat.segment_lower_bound' (hm : StrictMono f) {k : ℕ} (h : f 0 ≤ k) :
+    f (segment f k) ≤ k := by
   rw [← segment'_eq_segment hm, segment']
-  have := segment_lower_bound (base_zero_strict_mono hm) (base_zero_shift φ) (k - φ 0)
+  have := segment_lower_bound (base_zero_strict_mono hm) (base_zero_shift f) (k - f 0)
   omega