OAI/Probability/SKBarriers/Replicas/PairRecursion.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SK.Analytic.gaussianStep_half_double line 19
  2. theorem OAI.SK.Analytic.gaussianAverage_half_double line 31
  3. theorem OAI.SK.Analytic.gaussianAverage_add_prefix line 37
  4. def OAI.SK.Analytic.vectorStepAverage line 52
  5. def OAI.SK.Analytic.pairIndependentStep line 56
  6. def OAI.SK.Analytic.pairIndependentAverage line 59
  7. theorem OAI.SK.Analytic.vectorStep_pair_right line 62
  8. theorem OAI.SK.Analytic.vectorStep_pair_left line 81
  9. theorem OAI.SK.Analytic.pairIndependentStep_separate line 98
  10. theorem OAI.SK.Analytic.vectorStepAverage_pair_right line 104
  11. theorem OAI.SK.Analytic.vectorStepAverage_pair_left line 117
  12. theorem OAI.SK.Analytic.pairIndependentAverage_product line 130
  13. theorem OAI.SK.Analytic.vectorStep_pair_diagonal line 137
  14. theorem OAI.SK.Analytic.vectorStepAverage_pair_diagonal line 149