Separate information costs for two-variable and wider conjunctions #
The support-graph bound pays for a family of two-variable conjunctions jointly. Conjunctions with at least three variables retain the sharper one-eighth entropy cost instead of being weakened to the graph's edge cost.
noncomputable def
Algebraic.Cutwidth.Aggregate.Geometry.Joint.evalLiteralsFamiliesRefinedWeightBound
{V : Type u_1}
{I : Type u_2}
{J : Type u_3}
[Fintype V]
[DecidableEq V]
[Fintype I]
[DecidableEq I]
[Fintype J]
[DecidableEq J]
(L₂ : I → Finset (V × Bool))
(L₃ : J → Finset (V × Bool))
(two : ∀ (i : I), 2 ≤ (literalVars (L₂ i)).card)
(three : ∀ (j : J), 3 ≤ (literalVars (L₃ j)).card)
:
Entropy.WeightBound (fun (x : V → Bool) => (fun (i : I) => evalLiterals (L₂ i) x, fun (j : J) => evalLiterals (L₃ j) x))
(↑(Fintype.card I) * Entropy.Graph.edgeCost + ↑(Fintype.card V) * Entropy.Graph.vertexCost + ↑(Fintype.card J) * Real.binEntropy (1 / 8))
Two selected conjunction families retain their separate joint and marginal costs.
Equations
- One or more equations did not get rendered due to their size.