norm_le_pow_iff_norm_lt_pow_add_one

English

For x ∈ ℚ_p and integer n, ‖x‖ ≤ p^n iff ‖x‖ < p^{n+1}.

Русский

Для x ∈ ℚ_p и целого n верно: ‖x‖ ≤ p^n тогда и только если ‖x‖ < p^{n+1}.

LaTeX

$$‖x‖ ≤ p^n \Leftrightarrow ‖x‖ < p^{n+1}$$

Lean4

theorem norm_le_pow_iff_norm_lt_pow_add_one (x : ℚ_[p]) (n : ℤ) : ‖x‖ ≤ (p : ℝ) ^ n ↔ ‖x‖ < (p : ℝ) ^ (n + 1) :=
  by
  have aux (n : ℤ) : 0 < ((p : ℝ) ^ n) := zpow_pos (mod_cast hp.1.pos) _
  by_cases hx0 : x = 0
  · simp [hx0, norm_zero, aux, le_of_lt (aux _)]
  rw [norm_eq_zpow_neg_valuation hx0]
  have h1p : 1 < (p : ℝ) := mod_cast hp.1.one_lt
  have H := zpow_right_strictMono₀ h1p
  rw [H.le_iff_le, H.lt_iff_lt, Int.lt_add_one_iff]

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