OAI/Probability/SKGap/Terminal/TerminalMatrixTransfer.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.coupling_symmetric line 14
  2. lemma OAI.SKGap.coupling_norm_from_goe line 19
  3. lemma OAI.SKGap.coupling_principal_norm_from_goe line 28
  4. lemma OAI.SKGap.row_square_restrict line 49
  5. lemma OAI.SKGap.tanh_principal_norm line 56
  6. lemma OAI.SKGap.tanh_square_principal_norm line 69
  7. lemma OAI.SKGap.conditionalExpectation_flip line 90
  8. lemma OAI.SKGap.conditionalExpectation_idem line 96
  9. lemma OAI.SKGap.expectation_flip_average line 106
  10. lemma OAI.SKGap.conditionalExpectation_adjoint line 113
  11. lemma OAI.SKGap.conditionalExpectation_mul_invariant line 127
  12. lemma OAI.SKGap.conditionalExpectation_const line 135
  13. lemma OAI.SKGap.expectation_conditionalExpectation line 141
  14. lemma OAI.SKGap.expectation_projection_square line 146
  15. def OAI.SKGap.heatBathGenerator line 160
  16. lemma OAI.SKGap.expectation_sum line 163
  17. lemma OAI.SKGap.heatBathGenerator_form line 169
  18. lemma OAI.SKGap.heatBathGenerator_adjoint line 178
  19. lemma OAI.SKGap.conditionalDifference_zero_iff line 189
  20. lemma OAI.SKGap.flip_invariant_constant line 203
  21. lemma OAI.SKGap.dirichlet_eq_zero_iff line 229