Intervals with few specified positions

Consecutive chunks of an ordered support can be masked by intervals. Masking prevents an arbitrary completion of one chunk from changing the values specified in another chunk.

def Complexity.CircuitSparseSynthesis.Internal.supportCut {L : ℕ} (s : Finset (Fin L)) (rank : ℕ) : Fin (L + 1)

Position of the support element at rank, or the right endpoint L past the support.

Equations

• Complexity.CircuitSparseSynthesis.Internal.supportCut s rank = if h : rank < s.card then ((s.orderEmbOfFin ⋯) ⟨rank, h⟩).castSucc else Fin.last L

theorem Complexity.CircuitSparseSynthesis.Internal.supportCut_le_iff {L : ℕ} (s : Finset (Fin L)) (rank : ℕ) (i : Fin L) (hi : i ∈ s) : ↑(supportCut s rank) ≤ ↑i ↔ rank ≤ ↑((s.orderIsoOfFin ⋯).symm ⟨i, hi⟩)

theorem Complexity.CircuitSparseSynthesis.Internal.lt_supportCut_iff {L : ℕ} (s : Finset (Fin L)) (rank : ℕ) (i : Fin L) (hi : i ∈ s) : ↑i < ↑(supportCut s rank) ↔ ↑((s.orderIsoOfFin ⋯).symm ⟨i, hi⟩) < rank

def Complexity.CircuitSparseSynthesis.Internal.intervalChunk {L : ℕ} (s : Finset (Fin L)) (K block : ℕ) : Finset (Fin L)

Specified positions between consecutive cuts, at most K positions per chunk.

Equations

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

theorem Complexity.CircuitSparseSynthesis.Internal.mem_intervalChunk_iff {L : ℕ} (s : Finset (Fin L)) (K block : ℕ) (i : Fin L) (hi : i ∈ s) : i ∈ intervalChunk s K block ↔ block * K ≤ ↑((s.orderIsoOfFin ⋯).symm ⟨i, hi⟩) ∧ ↑((s.orderIsoOfFin ⋯).symm ⟨i, hi⟩) < (block + 1) * K

theorem Complexity.CircuitSparseSynthesis.Internal.intervalChunk_card {L : ℕ} (s : Finset (Fin L)) (K block : ℕ) : (intervalChunk s K block).card ≤ K

theorem Complexity.CircuitSparseSynthesis.Internal.exists_intervalChunk {L : ℕ} (s : Finset (Fin L)) (K : ℕ) (positive : 0 < K) (i : Fin L) (hi : i ∈ s) : ∃ (block : Fin (s.card / K + 1)), i ∈ intervalChunk s K ↑block