OAI/Computability/Logspace/ProbabilityDecision.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Conditioning at the initial configuration and deterministic separation of acceptance probabilities.

From OpenAI, Exact Derandomization of Logarithmic Space: L = RL = BPL.

  1. structure OAI.ExactDerandomization.Stage.Wares line 21

    Source documentation

    constants chosen once for the analytic part of the algorithm.

    structure Wares where
…
  2. def OAI.ExactDerandomization.Stage.Wares.density line 28
  3. def OAI.ExactDerandomization.Stage.Wares.levels line 29
  4. def OAI.ExactDerandomization.Stage.Wares.tolls line 30
  5. def OAI.ExactDerandomization.Stage.Wares.top line 31
  6. def OAI.ExactDerandomization.Stage.Wares.ceiling line 32
  7. structure OAI.ExactDerandomization.Stage.Wares.Proof line 33
  8. lemma OAI.ExactDerandomization.Stage.Wares.choose line 39
  9. def OAI.ExactDerandomization.Stage.Raw.H line 51
  10. lemma OAI.ExactDerandomization.Stage.Raw.honestly line 54
  11. lemma OAI.ExactDerandomization.Stage.Raw.fits line 78
  12. lemma OAI.ExactDerandomization.Stage.Raw.answer line 79
  13. structure OAI.ExactDerandomization.Stage.Matter line 86
  14. def OAI.ExactDerandomization.Stage.Matter.s line 94
  15. def OAI.ExactDerandomization.Stage.Matter.x0 line 96
  16. def OAI.ExactDerandomization.Stage.Matter.i line 97
  17. def OAI.ExactDerandomization.Stage.Matter.view line 98
  18. def OAI.ExactDerandomization.Stage.Matter.top line 99
  19. def OAI.ExactDerandomization.Stage.Matter.d line 100
  20. def OAI.ExactDerandomization.Stage.Matter.ready line 102
  21. lemma OAI.ExactDerandomization.Stage.Matter.cseq line 105
  22. lemma OAI.ExactDerandomization.Stage.Matter.lineup line 130
  23. lemma OAI.ExactDerandomization.Stage.Matter.identity line 138
  24. lemma OAI.ExactDerandomization.Stage.Matter.rank_allow line 170
  25. abbrev OAI.ExactDerandomization.Stage.Matter.oracleV line 197
  26. abbrev OAI.ExactDerandomization.Stage.Matter.polls line 199
  27. lemma OAI.ExactDerandomization.Stage.Matter.reachesB line 201
  28. lemma OAI.ExactDerandomization.Stage.Matter.origin line 208
  29. lemma OAI.ExactDerandomization.Stage.Matter.designate line 210
  30. lemma OAI.ExactDerandomization.Stage.Matter.designate_est line 261
  31. lemma OAI.ExactDerandomization.Stage.Matter.place line 288
  32. def OAI.ExactDerandomization.Stage.Matter.jury line 296
  33. lemma OAI.ExactDerandomization.Stage.Matter.yard line 297
  34. def OAI.ExactDerandomization.Stage.Matter.evidence line 313
  35. lemma OAI.ExactDerandomization.Stage.Matter.probes line 314
  36. lemma OAI.ExactDerandomization.Stage.Matter.tally_eq line 325

    Source documentation

    Compare arithmetic rather than doing probability tests.

    lemma tally_eq (f:Pool n→ℝ) :
    (∑ s∈ univ.filter (fun s:Pool n=>m.polls s),f s) =
        ((univ.filter (fun s:Pool n=>m.polls s)).card:ℝ) * m.evidence f := by
…

    Mentions: OAI.ExactDerandomization.Stage.Matter.s

  37. lemma OAI.ExactDerandomization.Stage.Matter.quorum line 338