OAI/Analysis/Conductivity/Variational/MatrixOperator.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.matrixOperator line 23
  2. lemma OAI.ScalarConductivity.matrixOperator_apply line 26
  3. lemma OAI.ScalarConductivity.operatorMatrix_matrixOperator line 29
  4. def OAI.ScalarConductivity.rotatedDirection line 33
  5. def OAI.ScalarConductivity.rotatedPhase line 35
  6. lemma OAI.ScalarConductivity.rotated_normalization line 38
  7. lemma OAI.ScalarConductivity.rotatedDirection_apply line 44
  8. lemma OAI.ScalarConductivity.rotatedPhase_single line 48
  9. lemma OAI.ScalarConductivity.normalStretch_decomposition line 52
  10. lemma OAI.ScalarConductivity.rotated_diagonal_single line 58
  11. lemma OAI.ScalarConductivity.splitJacobian_rotated line 63
  12. lemma OAI.ScalarConductivity.det_orthogonal_conjugate line 79
  13. lemma OAI.ScalarConductivity.conjugated_push line 88
  14. lemma OAI.ScalarConductivity.rotated_increment_annihilates line 101
  15. lemma OAI.ScalarConductivity.exists_two_state_primitive line 118
  16. lemma OAI.ScalarConductivity.exists_transition_width line 148