Frontiers on a tree of regions

A binary decomposition pays for the joint boundary states at each merge, rather than for the largest individual separator. Threshold charging now uses the two child interiors and the parent exterior. This costs (K - 1)^3 per merge, still subexponential when K is. The weighted version uses the same disjoint peeling idea as the linear sweep.

structure Complexity.Frontier.RegionTree (ι : Type u_5) (N : Type u_6) : Type (max u_5 u_6)

A finite binary region decomposition. Empty children serve as leaves; every nonempty child has smaller rank. Inputs not in either child are read at the current node.

• region : N → Set ι

  The inputs of each node's region.

• root : N

  The root node, whose region is everything.

• region_root : self.region self.root = Set.univ
• left : N → N

  The left child of a node.

• right : N → N

  The right child of a node.

• rank : N → ℕ

  A rank that decreases at every nonempty child.

• left_subset (v : N) : self.region (self.left v) ⊆ self.region v
• right_subset (v : N) : self.region (self.right v) ⊆ self.region v
• disjoint (v : N) : Disjoint (self.region (self.left v)) (self.region (self.right v))
• left_lt (v : N) : self.region (self.left v) = ∅ ∨ self.rank (self.left v) < self.rank v
• right_lt (v : N) : self.region (self.right v) = ∅ ∨ self.rank (self.right v) < self.rank v

structure Complexity.Frontier.TreeFrontier {ι : Type u_1} {U : Type u_2} (S : Set (ι → U)) (M : Type u_5) (N : Type u_6) extends Complexity.Frontier.RegionTree ι N : Type (max (max (max u_1 u_2) u_5) u_6)

Splicing messages on a binary tree of input regions.

• region : N → Set ι
• root : N
• region_root : self.region self.root = Set.univ
• left : N → N
• right : N → N
• rank : N → ℕ
• left_subset (v : N) : self.region (self.left v) ⊆ self.region v
• right_subset (v : N) : self.region (self.right v) ⊆ self.region v
• disjoint (v : N) : Disjoint (self.region (self.left v)) (self.region (self.right v))
• left_lt (v : N) : self.region (self.left v) = ∅ ∨ self.rank (self.left v) < self.rank v
• right_lt (v : N) : self.region (self.right v) = ∅ ∨ self.rank (self.right v) < self.rank v
• message : N → (ι → U) → M

  The message of each node, a function of the whole input.

• message_root (x : ι → U) : x ∈ S → ∀ y ∈ S, self.message self.root x = self.message self.root y
• splice (v : N) (x : ι → U) : x ∈ S → ∀ y ∈ S, self.message v x = self.message v y → ∀ (z : ι → U), Set.EqOn z x (self.region v) → Set.EqOn z y (self.region v)ᶜ → z ∈ S

def Complexity.Frontier.TreeFrontier.peers {ι : Type u_1} {U : Type u_2} {M : Type u_3} {N : Type u_4} {S : Set (ι → U)} (P : TreeFrontier S M N) (v : N) (x : ι → U) : Set (ι → U)

The inputs of S sending the same message at v as x.

Equations

• P.peers v x = {y : ι → U | y ∈ S ∧ P.message v y = P.message v x}

def Complexity.Frontier.TreeFrontier.inside {ι : Type u_1} {U : Type u_2} {M : Type u_3} {N : Type u_4} {S : Set (ι → U)} (P : TreeFrontier S M N) (v : N) (x : ι → U) : Set (↑(P.region v) → U)

The restrictions of the peers of x at v to the region of v.

Equations

• P.inside v x = (P.region v).domRestrict '' P.peers v x

def Complexity.Frontier.TreeFrontier.outside {ι : Type u_1} {U : Type u_2} {M : Type u_3} {N : Type u_4} {S : Set (ι → U)} (P : TreeFrontier S M N) (v : N) (x : ι → U) : Set (↑(P.region v)ᶜ → U)

The restrictions of the peers of x at v to the complement of its region.

Equations

• P.outside v x = (P.region v)ᶜ.domRestrict '' P.peers v x

def Complexity.Frontier.TreeFrontier.localInputs {ι : Type u_1} {U : Type u_2} {M : Type u_3} {N : Type u_4} {S : Set (ι → U)} (P : TreeFrontier S M N) (v : N) : Set ι

The inputs of the region of v in neither child region: those read at v.

Equations

• P.localInputs v = P.region v \ (P.region (P.left v) ∪ P.region (P.right v))

def Complexity.Frontier.TreeFrontier.transition {ι : Type u_1} {U : Type u_2} {M : Type u_3} {N : Type u_4} {S : Set (ι → U)} (P : TreeFrontier S M N) (v : N) (x : ι → U) : M × M × M × (↑(P.localInputs v) → U)

A merge includes all three messages, together with inputs read locally.

Equations

• P.transition v x = (P.message v x, P.message (P.left v) x, P.message (P.right v) x, (P.localInputs v).domRestrict x)

noncomputable def Complexity.Frontier.TreeFrontier.transitionCount {ι : Type u_1} {U : Type u_2} {M : Type u_3} {N : Type u_4} {S : Set (ι → U)} (P : TreeFrontier S M N) [Fintype N] : ℕ

The number of distinct merge transitions realized by S, summed over all nodes.

Equations

• P.transitionCount = ∑ v : N, (P.transition v '' S).ncard

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

A splice stays in the shared class and inherits each other message from a parent. Laminar network separators with unique satisfying assignments have this property.

Equations

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

theorem Complexity.Frontier.TreeFrontier.Coherent.peers_eq_rectangle {ι : Type u_1} {U : Type u_2} {M : Type u_3} {N : Type u_4} {S : Set (ι → U)} (P : TreeFrontier S M N) (hP : P.Coherent) (v : N) (x : ι → U) : P.peers v x = rectangle (P.region v) (P.inside v x) (P.outside v x)

def Complexity.Frontier.TreeFrontier.erase {ι : Type u_1} {U : Type u_2} {M : Type u_3} {N : Type u_4} {S : Set (ι → U)} (P : TreeFrontier S M N) (hP : P.Coherent) (v : N) (x : ι → U) : TreeFrontier (S \ P.peers v x) M N

Delete the peers of x at v from a coherent tree frontier.

Equations

• P.erase hP v x = { toRegionTree := P.toRegionTree, message := P.message, message_root := ⋯, splice := ⋯ }

theorem Complexity.Frontier.TreeFrontier.Coherent.erase {ι : Type u_1} {U : Type u_2} {M : Type u_3} {N : Type u_4} {S : Set (ι → U)} (P : TreeFrontier S M N) (hP : P.Coherent) (v : N) (x : ι → U) : (P.erase hP v x).Coherent

theorem Complexity.Frontier.TreeFrontier.transitionCount_erase_le {ι : Type u_1} {U : Type u_2} {M : Type u_3} {N : Type u_4} {S : Set (ι → U)} (P : TreeFrontier S M N) [Finite ι] [Finite U] [Fintype N] (hP : P.Coherent) (v : N) (x : ι → U) : (P.erase hP v x).transitionCount ≤ P.transitionCount

theorem Complexity.Frontier.TreeFrontier.ncard_inside_empty_le {ι : Type u_1} {U : Type u_2} {M : Type u_3} {N : Type u_4} {S : Set (ι → U)} (P : TreeFrontier S M N) {v : N} (hv : P.region v = ∅) (x : ι → U) : (P.inside v x).ncard ≤ 1

theorem Complexity.Frontier.TreeFrontier.ncard_inside_root {ι : Type u_1} {U : Type u_2} {M : Type u_3} {N : Type u_4} {S : Set (ι → U)} (P : TreeFrontier S M N) {x : ι → U} (hx : x ∈ S) : (P.inside P.root x).ncard = S.ncard

theorem Complexity.Frontier.TreeFrontier.exists_critical {ι : Type u_1} {U : Type u_2} {M : Type u_3} {N : Type u_4} {S : Set (ι → U)} (P : TreeFrontier S M N) {K : ℕ} (hK : 1 < K) (hS : K ≤ S.ncard) {x : ι → U} (hx : x ∈ S) : ∃ (v : N), K ≤ (P.inside v x).ncard ∧ (P.inside (P.left v) x).ncard < K ∧ (P.inside (P.right v) x).ncard < K

A minimal-rank region with a large interior has two small child interiors.

theorem Complexity.Frontier.TreeFrontier.ncard_le_of_small_sides {ι : Type u_1} {U : Type u_2} {M : Type u_3} {N : Type u_4} {S : Set (ι → U)} (P : TreeFrontier S M N) [Finite ι] [Finite U] [Fintype N] {K : ℕ} (hK : 1 < K) (hS : K ≤ S.ncard) (hsmall : ∀ (v : N), ∀ x ∈ S, (P.inside v x).ncard < K ∨ (P.outside v x).ncard < K) : S.ncard ≤ (K - 1) ^ 3 * P.transitionCount

Tree threshold charging. Only the actual number of joint merge states is charged.

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

theorem Complexity.Frontier.TreeFrontier.abs_sumOn_le_of_budget {ι : Type u_1} {U : Type u_2} {M : Type u_3} {N : Type u_4} {S : Set (ι → U)} (P : TreeFrontier S M N) [Finite ι] [Finite U] [Fintype N] (hP : P.Coherent) {K : ℕ} (hK : 1 < K) {w cost : (ι → U) → ℝ} {a : ℝ} (ha : 0 ≤ a) (hw : ∀ (x : ι → U), |w x| ≤ a) (hc : ∀ (x : ι → U), 0 ≤ cost x) (hrect : RectangleBudget w cost K K) : |sumOn w S| ≤ sumOn cost S + a * ↑((K - 1) ^ 3 * P.transitionCount)

Weighted tree peeling. A rectangle budget is paid once; the thin remainder pays at most (K - 1)^3 maximum atoms per joint merge state.