seq_norm_le — Mathlib

English

For every n, the integer-absolute norm of seq n, viewed in the K-side, is bounded by B: |N_Q(seq n)| ≤ B.

Русский

Для каждого n модуль нормы целых последовательности не превышает B: |N_Q(seq n)| ≤ B.

LaTeX

$$$\lvert \mathrm{N}_{\mathbb{Q}}(seq\ K\ w_1\ h_B\ n) \rvert ≤ B$$$

Lean4

/-- The terms of the sequence have norm bounded by `B`. -/
theorem seq_norm_le (n : ℕ) : Int.natAbs (Algebra.norm ℤ (seq K w₁ hB n : 𝓞 K)) ≤ B := by
  cases n with
  |
    zero =>
    have : 1 ≤ B := by
      contrapose! hB
      simp only [Nat.lt_one_iff.mp hB, CharP.cast_eq_zero, mul_zero, zero_le]
    simp only [ne_eq, seq, map_one, Int.natAbs_one, this]
  | succ n =>
    rw [← Nat.cast_le (α := ℚ), Int.cast_natAbs, Int.cast_abs, Algebra.coe_norm_int]
    exact (seq_next K w₁ hB (seq K w₁ hB n).prop).choose_spec.2.2

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