OAI/Probability/BinarySweep/MatrixBounds/HilbertBlockTrace.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Irrep.fiber_sum line 20
2. lemma OAI.BinaryCoordinateSweeps.Irrep.fiber_identity line 32
3. lemma OAI.BinaryCoordinateSweeps.Irrep.hilbertBlock_mul line 39
4. lemma OAI.BinaryCoordinateSweeps.Irrep.hilbertBlock_one line 50
5. lemma OAI.BinaryCoordinateSweeps.Irrep.hilbertBlock_sum line 57
6. lemma OAI.BinaryCoordinateSweeps.Irrep.hilbertBlock_smul line 63
7. lemma OAI.BinaryCoordinateSweeps.Irrep.fiber_adjoint line 68
8. lemma OAI.BinaryCoordinateSweeps.Irrep.hilbertBlock_adjoint line 77
9. def OAI.BinaryCoordinateSweeps.Irrep.hilbertBlocksHom line 84
10. lemma OAI.BinaryCoordinateSweeps.Irrep.trace_hilbertBlocks line 90
11. lemma OAI.BinaryCoordinateSweeps.Irrep.trace_hilbertBlocks_prod line 100
12. theorem OAI.BinaryCoordinateSweeps.Irrep.hilbert_block_trace_holder line 112
13. theorem OAI.BinaryCoordinateSweeps.Irrep.evenMoment_blocks_le line 126