English
For a vector of Diophantine functions f and a VectorAllP DiophFn g, there exists a Diophantine representation of their composition over a vector of variables.
Русский
Для вектора диагофантовых функций f и вектора диагофантных функций g существует диагофантовое представление их композиции над вектором переменных.
LaTeX
$$$$\mathrm{Dioph}(S) \Rightarrow \mathrm{Dioph}(\{v: Vector3 ((\alpha \to \mathbb{N}) \to \mathbb{N}) \to \mathbb{N} \mid \cdots\})$$$$
Lean4
theorem diophFn_compn :
∀ {n} {S : Set (α ⊕ (Fin2 n) → ℕ)} (_ : Dioph S) {f : Vector3 ((α → ℕ) → ℕ) n} (_ : VectorAllP DiophFn f),
Dioph {v : α → ℕ | (v ⊗ fun i => f i v) ∈ S}
| 0, S, d, f => fun _ =>
ext (reindex_dioph _ (id ⊗ Fin2.elim0) d) fun v =>
by
dsimp
-- TODO: `congr! 1; ext` should be equivalent to `congr! 1 with x` but that does not work.
congr! 1
ext x; obtain _ | _ | _ := x; rfl
| succ n, S, d, f =>
f.consElim fun f fl => by
simp only [vectorAllP_cons, and_imp]
exact fun df dfl =>
have : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S} :=
ext (diophFn_comp1 (reindex_dioph _ (some ∘ inl ⊗ none :: some ∘ inr) d) <| reindex_diophFn inl df) fun v =>
by
dsimp
-- TODO: `congr! 1; ext` should be equivalent to `congr! 1 with x`
-- but that does not work.
congr! 1
ext x; obtain _ | _ | _ := x <;> rfl
have : Dioph {v | (v ⊗ f v :: fun i : Fin2 n => fl i v) ∈ S} :=
@diophFn_compn n (fun v => S (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr)) this _ dfl
ext this fun v => by
dsimp
congr! 3 with x
obtain _ | _ | _ := x <;> rfl
