OAI/Probability/SATVariance/PairEvolution.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RandomKSAT.RootData line 13
  2. abbrev OAI.RandomKSAT.PairState line 15
  3. def OAI.RandomKSAT.DataSatisfies line 17
  4. def OAI.RandomKSAT.dataStep line 20
  5. def OAI.RandomKSAT.fibre line 23
  6. def OAI.RandomKSAT.dataMask line 26
  7. lemma OAI.RandomKSAT.fibre_dataStep line 29
  8. lemma OAI.RandomKSAT.rootSatisfies_zero line 34
  9. lemma OAI.RandomKSAT.satisfies_cast line 42
  10. def OAI.RandomKSAT.refreshData line 47
  11. lemma OAI.RandomKSAT.favg_refreshData line 50
  12. lemma OAI.RandomKSAT.fibre_refreshData line 59
  13. def OAI.RandomKSAT.forcedReward line 72
  14. lemma OAI.RandomKSAT.forcedReward_nonneg line 75
  15. lemma OAI.RandomKSAT.forcedReward_le_one line 78
  16. lemma OAI.RandomKSAT.forcedReward_le_alive line 81
  17. def OAI.RandomKSAT.pairEvolution line 93
  18. lemma OAI.RandomKSAT.pairEvolution_fibre_operator line 97
  19. lemma OAI.RandomKSAT.pairEvolution_drift line 117
  20. lemma OAI.RandomKSAT.rootPath_square line 126
  21. def OAI.RandomKSAT.pairPrefix line 140
  22. lemma OAI.RandomKSAT.pairPrefix_zero line 144
  23. lemma OAI.RandomKSAT.pairPrefix_cons line 147
  24. def OAI.RandomKSAT.dataRewards line 156
  25. lemma OAI.RandomKSAT.dataRewards_cons line 159
  26. lemma OAI.RandomKSAT.rootPath_eq_rewards line 166
  27. lemma OAI.RandomKSAT.rootRewards_avg line 183
  28. def OAI.RandomKSAT.noiseWordEquiv line 193
  29. lemma OAI.RandomKSAT.favg_noiseWord line 201
  30. lemma OAI.RandomKSAT.dataSatisfies_refresh_fixed line 207
  31. def OAI.RandomKSAT.fibrePrefix line 218
  32. lemma OAI.RandomKSAT.fibre_pairPrefix_refresh line 223
  33. def OAI.RandomKSAT.flipRoot line 231
  34. lemma OAI.RandomKSAT.flipRoot_ne line 233
  35. def OAI.RandomKSAT.UniqueTrue line 239
  36. lemma OAI.RandomKSAT.rootSatisfies_flip line 242
  37. lemma OAI.RandomKSAT.rootSize_one_unique line 257
  38. lemma OAI.RandomKSAT.trueRoot_eq line 263
  39. def OAI.RandomKSAT.TestAt line 270
  40. lemma OAI.RandomKSAT.refreshPart_test line 273
  41. def OAI.RandomKSAT.Available line 282
  42. lemma OAI.RandomKSAT.forcedPrefix_testKills line 285