Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Joint.Conjunction.Bias

One-eighth bias for conjunctions using three or more primary variables #

Three distinct required coordinates already force an event of probability at most one eighth. Contradictory literals only decrease this probability. Its binary entropy fits the graph bound's remaining-edge charge.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.eight_mul_card_evalLiterals_le {V : Type u_1} [Fintype V] [DecidableEq V] {L : Finset (V × Bool)} (three : 3 ≤ (literalVars L).card) :
8 * {x : V → Bool | evalLiterals L x = true}.card ≤ 2 ^ Fintype.card V

Three different primary variables force at least three independent Boolean coordinates.

source
noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Joint.evalLiteralsEighthWeightBoundOfThreeLe {V : Type u_1} [Fintype V] [DecidableEq V] {L : Finset (V × Bool)} (three : 3 ≤ (literalVars L).card) :
Entropy.WeightBound (evalLiterals L) (Real.binEntropy (1 / 8))

A conjunction on at least three primary variables has at most one-eighth bit entropy.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Joint.evalLiteralsWeightBoundOfThreeLe {V : Type u_1} [Fintype V] [DecidableEq V] {L : Finset (V × Bool)} (three : 3 ≤ (literalVars L).card) :
    Entropy.WeightBound (evalLiterals L) (3 / 2 * Real.log 2 - Real.binEntropy (1 / 4))

    A conjunction on at least three primary variables fits the remaining-edge graph cost.

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