OAI/Probability/SKBarriers/Replicas/VectorBranch.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.Analytic.vectorTranslation line 16
  2. theorem OAI.SK.Analytic.vectorStep_regular line 19
  3. def OAI.SK.Analytic.vectorIncrementChain line 23
  4. def OAI.SK.Analytic.vectorIncrementAverage line 27
  5. theorem OAI.SK.Analytic.vectorIncrementChain_regular line 32
  6. theorem OAI.SK.Analytic.vectorIncrementChain_append line 38
  7. theorem OAI.SK.Analytic.vectorIncrementAverage_append line 44
  8. theorem OAI.SK.Analytic.vectorIncrementChain_ofFn line 51
  9. theorem OAI.SK.Analytic.vectorIncrementAverage_ofFn line 59
  10. theorem OAI.SK.Analytic.vectorStep_prod_left line 69
  11. theorem OAI.SK.Analytic.vectorStep_prod_right line 80
  12. theorem OAI.SK.Analytic.vectorStepAverage_prod_left line 91
  13. theorem OAI.SK.Analytic.vectorStepAverage_prod_right line 100
  14. abbrev OAI.SK.Analytic.ProductIncrement line 110
  15. def OAI.SK.Analytic.productMass line 112
  16. def OAI.SK.Analytic.productVector line 116
  17. def OAI.SK.Analytic.productLeft line 120
  18. def OAI.SK.Analytic.productRight line 123
  19. def OAI.SK.Analytic.productBranchChain line 126
  20. def OAI.SK.Analytic.productBranchAverage line 129
  21. theorem OAI.SK.Analytic.vectorStep_half_double line 133
  22. theorem OAI.SK.Analytic.vectorStepAverage_half_double line 137
  23. theorem OAI.SK.Analytic.productBranchChain_factor line 141
  24. theorem OAI.SK.Analytic.productBranchAverage_factor line 162