max_log_padicValNat_succ_eq_log_succ

English

For any prime p, the maximum of log_p(n) and v_p(n+1) equals log_p(n+1).

Русский

Для любого простого p максимум из log_p(n) и v_p(n+1) равен log_p(n+1).

LaTeX

$$$\\forall p\\in \\mathbb{N},\\ n\\in \\mathbb{N},\\ p\\text{ prime} \\Rightarrow \\max\\big(\\log p n,\\operatorname{padicValNat} p (n+1)\\big) = \\log p (n+1)$$$

Lean4

theorem max_log_padicValNat_succ_eq_log_succ (n : ℕ) [hp : Fact p.Prime] :
    max (log p n) (padicValNat p (n + 1)) = log p (n + 1) :=
  by
  apply le_antisymm (max_le (le_log_of_pow_le hp.out.one_lt (pow_log_le_add_one p n)) (padicValNat_le_nat_log (n + 1)))
  rw [le_max_iff, or_iff_not_imp_left, not_le]
  intro h
  replace h := le_antisymm (add_one_le_iff.mpr (lt_pow_of_log_lt hp.out.one_lt h)) (pow_log_le_self p n.succ_ne_zero)
  rw [h, padicValNat.prime_pow, ← h]

Похожие утверждения