OAI/Analysis/BoundedHochschild/MatrixDisplacement.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Projection displacement and energy-decreasing matrix extensions.

  1. lemma OAI.HochschildQuantization.positive_contraction_bound_of_projections line 39
  2. lemma OAI.HochschildQuantization.contraction_bound_of_projections line 72
  3. def OAI.HochschildQuantization.commutatorGNS line 94
  4. lemma OAI.HochschildQuantization.commutatorGNS_apply line 99
  5. lemma OAI.HochschildQuantization.commutatorGNS_bound line 101
  6. lemma OAI.HochschildQuantization.norm_sub_trace_le_of_projection_commutators line 111
  7. theorem OAI.HochschildQuantization.exists_projection_displacement line 139
  8. lemma OAI.HochschildMatrixSystems.MatrixSystem.coe_entry_star line 166
  9. lemma OAI.HochschildMatrixSystems.MatrixSystem.coe_entry_mul line 171
  10. lemma OAI.HochschildMatrixSystems.MatrixSystem.coe_sum_diagonal line 178
  11. def OAI.HochschildMatrixSystems.MatrixSystem.extend line 184
  12. lemma OAI.HochschildMatrixSystems.MatrixSystem.extend_entry line 213
  13. lemma OAI.HochschildMatrixSystems.MatrixSystem.entry_sum_extension line 218
  14. lemma OAI.HochschildMatrixSystems.MatrixSystem.commutant_entry_sum_extension line 223
  15. lemma OAI.HochschildMatrixSystems.MatrixSystem.extension_expectation_commutes line 229
  16. lemma OAI.HochschildMatrixSystems.MatrixSystem.extension_residual_orthogonal line 245
  17. lemma OAI.HochschildMatrixSystems.MatrixSystem.extension_pythagoras line 254
  18. lemma OAI.HochschildMatrixSystems.MatrixSystem.extension_gns_contract line 280
  19. lemma OAI.HochschildQuantization.commutator_gns_le line 305
  20. lemma OAI.HochschildQuantization.exists_matrix_displacement line 315
  21. lemma OAI.HochschildMatrixSystems.MatrixSystem.commutant_gns_norm line 366
  22. theorem OAI.HochschildMatrixSystems.MatrixSystem.exists_energy_decreasing_extension line 375