Entropy certificates after selecting a large majority fiber

The remaining conjunctions are still biased under the uniform distribution on the majority event. Two distinct literals cost at most H(4/9) and three cost at most H(8/27), in natural logarithmic units.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.evalLiteralsPairWeightBound {E : Type u_1} {V : Type u_2} [Fintype E] [Fintype V] [DecidableEq V] (edge : E → Entropy.SignedEdge V) (disjoint : Function.Injective (endpoint edge)) {L : Finset (V × Bool)} (two : 2 ≤ (Joint.literalVars L).card) : Entropy.WeightBound (fun (x : ↥(majorityInputs edge)) => Joint.evalLiterals L ↑x) (Real.binEntropy (4 / 9))

Two distinct literals retain a strict entropy saving on a majority fiber.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.evalLiteralsTripleWeightBound {E : Type u_1} {V : Type u_2} [Fintype E] [Fintype V] [DecidableEq V] (edge : E → Entropy.SignedEdge V) (disjoint : Function.Injective (endpoint edge)) {L : Finset (V × Bool)} (three : 3 ≤ (Joint.literalVars L).card) : Entropy.WeightBound (fun (x : ↥(majorityInputs edge)) => Joint.evalLiterals L ↑x) (Real.binEntropy (8 / 27))

Three distinct literals retain a stronger entropy saving on a majority fiber.

Equations

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

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.log_card_le_of_weight {E : Type u_1} {V : Type u_2} {Y : Type u_3} [Fintype E] [Fintype V] [Fintype Y] (edge : E → Entropy.SignedEdge V) (disjoint : Function.Injective (endpoint edge)) (key : ↥(majorityInputs edge) → Y) {K : ℕ} (hK : 0 < K) (fibers : ∀ (y : Y), {x : ↥(majorityInputs edge) | key x = y}.card ≤ K) {cost : ℝ} (bound : Entropy.WeightBound key cost) : ↑(Fintype.card V) + (Real.logb 2 3 - 2) * ↑(Fintype.card E) ≤ cost / Real.log 2 + Real.logb 2 ↑K

A weight certificate measures the actual coding cost on the majority event.