Finite chunks of a support

Enumerating a finite support in chunks gives at most card / size + 1 patterns, each containing at most size positions.

def Complexity.CircuitSparseSynthesis.Internal.tupleSupport {α : Type} [DecidableEq α] {K : ℕ} (v : Fin K → Option α) : Finset α

The positions named by a tuple, ignoring empty entries and repetitions.

Equations

• Complexity.CircuitSparseSynthesis.Internal.tupleSupport v = Finset.univ.biUnion fun (i : Fin K) => (v i).toFinset

@[simp]

theorem Complexity.CircuitSparseSynthesis.Internal.mem_tupleSupport {α : Type} [DecidableEq α] {K : ℕ} (v : Fin K → Option α) (a : α) : a ∈ tupleSupport v ↔ ∃ (i : Fin K), v i = some a

theorem Complexity.CircuitSparseSynthesis.Internal.tupleSupport_card {α : Type} [DecidableEq α] {K : ℕ} (v : Fin K → Option α) : (tupleSupport v).card ≤ K

noncomputable def Complexity.CircuitSparseSynthesis.Internal.chunkTuple {α : Type} (s : Finset α) (K block : ℕ) : Fin K → Option α

One chunk of an enumeration of s, padded with empty entries.

Equations

• Complexity.CircuitSparseSynthesis.Internal.chunkTuple s K block i = if h : block * K + ↑i < s.card then some ↑(s.equivFin.symm ⟨block * K + ↑i, h⟩) else none

theorem Complexity.CircuitSparseSynthesis.Internal.mem_chunkTuple_iff {α : Type} [DecidableEq α] (s : Finset α) (K : ℕ) (positive : 0 < K) (a : α) : (∃ (block : Fin (s.card / K + 1)), a ∈ tupleSupport (chunkTuple s K ↑block)) ↔ a ∈ s

theorem Complexity.CircuitSparseSynthesis.Internal.sum_div_le_div_sum {ι : Type} (s : Finset ι) (f : ι → ℕ) (K : ℕ) : ∑ i ∈ s, f i / K ≤ (∑ i ∈ s, f i) / K