normEDSRec — Mathlib

English

normEDSRec defines a recursion principle for a normalised elliptic divisibility sequence on natural numbers, using base values at 0–4 and two recursive schemes to propagate to all natural indices.

Русский

normEDSRec задаёт принцип рекурсии для нормализованной эллиптической последовательности делимости на множество натуральных чисел, задавая базовые значения для 0–4 и две схемы рекурсии для перехода к всем индексам.

LaTeX

$$$\text{normEDSRec}\;\{P:\mathbb{N}\to \text{Sort}\} \ P(0)\land P(1)\land P(2)\land P(3)\land P(4) \land\ (\forall m\; (P(m+1)\to P(m+2)\to P(m+3)\to P(m+4)\to P(m+5)\to P(2(m+3)))) \land\ (\forall m\; (P(m+1)\to P(m+2)\to P(m+3)\to P(m+4)\to P(2(m+2)+1))) \rightarrow \forall n\; P(n)$$$

Lean4

/-- Recursion principle for a normalised EDS: if we have
* `P 0`, `P 1`, `P 2`, `P 3`, and `P 4`,
* for all `m : ℕ` we can prove `P (2 * (m + 3))` from `P (m + 1)`, `P (m + 2)`, `P (m + 3)`,
  `P (m + 4)`, and `P (m + 5)`, and
* for all `m : ℕ` we can prove `P (2 * (m + 2) + 1)` from `P (m + 1)`, `P (m + 2)`, `P (m + 3)`,
  and `P (m + 4)`,
then we have `P n` for all `n : ℕ`. -/
@[elab_as_elim]
noncomputable def normEDSRec {P : ℕ → Sort u} (zero : P 0) (one : P 1) (two : P 2) (three : P 3) (four : P 4)
    (even : ∀ m : ℕ, P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3)))
    (odd : ∀ m : ℕ, P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)) (n : ℕ) : P n :=
  normEDSRec' zero one two three four (fun _ ih => by apply even <;> exact ih _ <| by linarith only)
    (fun _ ih => by apply odd <;> exact ih _ <| by linarith only) n

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