OAI/NumberTheory/JointDickman/Probability/TwoSiteSplitModel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Two independent sites with two fair splits at each site

  1. structure OAI.JointDickman.TwoSiteSplit line 12
  2. def OAI.JointDickman.twoSiteSplitMass line 21
  3. def OAI.JointDickman.TwoSiteSplit.swap line 29
  4. theorem OAI.JointDickman.TwoSiteSplit.swap_swap line 32
  5. def OAI.JointDickman.twoSiteSwapEquiv line 36
  6. theorem OAI.JointDickman.twoSiteSplitMass_swap line 42
  7. theorem OAI.JointDickman.subsetRetentionMass_nonneg line 47
  8. theorem OAI.JointDickman.twoSiteSplitMass_nonneg line 51
  9. def OAI.JointDickman.twoSiteSplitProbability line 66
  10. theorem OAI.JointDickman.twoSiteSplitProbability_swap line 69
  11. def OAI.JointDickman.amplificationSplitGood line 81
  12. def OAI.JointDickman.bothAmplificationSplitsGood line 86
  13. theorem OAI.JointDickman.bothAmplificationSplitsGood_swap line 91