Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Fiber.Conditional.Message

Actual primary messages conditioned on a majority event #

The selected exact-two messages are constant. Every other retained conjunction still has bounded bias under the product of three-state pair distributions. Constant designated-output summaries may be omitted at the same time.

source
noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.majorityKeyWeightBound {n g : ℕ} (p : Program Aggregate.Geometry.signature n g) (U : Finset (Fin n)) (S : Finset (Fin g)) (selected : S ⊆ Joint.retainedTwo p U) (edge : ↥S → Entropy.SignedEdge ↥U) (injective : Function.Injective (endpoint edge)) (forced : ∀ (x : ↥U → Bool) (i : ↥S), Aggregate.Geometry.key p U (glue U x fun (x : ↥Uᶜ) => false) ↑i = true → (edge i).eval x = true) (O : Finset (Fin g)) (outside : Disjoint (Joint.retainedTwo p U ∪ Joint.retainedWide p U) O) (constant : ∀ i ∈ O, ∀ (x : ↥U → Bool), Aggregate.Geometry.key p U (glue U x fun (x : ↥Uᶜ) => false) i = true) :
Entropy.WeightBound (fun (x : ↥(majorityInputs edge)) => Aggregate.Geometry.key p U (glue U ↑x fun (x : ↥Uᶜ) => false)) ((↑g - ↑S.card - ↑O.card) * Real.log 2 - (↑(Joint.retainedTwo p U).card - ↑S.card) * (Real.log 2 - Real.binEntropy (4 / 9)) - ↑(Joint.retainedWide p U).card * (Real.log 2 - Real.binEntropy (8 / 27)))

Conditional primary messages retain two- and three-coordinate entropy savings.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.majorityOutputKeyWeightBound {n g : ℕ} (p : Program Aggregate.Geometry.signature n g) (U : Finset (Fin n)) (S : Finset (Fin g)) (selected : S ⊆ Joint.retainedTwo p U) (edge : ↥S → Entropy.SignedEdge ↥U) (injective : Function.Injective (endpoint edge)) (forced : ∀ (x : ↥U → Bool) (i : ↥S), Aggregate.Geometry.key p U (glue U x fun (x : ↥Uᶜ) => false) ↑i = true → (edge i).eval x = true) (out : Wire n g) :
    Entropy.WeightBound (fun (x : ↥(majorityInputs edge)) => Aggregate.Geometry.outputKey p U out (glue U ↑x fun (x : ↥Uᶜ) => false)) ((↑g + 1 - ↑S.card) * Real.log 2 - (↑(Joint.retainedTwo p U).card - ↑S.card) * (Real.log 2 - Real.binEntropy (4 / 9)) - ↑(Joint.retainedWide p U).card * (Real.log 2 - Real.binEntropy (8 / 27)))

    Adding a designated-output bit does not change the conditional gate savings.

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