Documentation

Complexitylib.BooleanAnalysis.PolynomialCorrelation.Internal.Counting

Counting retained and exceptional generators #

Toggling the chosen majority flag pairs the retained and omitted generators. The unpaired generators have every block in the top d low-degree levels.

source
@[reducible, inline]
abbrev Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.ExceptionalAtom (m d : ℕ) :
Type

A block whose low monomial lies within d levels of the middle.

Equations
Instances For
    source
    noncomputable def Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.toggle {k m : ℕ} (d : ℕ) (a : Term k m) :
    Term k m

    Toggle the selected majority flag, fixing generators without a pivot.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.pivot_toggle {k m d : ℕ} (a : Term k m) :
      pivot d (toggle d a) = pivot d a
      source
      theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.toggle_involutive {k m d : ℕ} :
      Function.Involutive (toggle d)
      source
      theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.allowed_of_pivot_none {k m d : ℕ} {a : Term k m} (h : pivot d a = none) :
      Allowed d a
      source
      theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.allowed_iff_of_pivot {k m d : ℕ} {a : Term k m} {i : Fin k} (h : pivot d a = some i) :
      Allowed d a ↔ (a i).2 = false
      source
      theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.pivot_none_iff {k m d : ℕ} (a : Term k m) :
      pivot d a = none ↔ ∀ (i : Fin k), m < (↑(a i).1).card + d
      source
      noncomputable def Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.exceptionalEquiv {k m d : ℕ} :
      { a : Term k m // pivot d a = none } ≃ (Fin k → ExceptionalAtom m d)

      A generator has no pivot exactly when each of its block indices is exceptional.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.card_allowed {k m d : ℕ} :
        2 * Nat.card { a : Term k m // Allowed d a } = Nat.card (Term k m) + Nat.card (ExceptionalAtom m d) ^ k
        source
        theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.compl_low {m : ℕ} {x : Finset (Fin (2 * m + 1))} (hx : m < x.card) :
        xᶜ.card ≤ m
        source
        theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.low_compl_high {m : ℕ} (a : Low (Fin (2 * m + 1)) m) :
        m < (↑a)ᶜ.card
        source
        def Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.atomCubeEquiv {m : ℕ} :
        Atom m ≃ Finset (Fin (2 * m + 1))

        Pairing a lower-half subset with its complement enumerates the whole block.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.card_atom {m : ℕ} :
          Nat.card (Atom m) = 2 ^ (2 * m + 1)
          source
          theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.card_term {k m : ℕ} :
          Nat.card (Term k m) = Nat.card (BlockCube k m)
          source
          theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.twice_agreement_card_le {k m d : ℕ} (p : MvPolynomial (Fin k × Fin (2 * m + 1)) (ZMod 2)) (hp : p.totalDegree ≤ d) (E : Set (BlockCube k m)) (hE : ∀ x ∈ E, polynomialEval p x = xorMajority x) :
          2 * Nat.card ↑E ≤ Nat.card (BlockCube k m) + Nat.card (ExceptionalAtom m d) ^ k

          The finite counting inequality underlying the exponential correlation bound.