Combining conditional message weights

A normalized conditional kernel extends a weight on an earlier tuple. The kernels may depend on earlier coordinates, and positivity is needed only on realized inputs.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.equiv {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) (e : Y ≃ Z) : WeightBound (fun (x : X) => e (key x)) cost

Relabelling a finite message space preserves a weight certificate.

Equations

• bound.equiv e = { weight := fun (z : Z) => bound.weight (e.symm z), nonneg := ⋯, mass := ⋯, positive := ⋯, log_bound := ⋯ }

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.subsingleton {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] [Unique Y] (key : X → Y) : WeightBound key 0

A message on a subsingleton output space has zero cost.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.subsingleton key = { weight := fun (x : Y) => 1, nonneg := ⋯, mass := ⋯, positive := ⋯, log_bound := ⋯ }

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.toConditional {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] {key : X → Y} {cost : ℝ} (bound : WeightBound key cost) (parent : X → Z) : ConditionalWeightBound key parent cost

A parent-independent probability weight is a conditional kernel.

Equations

• bound.toConditional parent = { weight := fun (x : Z) => bound.weight, nonneg := ⋯, mass := ⋯, positive := ⋯, log_bound := ⋯ }

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.ConditionalWeightBound.pullParent {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {W : Type u_4} [Fintype X] [Fintype Y] {key : X → Y} {parent : X → Z} {cost : ℝ} (readout : W → Z) (whole : X → W) (agree : ∀ (x : X), readout (whole x) = parent x) (bound : ConditionalWeightBound key parent cost) : ConditionalWeightBound key whole cost

A kernel depending on selected coordinates can be read from a larger parent key.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.pairConditional {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] {parent : X → Z} {key : X → Y} {a b : ℝ} (previous : WeightBound parent a) (next : ConditionalWeightBound key parent b) : WeightBound (fun (x : X) => (key x, parent x)) (a + b)

Multiplying an earlier weight by a normalized conditional kernel adds their costs.

Equations

• previous.pairConditional next = { weight := fun (yz : Y × Z) => previous.weight yz.2 * next.weight yz.2 yz.1, nonneg := ⋯, mass := ⋯, positive := ⋯, log_bound := ⋯ }

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.map {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) (readout : Y → Z) : WeightBound (fun (x : X) => readout (key x)) cost

A deterministic readout cannot increase the certified message cost.

Equations

• bound.map readout = { weight := fun (z : Z) => ∑ y : Y with readout y = z, bound.weight y, nonneg := ⋯, mass := ⋯, positive := ⋯, log_bound := ⋯ }

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.const {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] (value : Y) : WeightBound (fun (x : X) => value) 0

A constant message has a zero-cost point-mass certificate.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.const value = (Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.subsingleton fun (x : X) => ()).map fun (x : Unit) => value

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.boolean {X : Type u_1} [Fintype X] (key : X → Bool) : WeightBound key (Real.log 2)

An arbitrary Boolean message has the uniform one-bit certificate.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.prod {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] {left : X → Y} {right : X → Z} {a b : ℝ} (first : WeightBound left a) (second : WeightBound right b) : WeightBound (fun (x : X) => (left x, right x)) (a + b)

Product weights add costs even when the two actual messages are dependent.

Equations

• first.prod second = (second.pairConditional (first.toConditional right)).mono ⋯

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.pi {X : Type u_1} [Fintype X] {ι : Type u_5} [Fintype ι] [DecidableEq ι] {T : ι → Type u_6} [(i : ι) → Fintype (T i)] {key : (i : ι) → X → T i} {cost : ι → ℝ} (bound : (i : ι) → WeightBound (key i) (cost i)) : WeightBound (fun (x : X) (i : ι) => key i x) (∑ i : ι, cost i)

Coordinatewise probability weights add their costs without an independence premise.

Equations

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