Message weights with several constant and biased classes

Frozen coordinates may have different constant values. Two disjoint biased classes and the remaining Boolean coordinates reconstruct the full message without any independence assumption on their outputs.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.keyWeightBoundOfConstantClasses {X : Type u_1} [Fintype X] {g : ℕ} (message : X → Fin g → Bool) (T W O : Finset (Fin g)) (disjoint : Disjoint T W) (outputs : Disjoint (T ∪ W) O) (value : Fin g → Bool) (constant : ∀ i ∈ O, ∀ (x : X), message x i = value i) {cost : ℝ} (classes : Entropy.WeightBound (fun (x : X) => (fun (i : ↥T) => message x ↑i, fun (i : ↥W) => message x ↑i)) cost) : Entropy.WeightBound message (cost + (↑g - ↑T.card - ↑W.card - ↑O.card) * Real.log 2)

Reconstruct a message from two weighted classes and the remaining nonconstant bits.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.keyWeightBoundWithFrozen {X : Type u_1} [Fintype X] {g : ℕ} (message : X → Fin g → Bool) (T W S O : Finset (Fin g)) (selected : S ⊆ T) (disjoint : Disjoint T W) (outputs : Disjoint (T ∪ W) O) (frozen : ∀ i ∈ S, ∀ (x : X), message x i = false) (constant : ∀ i ∈ O, ∀ (x : X), message x i = true) {ct cw : ℝ} (narrow : Entropy.WeightBound (fun (x : X) (i : ↥(T \ S)) => message x ↑i) (↑(T \ S).card * ct)) (wide : Entropy.WeightBound (fun (x : X) (i : ↥W) => message x ↑i) (↑W.card * cw)) : Entropy.WeightBound message ((↑g - ↑S.card - ↑O.card) * Real.log 2 - (↑T.card - ↑S.card) * (Real.log 2 - ct) - ↑W.card * (Real.log 2 - cw))

Frozen narrow summaries and separately constant outputs have disjoint costs.

Equations

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