Interpolating arbitrary samples with small circuits

At 2 * p input bits, every sample of at most 2 ^ p points is shattered by circuits of size at most ⌊(1 + ε) * 2 ^ p / p⌋, for all sufficiently large p. Labels are prescribed only on the sample. The circuit supports form a set family in Mathlib's shattering and VC-dimension API.

noncomputable def Complexity.CircuitSparseSynthesis.circuitSupports (n budget : ℕ) : Finset (Finset (Fin n → Bool))

Supports of scalar Boolean functions computable with at most budget gates.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.CircuitSparseSynthesis.exists_interpolating_circuit (ε : ℝ) (positive : 0 < ε) : ∃ (p₀ : ℕ), ∀ p ≥ p₀, ∀ (domain : Finset (Fin (2 * p) → Bool)), domain.card ≤ 2 ^ p → ∀ (labels : ↥domain → Bool), ∃ (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature (2 * p) 1), ↑c.size ≤ (1 + ε) * 2 ^ p / ↑p ∧ ∀ (x : ↥domain), c.eval Cslib.Circuits.Boolean.interpretation (↑x) 0 = labels x

Every labeling of a square-root-sized sample has a circuit of the partial-synthesis size.

theorem Complexity.CircuitSparseSynthesis.circuitSupports_shatters (ε : ℝ) (positive : 0 < ε) : ∃ (p₀ : ℕ), ∀ p ≥ p₀, ∀ (domain : Finset (Fin (2 * p) → Bool)), domain.card ≤ 2 ^ p → (circuitSupports (2 * p) ⌊(1 + ε) * 2 ^ p / ↑p⌋₊).Shatters domain

Every sample of the allowed size is shattered, with no geometric condition on its points.

theorem Complexity.CircuitSparseSynthesis.le_vcDim_circuitSupports (ε : ℝ) (positive : 0 < ε) : ∃ (p₀ : ℕ), ∀ p ≥ p₀, 2 ^ p ≤ (circuitSupports (2 * p) ⌊(1 + ε) * 2 ^ p / ↑p⌋₊).vcDim

At this gate budget the circuit class has VC dimension at least 2 ^ p.