OAI/Analysis/TracialSplitting/SpectralBlocks.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CurrentMain.spectral_row_block line 18
  2. def OAI.CurrentMain.sortedIndex line 86
  3. lemma OAI.CurrentMain.sortedIndex_monotone line 89
  4. def OAI.CurrentMain.ProjectionRow.sorted line 96
  5. lemma OAI.CurrentMain.ProjectionRow.sorted_weighted_sum line 99
  6. lemma OAI.CurrentMain.ProjectionRow.layer_sum line 103
  7. lemma OAI.CurrentMain.ProjectionRow.subrow_entry_error line 108
  8. lemma OAI.CurrentMain.ProjectionRow.subrow_compression line 114
  9. lemma OAI.CurrentMain.traceOneNorm_unitary_conjugate line 136
  10. lemma OAI.CurrentMain.trace_re_le_oneNorm line 145
  11. lemma OAI.CurrentMain.trace_mass_perturb line 150
  12. lemma OAI.CurrentMain.trace_central_perturb line 158
  13. lemma OAI.CurrentMain.layer_energy_perturb line 175
  14. lemma OAI.CurrentMain.block_tolerances line 215
  15. def OAI.CurrentMain.rowCorrectionError line 262
  16. def OAI.CurrentMain.rowCompressionError line 265
  17. structure OAI.CurrentMain.BlockControl line 269
  18. lemma OAI.CurrentMain.exists_blockControl line 280
  19. lemma OAI.CurrentMain.rowCompressionError_nonneg line 285
  20. theorem OAI.CurrentMain.raw_spectral_block line 293
  21. def OAI.CurrentMain.upperEmbedding line 361
  22. lemma OAI.CurrentMain.upperColumn_nonempty line 366
  23. lemma OAI.CurrentMain.ProjectionRow.sum_pos_weights line 373
  24. lemma OAI.CurrentMain.ProjectionRow.upperEmbedding_range line 386
  25. lemma OAI.CurrentMain.ProjectionRow.positive_layer_sum line 392
  26. lemma OAI.CurrentMain.ProjectionRow.positive_layer_energy line 403