OAI/Analysis/TracialSplitting/BlockAveraging.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentMain.kraus_coefficient_norm line 22
2. lemma OAI.CurrentMain.scalarRowGram_eigenvalue_le_of_trace line 31
3. lemma OAI.CurrentMain.scalarRowGram_kraus_trace line 42
4. theorem OAI.CurrentMain.spectral_row_block_of_spectral_bound line 52
5. theorem OAI.CurrentMain.raw_kraus_spectral_block line 121
6. theorem OAI.CurrentMain.layer_energy_global line 207
7. lemma OAI.CurrentMain.kraus_average_trace line 276
8. theorem OAI.CurrentMain.weighted_family_of_kraus_average line 287