OAI/Analysis/Triangular/Certificate/AtomicCandidate.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.candidateNumerator line 13

    Source documentation

    Numerators for the rational inverse candidates of I - R and I + R.

    def candidateNumerator : Fin 2 → Fin 20 → Fin 20 → ℤ :=
…
  2. def OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.candidate line 60

    Source documentation

    The singleton interval of an inverse candidate entry.

    def candidate (side : Fin 2) (i j : Fin 20) : RI :=
…
  3. def OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.candidateValue line 64

    Source documentation

    The exact real value of an inverse candidate entry.

    def candidateValue (side : Fin 2) : Matrix (Fin 20) (Fin 20) ℝ :=
…
  4. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.candidate_mem line 67
  5. def OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.plusEpsilonNumerator line 71
  6. def OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.minusEpsilonNumerator line 72
  7. def OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.plusNormNumerator line 73
  8. def OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.minusNormNumerator line 74
  9. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.candidatePlus_bound line 76
  10. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.candidateMinus_bound line 80
  11. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.plus_epsilon_nonneg line 84
  12. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.plus_epsilon_lt_one line 87
  13. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.plus_norm_nonneg line 90
  14. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.plus_second_order_bound line 93
  15. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.minus_epsilon_nonneg line 99
  16. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.minus_epsilon_lt_one line 102
  17. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.minus_norm_nonneg line 105
  18. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.minus_second_order_bound line 108