Equality.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A fixed-precision deterministic estimator and the equality L = RL = BPL.

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

lemma OAI.ExactDerandomization.Umbra.Scope.Sane.shard line 29
lemma OAI.ExactDerandomization.Umbra.Scope.Sane.plump line 47
theorem OAI.ExactDerandomization.Umbra.Scope.Sane.delivered line 58
theorem OAI.ExactDerandomization.Umbra.fixed_precision_estimator line 70
Source documentation
One deterministic estimator works for every input and every finite sampling environment, with additive error at most 1 / 32 for the normalized oracle value.
```
theorem fixed_precision_estimator (r:Rock q w h)(e:r.w.Proof)(hp:6≤r.pad)(he:e.T.bank≤Est.box r.pad)(hS:r.P.Space):
    ∃ f:PT ℕ ℕ, Kn f ∧ ∀ (x:Word) (s:Pool (r.n x)),
                        let m:=r.matter0 x
…
```
Mentions: OAI.ExactDerandomization.Est.box, OAI.ExactDerandomization.Word
theorem OAI.ExactDerandomization.BPL_subset_L line 83
Source documentation
Every bounded-error probabilistic logspace language has a deterministic logspace decider.
```
theorem BPL_subset_L : BPL ⊆ L:=by
…
```
Mentions: OAI.ExactDerandomization.BPL, OAI.ExactDerandomization.L
theorem OAI.ExactDerandomization.exact_logarithmic_space_derandomization line 104
Source documentation
Deterministic, one-sided randomized, and two-sided randomized logarithmic space coincide.
Distinct definitions of this name: ComparatorChallenges/LogspaceEquality.lean:136 (different declaration text). Qualify references as OAI.ExactDerandomization.exact_logarithmic_space_derandomization@path.
```
theorem exact_logarithmic_space_derandomization :
     L=RL ∧ RL=BPL:=by
…
```
Mentions: OAI.ExactDerandomization.L, OAI.ExactDerandomization.RL, OAI.ExactDerandomization.BPL