Weighted approximate frontier bounds

Coherent sweeps remember that splicing also splices the message trace. This stronger property holds for networks with unique satisfying assignments and makes state deletion exact. The disjoint peeling argument was contributed by Sam McGuire.

noncomputable def Complexity.Frontier.sumOn {α : Type u_1} [Finite α] (w : α → ℝ) (S : Set α) : ℝ

The sum of a real weight over a finite set.

Equations

• Complexity.Frontier.sumOn w S = ∑ x ∈ ⋯.toFinset, w x

@[simp]

theorem Complexity.Frontier.sumOn_empty {α : Type u_1} [Finite α] (w : α → ℝ) : sumOn w ∅ = 0

theorem Complexity.Frontier.sumOn_nonneg {α : Type u_1} [Finite α] {w : α → ℝ} (hw : ∀ (x : α), 0 ≤ w x) (S : Set α) : 0 ≤ sumOn w S

theorem Complexity.Frontier.sumOn_sdiff {α : Type u_1} [Finite α] (w : α → ℝ) {S T : Set α} (h : T ⊆ S) : sumOn w S = sumOn w T + sumOn w (S \ T)

theorem Complexity.Frontier.abs_sumOn_le {α : Type u_1} [Finite α] {w : α → ℝ} {a : ℝ} (hw : ∀ (x : α), |w x| ≤ a) (S : Set α) : |sumOn w S| ≤ a * ↑S.ncard

def Complexity.Frontier.RectangleBudget {ι : Type u_2} {U : Type u_3} [Finite ι] [Finite U] (w cost : (ι → U) → ℝ) (KL KR : ℕ) : Prop

A pointwise nonnegative budget controls the signed weight of every thick rectangle.

Equations

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

def Complexity.Frontier.Sweep.Coherent {ι : Type u_2} {U : Type u_3} {M : Type u_4} {S : Set (ι → U)} (P : Sweep S M) : Prop

Splicing inputs through a shared message splices their whole message traces.

Equations

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

theorem Complexity.Frontier.Sweep.Coherent.peers_eq_rectangle {ι : Type u_2} {U : Type u_3} {M : Type u_4} {S : Set (ι → U)} (P : Sweep S M) (hP : P.Coherent) (t : ℕ) (x : ι → U) : P.peers t x = rectangle (P.revealed t) (P.pastSide t x) (P.futureSide t x)

A message class in a coherent sweep is exactly its rectangular hull.

noncomputable def Complexity.Frontier.Sweep.erase {ι : Type u_2} {U : Type u_3} {M : Type u_4} {S : Set (ι → U)} (P : Sweep S M) (hP : P.Coherent) (t : ℕ) (x : ι → U) : Sweep (S \ P.peers t x) M

Deleting a message class preserves a coherent sweep on exactly the remaining inputs.

Equations

• P.erase hP t x = { length := P.length, revealed := P.revealed, revealed_zero := ⋯, revealed_length := ⋯, message := P.message, message_length := ⋯, splice := ⋯ }

theorem Complexity.Frontier.Sweep.Coherent.erase {ι : Type u_2} {U : Type u_3} {M : Type u_4} {S : Set (ι → U)} (P : Sweep S M) (hP : P.Coherent) (t : ℕ) (x : ι → U) : (P.erase hP t x).Coherent

theorem Complexity.Frontier.Sweep.transitionCount_erase_le {ι : Type u_2} {U : Type u_3} {M : Type u_4} {S : Set (ι → U)} (P : Sweep S M) [Finite ι] [Finite U] (hP : P.Coherent) (t : ℕ) (x : ι → U) : (P.erase hP t x).transitionCount ≤ P.transitionCount

theorem Complexity.Frontier.Sweep.transitionCount_pos {ι : Type u_2} {U : Type u_3} {M : Type u_4} {S : Set (ι → U)} (P : Sweep S M) [Finite ι] [Finite U] (hL : 0 < P.length) (hS : S.Nonempty) : 0 < P.transitionCount

theorem Complexity.Frontier.Sweep.abs_sumOn_le_of_budget {ι : Type u_2} {U : Type u_3} {M : Type u_4} {S : Set (ι → U)} (P : Sweep S M) [Finite ι] [Finite U] (hP : P.Coherent) (hL : 0 < P.length) {KL KR : ℕ} (hKL : 1 < KL) (hKR : 1 < KR) {w cost : (ι → U) → ℝ} {a : ℝ} (ha : 0 ≤ a) (hw : ∀ (x : ι → U), |w x| ≤ a) (hc : ∀ (x : ι → U), 0 ≤ cost x) (hrect : RectangleBudget w cost KL KR) : |sumOn w S| ≤ sumOn cost S + a * ↑((KL - 1) * (KR - 1) * P.transitionCount)

Weighted peeling. A shared nonnegative budget on thick rectangles is paid once; only the residual thin sweep pays its maximum atom times the transition count.