FiniteSelection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.FiniteLaw.exists_good_simultaneously line 21
Source documentation
All finite tests and any additional table event can be imposed at once. The only premise is the actual expectation/probability estimate, not the existence of a good table.
```
theorem exists_good_simultaneously (μ : FiniteLaw α) (f : J → α → ℝ)
    (hf : ∀ j a, 0 ≤ f j a) (bad : α → Prop) [DecidablePred bad]
    {ε : ℝ} (hε : 0 < ε)
    (h : (∑ j, μ.expect (f j)) + ε*μ.prob bad < ε) :
    ∃ a, ¬bad a ∧ ∀ j, f j a < ε := by
…
```
Mentions: OAI.HyperbolicObstruction.FiniteLaw
def OAI.HyperbolicObstruction.FiniteLaw.prod line 46
Source documentation
Product law for the independent master and six-letter arrays.
```
def prod (μ : FiniteLaw α) (ν : FiniteLaw β) : FiniteLaw (α × β) where
…
```
Mentions: OAI.HyperbolicObstruction.FiniteLaw
lemma OAI.HyperbolicObstruction.FiniteLaw.expect_prod line 54
lemma OAI.HyperbolicObstruction.FiniteLaw.expect_prod_fst line 64
lemma OAI.HyperbolicObstruction.FiniteLaw.expect_prod_snd line 69