OAI/Analysis/MutuallyUnbiased/Certificate/Integer.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Integer coefficient checking after denominator clearing. The arithmetic checker uses only integer operations; its interpretation remains over arbitrary real moment vectors.

  1. abbrev OAI.MUB6.Certificate.Integer.Sparse line 12
  2. def OAI.MUB6.Certificate.Integer.Sparse.eval line 18
  3. def OAI.MUB6.Certificate.Integer.Sparse.coeff line 21
  4. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_nil line 24
  5. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_cons line 25
  6. theorem OAI.MUB6.Certificate.Integer.Sparse.coeff_nil line 27
  7. theorem OAI.MUB6.Certificate.Integer.Sparse.coeff_cons line 28
  8. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_eq_sum_coeff line 31
  9. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_le_abs_sum line 42
  10. inductive OAI.MUB6.Certificate.Integer.Combination line 57
  11. def OAI.MUB6.Certificate.Integer.Combination.eval line 66
  12. def OAI.MUB6.Certificate.Integer.Combination.coeff line 71
  13. theorem OAI.MUB6.Certificate.Integer.Combination.eval_eq_sum_coeff line 76
  14. theorem OAI.MUB6.Certificate.Integer.Combination.eval_zero_of_rows line 86
  15. theorem OAI.MUB6.Certificate.Integer.Combination.eval_eq_of_coeff_eq line 93
  16. theorem OAI.MUB6.Certificate.Integer.Combination.target_zero_of_coeff_eq line 100
  17. theorem OAI.MUB6.Certificate.Integer.Combination.consequence line 110

    Source documentation

    An integer coefficient comparison proves a sparse target relation.

    theorem consequence [Fintype ι] [DecidableEq ι]
    (rows : κ → Sparse ι) (source : Combination κ) (target : Sparse ι)
    (h : ∀ i, Sparse.coeff target i = coeff rows i source)
    (x : ι → ℝ) (hrows : ∀ k, Sparse.eval (rows k) x = 0) :
    Sparse.eval target x = 0 := by
…

    Mentions: OAI.MUB6.Certificate.Integer.Sparse, OAI.MUB6.Certificate.Integer.Combination, OAI.MUB6.Certificate.Integer.Sparse.coeff, OAI.MUB6.Certificate.Integer.Combination.coeff, OAI.MUB6.Certificate.Integer.Sparse.eval