div_dioph — Mathlib

English

DiophFn f / g is Diophantine.

Русский

Диофантово деление функцию f на g сохраняет диофантовость.

LaTeX

$$$$\\forall \\{\\alpha : Type\\} {f,g:(\\alpha \\to \\mathbb{N})\\to \\mathbb{N},\\;\\mathrm{DiophFn}\\,f \\to \\mathrm{DiophFn}\\,g \\to \\mathrm{DiophFn}\\bigl(\\lambda v. f(v) / g(v)\\bigr).$$$$

Lean4

/-- Diophantine functions are closed under integer division. -/
theorem div_dioph : DiophFn fun v => f v / g v :=
  have : Dioph fun v : Vector3 ℕ 3 => v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2 :=
    (D&2 D= D.0 D∧ D&0 D= D.0) D∨ D&0 D* D&2 D≤ D&1 D∧ D&1 D< (D&0 D+ D.1) D* D&2
  diophFn_comp2 df dg <|
    (diophFn_vec _).2 <|
      ext this <|
        (vectorAll_iff_forall _).1 fun z x y =>
          show y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z
            by
            refine Iff.trans ?_ eq_comm
            exact
              y.eq_zero_or_pos.elim
                (fun y0 => by
                  rw [y0, Nat.div_zero]
                  exact
                    ⟨fun o => (o.resolve_right fun ⟨_, h2⟩ => Nat.not_lt_zero _ h2).right, fun z0 => Or.inl ⟨rfl, z0⟩⟩)
                fun ypos =>
                Iff.trans ⟨fun o => o.resolve_left fun ⟨h1, _⟩ => Nat.ne_of_gt ypos h1, Or.inr⟩
                  (le_antisymm_iff.trans <|
                      and_congr (Nat.le_div_iff_mul_le ypos) <|
                        Iff.trans ⟨lt_succ_of_le, le_of_lt_succ⟩ (div_lt_iff_lt_mul ypos)).symm

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