+# Finite probability weights for message bounds

A normalized weight on messages certifies an upper bound on their average coding cost. Conditional weights may depend on earlier coordinates, without requiring independence. The logarithmic counting argument is the finite communication method of Roychowdhury--Orlitsky--Siu, with explicit probability weights.

structure Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] (key : X → Y) (cost : ℝ) : Type u_2

A normalized message weight with a bound on its average natural-log cost.

• weight : Y → ℝ

  Probability weight assigned to each possible message.

• nonneg (y : Y) : 0 ≤ self.weight y
• mass : ∑ y : Y, self.weight y = 1
• positive (x : X) : 0 < self.weight (key x)
• log_bound : -↑(Fintype.card X) * cost ≤ ∑ x : X, Real.log (self.weight (key x))

structure Algebraic.Cutwidth.Aggregate.Geometry.Entropy.ConditionalWeightBound {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] (key : X → Y) (parent : X → Z) (cost : ℝ) : Type (max u_2 u_3)

A conditional probability weight, normalized at every possible parent value.

• weight : Z → Y → ℝ

  Probability weight on new messages, indexed by the earlier observation.

• nonneg (z : Z) (y : Y) : 0 ≤ self.weight z y
• mass (z : Z) : ∑ y : Y, self.weight z y = 1
• positive (x : X) : 0 < self.weight (parent x) (key x)
• log_bound : -↑(Fintype.card X) * cost ≤ ∑ x : X, Real.log (self.weight (parent x) (key x))

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.log_card_le {X : Type u_1} {Y : Type u_2} [Fintype X] [Nonempty X] [Fintype Y] {key : X → Y} {cost : ℝ} (bound : WeightBound key cost) {K : ℕ} (hK : 0 < K) (fibres : ∀ (y : Y), {x : X | key x = y}.card ≤ K) : Real.log ↑(Fintype.card X) ≤ Real.log ↑K + cost

A weight certificate and a bound on every fibre bound the number of inputs.

def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.mono {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {key : X → Y} {a b : ℝ} (bound : WeightBound key a) (hab : a ≤ b) : WeightBound key b

Increasing the certified cost preserves a weight certificate.

Equations

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

def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.ofPointwiseWeightLE {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {key : X → Y} {cost : ℝ} (bound : WeightBound key cost) (next : X → Y) (increase : ∀ (x : X), bound.weight (key x) ≤ bound.weight (next x)) : WeightBound next cost

Reuse a weight when changing the message only increases its pointwise weight.

Equations

• bound.ofPointwiseWeightLE next increase = { weight := bound.weight, nonneg := ⋯, mass := ⋯, positive := ⋯, log_bound := ⋯ }

def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.ConditionalWeightBound.mono {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] {key : X → Y} {parent : X → Z} {a b : ℝ} (bound : ConditionalWeightBound key parent a) (hab : a ≤ b) : ConditionalWeightBound key parent b

Increasing a conditional cost preserves its certificate.

Equations

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