CircuitClauseIndependence.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The first gate case of bounded-independence circuit fooling. A clause is the complement of a Boolean cylinder. Restricting a wide clause to t distinct coordinates makes both its exceptional probabilities at most 2⁻ᵗ.

lemma OAI.TwoPointCorrelations.cubeAverage_pattern line 16
lemma OAI.TwoPointCorrelations.cubePattern_nonneg line 24
lemma OAI.TwoPointCorrelations.cubePattern_antitone line 29
lemma OAI.TwoPointCorrelations.TWiseUniformDensity.large_pattern_bound line 40
Source documentation
Exact t-wise independence bounds a cylinder of at least t coordinates, even when the cylinder uses more than t coordinates.
```
lemma TWiseUniformDensity.large_pattern_bound {n t : ℕ} {g : BooleanCube n → ℝ}
    (hg : TWiseUniformDensity g t) (hn : ∀ x, 0 ≤ g x)
    (S : Finset (Fin n)) (ht : t ≤ S.card) (z : BooleanCube n) :
    0 ≤ cubeAverage (fun x => g x * cubePattern S z x) ∧
      cubeAverage (fun x => g x * cubePattern S z x) ≤ 1 / (2 : ℝ) ^ t := by
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube, OAI.TwoPointCorrelations.TWiseUniformDensity, OAI.TwoPointCorrelations.cubeAverage, OAI.TwoPointCorrelations.cubePattern
theorem OAI.TwoPointCorrelations.TWiseUniformDensity.clause_error line 58
Source documentation
A clause, represented as the complement of its unique failing pattern, is fooled to error 2⁻ᵗ, independently of its width.
```
theorem TWiseUniformDensity.clause_error {n t : ℕ} {g : BooleanCube n → ℝ}
    (hg : TWiseUniformDensity g t) (hn : ∀ x, 0 ≤ g x)
    (hm : cubeAverage g = 1) (S : Finset (Fin n)) (z : BooleanCube n) :
    |cubeAverage (fun x => g x * (1 - cubePattern S z x)) -
      cubeAverage (fun x => 1 - cubePattern S z x)| ≤ 1 / (2 : ℝ) ^ t := by
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube, OAI.TwoPointCorrelations.TWiseUniformDensity, OAI.TwoPointCorrelations.cubeAverage, OAI.TwoPointCorrelations.cubePattern