OAI/Probability/SKBarriers/Replicas/PairFactor.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.Analytic.pairMatrix line 16
  2. def OAI.SK.Analytic.pairFactor line 18
  3. def OAI.SK.Analytic.splitPairFactor line 21
  4. theorem OAI.SK.Analytic.pairFactor_covariance line 24
  5. theorem OAI.SK.Analytic.pairFactor_vector line 30
  6. theorem OAI.SK.Analytic.splitPairFactor_vector line 35
  7. theorem OAI.SK.Analytic.splitPairFactor_path line 41
  8. def OAI.SK.Analytic.pairMultiplier line 49
  9. theorem OAI.SK.Analytic.pairMultiplier_observable line 51
  10. theorem OAI.SK.Analytic.pairMultiplier_inner line 58
  11. theorem OAI.SK.Analytic.pairMatrix_square line 62
  12. theorem OAI.SK.Analytic.matrixInner_self line 66