OAI/Analysis/Triangular/Certificate/AtomicMatrix.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.RValue line 10

   Source documentation

   The twenty dimensional finite atomic jet map.

   noncomputable abbrev RValue : Matrix (Fin 20) (Fin 20) ℝ := Construction.R

   Mentions: OAI.AtomicTriangular.Construction.R

2. def OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.literalR line 13

   Source documentation

   Rational enclosures for every entry of the finite atomic jet map.

   def literalR : Fin 20 → Fin 20 → RI :=
   …

3. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.literalR_refinement line 415
4. lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.literalR_mem line 420