OAI/Analysis/HyperbolicCones/PencilBlocks.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Paper256.BlockPencil line 13

   Source documentation

   The actual finite blocks after common-kernel compression and fixed diagonal congruence.

   structure BlockPencil (K : Set Ambient) where
   …

   Mentions: OAI.Paper256.Ambient

2. def OAI.Paper256.BlockPencil.matrix line 35
3. def OAI.Paper256.BlockPencil.scaled line 40
4. def OAI.Paper256.BlockPencil.limit line 46
5. theorem OAI.Paper256.BlockPencil.matrix_isHermitian line 50
6. theorem OAI.Paper256.BlockPencil.limit_isHermitian line 57