OAI/Analysis/Triangular/Certificate/AtomicResidual.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Interval multiplication with floor and ceiling at the common integer grid.

   def exactMul (a b : RI) : RI :=
   …

   Mentions: OAI.AtomicTriangular.b

2. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.exactMul_mem line 17
3. def OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.exactMatrixMul line 35
4. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.exactMatrixMul_mem line 38
5. def OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.system line 45

   Source documentation

   Side zero is the sum block I−R; side one is the difference block I+R.

   def system (side : Fin 2) (i j : Fin 20) : RI :=
   …

6. def OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.systemValue line 49
7. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.system_mem line 52
8. def OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.residual line 61

   Source documentation

   The full right residual of the rational inverse candidate.

   def residual (side : Fin 2) (i j : Fin 20) : RI :=
   …

9. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.residual_mem line 64
10. def OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.residualCorrection line 69
11. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.residualCorrection_mem line 72
12. def OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.inverseEnclosure line 80

    Source documentation

    Second-order inverse enclosure, padded by the exact radius 2·10⁻¹⁷.

    def inverseEnclosure (side : Fin 2) (i j : Fin 20) : RI :=
    …