OAI/Probability/SignedSweeps/TensorDensity.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SignedSweeps.FiniteComplexHilbert line 13
  2. instance OAI.SignedSweeps.(instance at line 32) line 32
  3. def OAI.SignedSweeps.scalarHilbert line 34
  4. def OAI.SignedSweeps.tensorHilbert line 36
  5. def OAI.SignedSweeps.tensorHilbertPower line 39
  6. def OAI.SignedSweeps.tensorOperator line 43
  7. lemma OAI.SignedSweeps.tensorOperator_mul line 48
  8. lemma OAI.SignedSweeps.tensorOperator_one line 57
  9. lemma OAI.SignedSweeps.tensorOperator_adjoint line 65
  10. lemma OAI.SignedSweeps.tensorOperator_positive line 75
  11. lemma OAI.SignedSweeps.positiveRoot_one line 82
  12. lemma OAI.SignedSweeps.tensorOperator_positiveRoot line 87
  13. lemma OAI.SignedSweeps.tensorOperator_norm_sq_le line 96
  14. lemma OAI.SignedSweeps.tensor_normalized_density_bound line 110