Pruning a coherent sweep

Deleting transitions, rather than arbitrary inputs, preserves the rectangular structure needed for weighted peeling. A nested reveal order is essential here: a splice inherits each transition from one of its two parents. The resulting error is the weight of inputs using a deleted transition, which can be bounded by a union bound on transition tails.

theorem Complexity.Frontier.sumOn_le_sum_of_cover {α : Type u_1} [Finite α] {w : α → ℝ} (hw : ∀ (x : α), 0 ≤ w x) {S : Set α} {T : ℕ} {B : ℕ → Set α} (hcover : ∀ x ∈ S, ∃ t < T, x ∈ B t) : sumOn w S ≤ ∑ t ∈ Finset.range T, sumOn w (B t)

A finite union bound for nonnegative weights, allowing overlapping exceptional sets.

def Complexity.Frontier.Sweep.kept {ι : Type u_2} {U : Type u_3} {M : Type u_4} {S : Set (ι → U)} (P : Sweep S M) (T : (t : ℕ) → Set (M × M × (↑(P.newly t) → U))) : Set (ι → U)

Inputs all of whose transitions survive the selected pruning.

Equations

• P.kept T = {x : ι → U | x ∈ S ∧ ∀ t < P.length, P.transition t x ∈ T t}

theorem Complexity.Frontier.Sweep.transition_splice {ι : Type u_2} {U : Type u_3} {M : Type u_4} {S : Set (ι → U)} (P : Sweep S M) (hP : P.Coherent) (hmono : Monotone P.revealed) (t : ℕ) {x y : ι → U} (hx : x ∈ S) (hy : y ∈ S) (hxy : P.message t x = P.message t y) (z : ι → U) (hzx : Set.EqOn z x (P.revealed t)) (hzy : Set.EqOn z y (P.revealed t)ᶜ) (u : ℕ) : P.transition u z = P.transition u x ∨ P.transition u z = P.transition u y

A splice in a nested coherent sweep inherits each entire transition from a parent.

def Complexity.Frontier.Sweep.prune {ι : Type u_2} {U : Type u_3} {M : Type u_4} {S : Set (ι → U)} (P : Sweep S M) (hP : P.Coherent) (hmono : Monotone P.revealed) (T : (t : ℕ) → Set (M × M × (↑(P.newly t) → U))) : Sweep (P.kept T) M

Delete any collection of transitions. Accepted inputs are exactly the surviving paths.

Equations

• P.prune hP hmono T = { length := P.length, revealed := P.revealed, revealed_zero := ⋯, revealed_length := ⋯, message := P.message, message_length := ⋯, splice := ⋯ }

theorem Complexity.Frontier.Sweep.Coherent.prune {ι : Type u_2} {U : Type u_3} {M : Type u_4} {S : Set (ι → U)} (P : Sweep S M) (hP : P.Coherent) (hmono : Monotone P.revealed) (T : (t : ℕ) → Set (M × M × (↑(P.newly t) → U))) : (P.prune hP hmono T).Coherent

theorem Complexity.Frontier.Sweep.transitionCount_prune_le {ι : Type u_2} {U : Type u_3} {M : Type u_4} {S : Set (ι → U)} (P : Sweep S M) (hP : P.Coherent) (hmono : Monotone P.revealed) (T : (t : ℕ) → Set (M × M × (↑(P.newly t) → U))) (hT : ∀ t < P.length, (T t).Finite) : (P.prune hP hmono T).transitionCount ≤ ∑ t ∈ Finset.range P.length, (T t).ncard

theorem Complexity.Frontier.Sweep.sumOn_discarded_le {ι : Type u_2} {U : Type u_3} {M : Type u_4} {S : Set (ι → U)} (P : Sweep S M) [Finite ι] [Finite U] (T : (t : ℕ) → Set (M × M × (↑(P.newly t) → U))) {w : (ι → U) → ℝ} (hw : ∀ (x : ι → U), 0 ≤ w x) : sumOn w (S \ P.kept T) ≤ ∑ t ∈ Finset.range P.length, sumOn w {x : ι → U | x ∈ S ∧ P.transition t x ∉ T t}

Lost probability or weight is at most the sum of the individual transition tails.

theorem Complexity.Frontier.Sweep.abs_sumOn_le_pruned {ι : Type u_2} {U : Type u_3} {M : Type u_4} {S : Set (ι → U)} (P : Sweep S M) [Finite ι] [Finite U] (hP : P.Coherent) (hmono : Monotone P.revealed) (hL : 0 < P.length) (T : (t : ℕ) → Set (M × M × (↑(P.newly t) → U))) (hT : ∀ t < P.length, (T t).Finite) {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) * ∑ t ∈ Finset.range P.length, (T t).ncard) + sumOn (fun (x : ι → U) => |w x|) (S \ P.kept T)

Approximate pruning bound. Retained transitions pay the frontier cost; discarded inputs pay their actual absolute weight. No independence assumption is required.

theorem Complexity.Frontier.Network.sweep_revealed_mono {ι : Type u_2} {U : Type u_3} {V : Type u_5} {E : Type u_6} (N : Network U ι V E) (π : Layout V) [Nonempty U] : Monotone (N.sweep π).revealed

Network sweeps reveal inputs monotonically, including the final unused-input step.

theorem Complexity.Frontier.agreement_le_of_output_errors {α : Type u_1} [Finite α] [Nonempty α] (f g : α → Bool) {β : ℝ} (R : Bool → ℝ) (h : ∀ (b : Bool), |sumOn (fun (x : α) => boolSign (f x)) {x : α | g x = b}| ≤ β * ↑{x : α | g x = b}.ncard + R b) : agreement f g ≤ (1 + β) / 2 + (R true + R false) / (2 * ↑(Nat.card α))

Unequal error budgets on the two prediction classes are added before normalization.

theorem Complexity.Frontier.agreement_le_pruned_sweeps {ι : Type u_2} {U : Type u_3} [Finite ι] [Finite U] [Nonempty U] {f g : (ι → U) → Bool} {K : ℕ} {β : ℝ} (hf : RectangleBias f K β) (hK : 1 < K) (hβ : 0 ≤ β) {Msg : Bool → Type u_5} (P : (b : Bool) → Sweep {x : ι → U | g x = b} (Msg b)) (hP : ∀ (b : Bool), (P b).Coherent) (hmono : ∀ (b : Bool), Monotone (P b).revealed) (hL : ∀ (b : Bool), 0 < (P b).length) (T : (b : Bool) → (t : ℕ) → Set (Msg b × Msg b × (↑((P b).newly t) → U))) (hT : ∀ (b : Bool), ∀ t < (P b).length, (T b t).Finite) : have D := fun (b : Bool) => ∑ t ∈ Finset.range (P b).length, (T b t).ncard; have lost := fun (b : Bool) => ({x : ι → U | g x = b} \ (P b).kept (T b)).ncard; agreement f g ≤ (1 + β) / 2 + ↑((K - 1) ^ 2 * (D true + D false) + lost true + lost false) / (2 * ↑(Nat.card (ι → U)))

Pruned prediction bound. D b counts the retained transitions for output b, and lost b counts the discarded inputs. Their contribution to agreement has the factor 1/(2 |domain|), so discarding probability mass δ costs at most δ/2.