OAI/Probability/SKBarriers/Replicas/MergedBranch.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SK.Analytic.BranchIncrement line 13
  2. abbrev OAI.SK.Analytic.TaggedBranchIncrement line 14
  3. def OAI.SK.Analytic.branchMass line 16
  4. def OAI.SK.Analytic.branchVector line 20
  5. def OAI.SK.Analytic.scalarIncrementChain line 24
  6. def OAI.SK.Analytic.scalarIncrementAverage line 28
  7. def OAI.SK.Analytic.taggedBranchChain line 32
  8. def OAI.SK.Analytic.taggedBranchAverage line 36
  9. def OAI.SK.Analytic.leftBranch line 42
  10. def OAI.SK.Analytic.rightBranch line 44
  11. theorem OAI.SK.Analytic.scalarIncrementChain_regular line 47
  12. theorem OAI.SK.Analytic.scalarStep_half_double line 53
  13. theorem OAI.SK.Analytic.scalarStepAverage_half_double line 57
  14. theorem OAI.SK.Analytic.taggedBranchChain_factor line 63
  15. theorem OAI.SK.Analytic.taggedBranchAverage_factor line 84
  16. def OAI.SK.Analytic.mergedBranches line 109
  17. theorem OAI.SK.Analytic.mergedBranches_left line 112
  18. theorem OAI.SK.Analytic.mergedBranches_right line 128
  19. theorem OAI.SK.Analytic.mergedBranches_monotone line 144