English
For integers p prime and natural numbers n,i,j with i ≤ n and j < p^{n-i}, a certain equality of indices holds: j - v_p(j+1) + n = i + j + (n - i - v_p(j+1)).
Русский
Пусть p — простое, n,i,j натуральные; при i ≤ n и j < p^{n-i} выполняется числовое равенство: j - v_p(j+1) + n = i + j + (n - i - v_p(j+1)).
LaTeX
$$$\forall (n,i,j)\;(i\le n)\; (hj: j < p^{n-i})\; \Rightarrow j - v_p(j+1) + n = i + j + (n - i - v_p(j+1)).$$$
Lean4
/-- A key numerical identity needed for the proof of `WittVector.map_frobeniusPoly`. -/
theorem key₂ {n i j : ℕ} (hi : i ≤ n) (hj : j < p ^ (n - i)) : j - v p (j + 1) + n = i + j + (n - i - v p (j + 1)) :=
by
generalize h : v p (j + 1) = m
rsuffices ⟨h₁, h₂⟩ : m ≤ n - i ∧ m ≤ j
·
rw [tsub_add_eq_add_tsub h₂, add_comm i j, add_tsub_assoc_of_le (h₁.trans (Nat.sub_le n i)), add_assoc,
tsub_right_comm, add_comm i, tsub_add_cancel_of_le (le_tsub_of_add_le_right ((le_tsub_iff_left hi).mp h₁))]
have hle : p ^ m ≤ j + 1 := h ▸ Nat.le_of_dvd j.succ_pos (pow_multiplicity_dvd _ _)
exact
⟨(Nat.pow_le_pow_iff_right hp.1.one_lt).1 (hle.trans hj),
Nat.le_of_lt_succ ((m.lt_pow_self hp.1.one_lt).trans_le hle)⟩
