Conditional weights from finite tables

For a uniform finite source, empirical conditional probabilities give a normalized kernel. Unobserved parent values use the uniform bit distribution. This keeps normalization valid on every possible message, including impossible prefixes.

def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.tableCount {X : Type u_1} {Y : Type u_2} [Fintype X] [DecidableEq Y] (key : X → Y) (y : Y) : ℕ

Number of source points producing an outcome.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Entropy.tableCount key y = {x : X | key x = y}.card

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.tableWeight {X : Type u_1} {Z : Type u_2} [Fintype X] [DecidableEq Z] (key : X → Bool) (parent : X → Z) (z : Z) (b : Bool) : ℝ

Empirical conditional bit weights, with a normalized fallback at empty parents.

Equations

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

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.tableCount_pos {X : Type u_1} {Y : Type u_2} [Fintype X] [DecidableEq Y] (key : X → Y) (x : X) : 0 < tableCount key (key x)

Every observed outcome occurs at least once.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.tableWeight_nonneg {X : Type u_1} {Z : Type u_2} [Fintype X] [DecidableEq Z] (key : X → Bool) (parent : X → Z) (z : Z) (b : Bool) : 0 ≤ tableWeight key parent z b

Every conditional weight is nonnegative.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.sum_tableWeight {X : Type u_1} {Z : Type u_2} [Fintype X] [DecidableEq Z] (key : X → Bool) (parent : X → Z) (z : Z) : ∑ b : Bool, tableWeight key parent z b = 1

The empirical bit kernel is normalized, including at impossible parent values.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.tableWeight_pos {X : Type u_1} {Z : Type u_2} [Fintype X] [DecidableEq Z] (key : X → Bool) (parent : X → Z) (x : X) : 0 < tableWeight key parent (parent x) (key x)

Empirical weights are positive on all actual source points.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.tableCost {X : Type u_1} {Z : Type u_2} [Fintype X] [DecidableEq Z] (key : X → Bool) (parent : X → Z) : ℝ

Average natural-log cost of the empirical conditional kernel.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.tableConditionalBound {X : Type u_1} {Z : Type u_2} [Fintype X] [Nonempty X] [DecidableEq Z] (key : X → Bool) (parent : X → Z) : ConditionalWeightBound key parent (tableCost key parent)

A finite conditional table supplies its own exact weight certificate.

Equations

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