OAI/Probability/SATVariance/BystanderVariance.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RandomKSAT.bystanders_perm_right line 13
  2. def OAI.RandomKSAT.shuffleVar line 20
  3. lemma OAI.RandomKSAT.shuffleVar_nonneg line 23
  4. lemma OAI.RandomKSAT.shuffleVar_perm line 26
  5. lemma OAI.RandomKSAT.shuffleVar_append_lower line 31
  6. lemma OAI.RandomKSAT.favg_shuffleVar_lower line 38
  7. def OAI.RandomKSAT.outsideWindow line 46
  8. lemma OAI.RandomKSAT.outsideWindow_nonneg line 49
  9. lemma OAI.RandomKSAT.bystander_variance line 52
  10. lemma OAI.RandomKSAT.bystanders_map line 100
  11. def OAI.RandomKSAT.chosenIsolates line 124
  12. lemma OAI.RandomKSAT.chosenIsolates_subset line 127
  13. lemma OAI.RandomKSAT.chosenIsolates_card line 132
  14. def OAI.RandomKSAT.bystanderList line 137
  15. def OAI.RandomKSAT.activeList line 140
  16. lemma OAI.RandomKSAT.selected_bystanders line 143
  17. lemma OAI.RandomKSAT.selected_perm line 152
  18. lemma OAI.RandomKSAT.bystanderList_length line 172
  19. lemma OAI.RandomKSAT.selected_lengths line 176
  20. lemma OAI.RandomKSAT.selected_variance line 181
  21. lemma OAI.RandomKSAT.min_isolate_mean_lower line 214