CircuitProbabilisticMethod.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The averaging step that chooses one polynomial approximation from a finite random construction, for an arbitrary input distribution.

lemma OAI.TwoPointCorrelations.FiniteLaw.exists_average_le line 13
theorem OAI.TwoPointCorrelations.exists_choice_of_pointwise_failure line 33
Source documentation
If every fixed input has small failure probability over random choices, one fixed choice has small failure probability for the supplied input law.
```
theorem exists_choice_of_pointwise_failure {α β : Type*} [Fintype α] [Fintype β]
    (μ : FiniteLaw α) (ν : FiniteLaw β) (E : α → β → Prop) {ε : ℝ}
    (hE : ∀ x, μ.probability (fun a => E a x) ≤ ε) :
    ∃ a, ν.probability (E a) ≤ ε := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw