+# Uniform changes of coordinates for finite weight certificates

An injective selection of Boolean coordinates is uniformly distributed. Splitting the cube into selected and unused coordinates transports local certificates to the full input cube without any independence hypotheses about other messages.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.precompEquiv {X : Type u_1} {X' : Type u_2} {Y : Type u_3} [Fintype X] [Fintype X'] [Fintype Y] {key : X → Y} {cost : ℝ} (bound : WeightBound key cost) (e : X' ≃ X) : WeightBound (key ∘ ⇑e) cost

Reindex the uniform source of a weight certificate by an equivalence.

Equations

• bound.precompEquiv e = { weight := bound.weight, nonneg := ⋯, mass := ⋯, positive := ⋯, log_bound := ⋯ }

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.precompFst {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] {key : X → Y} {cost : ℝ} (bound : WeightBound key cost) : WeightBound (fun (x : X × Z) => key x.1) cost

Add unused independent coordinates to a weight certificate.

Equations

• bound.precompFst = { weight := bound.weight, nonneg := ⋯, mass := ⋯, positive := ⋯, log_bound := ⋯ }

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.ConditionalWeightBound.precompEquiv {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Z : Type u_4} [Fintype X] [Fintype X'] [Fintype Y] {key : X → Y} {parent : X → Z} {cost : ℝ} (bound : ConditionalWeightBound key parent cost) (e : X' ≃ X) : ConditionalWeightBound (key ∘ ⇑e) (parent ∘ ⇑e) cost

Reindex the uniform source of a conditional certificate.

Equations

• bound.precompEquiv e = { weight := bound.weight, nonneg := ⋯, mass := ⋯, positive := ⋯, log_bound := ⋯ }

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.ConditionalWeightBound.precompFst {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {W : Type u_4} [Fintype X] [Fintype Y] [Fintype W] {key : X → Y} {parent : X → Z} {cost : ℝ} (bound : ConditionalWeightBound key parent cost) : ConditionalWeightBound (fun (x : X × W) => key x.1) (fun (x : X × W) => parent x.1) cost

Add unused independent coordinates to a conditional certificate.

Equations

• bound.precompFst = { weight := bound.weight, nonneg := ⋯, mass := ⋯, positive := ⋯, log_bound := ⋯ }

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.coordinateSplit {I : Type u_1} {V : Type u_2} (e : I ↪ V) : (V → Bool) ≃ (I → Bool) × ({ v : V // v ∉ Set.range ⇑e } → Bool)

Split a Boolean cube into injectively selected coordinates and their complement.

Equations

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

@[simp]

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.coordinateSplit_fst {I : Type u_1} {V : Type u_2} (e : I ↪ V) (x : V → Bool) : ((coordinateSplit e) x).1 = x ∘ ⇑e

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.precompCoordinates {I : Type u_1} {V : Type u_2} {Y : Type u_3} [Fintype I] [Fintype V] [Fintype Y] [DecidableEq I] [DecidableEq V] {key : (I → Bool) → Y} {cost : ℝ} (bound : WeightBound key cost) (e : I ↪ V) : WeightBound (fun (x : V → Bool) => key (x ∘ ⇑e)) cost

Lift a local weight certificate along an injective choice of Boolean coordinates.

Equations

• bound.precompCoordinates e = bound.precompFst.precompEquiv (Algebraic.Cutwidth.Aggregate.Geometry.Entropy.coordinateSplit e)

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.ConditionalWeightBound.precompCoordinates {I : Type u_1} {V : Type u_2} {Y : Type u_3} {Z : Type u_4} [Fintype I] [Fintype V] [Fintype Y] [DecidableEq I] [DecidableEq V] {key : (I → Bool) → Y} {parent : (I → Bool) → Z} {cost : ℝ} (bound : ConditionalWeightBound key parent cost) (e : I ↪ V) : ConditionalWeightBound (fun (x : V → Bool) => key (x ∘ ⇑e)) (fun (x : V → Bool) => parent (x ∘ ⇑e)) cost

Lift a local conditional certificate along an injective choice of coordinates.

Equations

• bound.precompCoordinates e = bound.precompFst.precompEquiv (Algebraic.Cutwidth.Aggregate.Geometry.Entropy.coordinateSplit e)