CircuitGateApproximation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A single fixed polynomial approximates an arbitrarily wide AND gate under any supplied finite input law. The sampling and its error bound are explicit, and the polynomial degree is bounded by the number of sampled linear factors.

lemma OAI.TwoPointCorrelations.FiniteLaw.probability_mono line 15
theorem OAI.TwoPointCorrelations.gate_pointwise_failure line 26
theorem OAI.TwoPointCorrelations.exists_and_gate_approximation line 57
Source documentation
The probabilistic method fixes all samples simultaneously for the input law, without imposing a condition on that law.
```
theorem exists_and_gate_approximation {α : Type*} [Fintype α]
    (ν : FiniteLaw α) (k s : ℕ) (b : α → Fin k → Bool) :
    ∃ x : GateSamplingChoices k k s,
      ν.probability (fun y =>
        sampledAndPolynomial x (fun i => if b y i then 1 else 0) ≠ boolAndValue (b y)) ≤
          (7 / 8 : ℝ) ^ s := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.GateSamplingChoices, OAI.TwoPointCorrelations.sampledAndPolynomial, OAI.TwoPointCorrelations.boolAndValue