Cryptographic Boolean Functions in Lean

3.1. Distribution of algebraic degree🔗

Theorem3.1.1
Group: Chapter 3: Boolean functions and cryptography (72)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Theorem 1.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 4.4.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-4algebraic-degreepage-49fidelity-exact

High algebraic degree is typical (Carlet, p. 49). For n\ge2, the number of functions f:V_n\to\mathbb F_2 with \deg_{\mathrm{alg}}(f)\le n-2 is 2^{\sum_{i=0}^{n-2}\binom ni}=2^{2^n-n-1}. Consequently, the probability that a uniformly chosen n-variable Boolean function has degree at least n-1 tends to one as n\to\infty.

Lean code for Theorem3.1.1●7 declarations
  • theoremdefined in CryptBoolean/Carlet/Chapter04/DegreeCount.lean
    complete
    theorem CryptBoolean.sum_choose_le_n_sub_two (n : ℕ) (hn : 2 ≤ n) :
  ∑ j ∈ Finset.range (n - 2 + 1), n.choose j = 2 ^ n - n - 1
    theorem CryptBoolean.sum_choose_le_n_sub_two
  (n : ℕ) (hn : 2 ≤ n) :
  ∑ j ∈ Finset.range (n - 2 + 1),
      n.choose j =
    2 ^ n - n - 1
    The low-degree binomial sum omits exactly the last two terms of the
full binomial expansion.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/DegreeCount.lean
    complete
    theorem CryptBoolean.card_booleanFunctions_degree_le_n_sub_two (n : ℕ) :
  Nat.card { f // FABL.functionAlgebraicDegree f ≤ n - 2 } =
    2 ^ ∑ j ∈ Finset.range (n - 2 + 1), n.choose j
    theorem CryptBoolean.card_booleanFunctions_degree_le_n_sub_two
  (n : ℕ) :
  Nat.card
      { f //
        FABL.functionAlgebraicDegree f ≤
          n - 2 } =
    2 ^
      ∑ j ∈ Finset.range (n - 2 + 1),
        n.choose j
    The functions of degree at most `n - 2` are exactly the corresponding
Reed--Muller codewords, so their number has the standard dimension formula.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/DegreeCount.lean
    complete
    theorem CryptBoolean.card_booleanFunctions_degree_le_n_sub_two_eq (n : ℕ)
  (hn : 2 ≤ n) :
  Nat.card { f // FABL.functionAlgebraicDegree f ≤ n - 2 } =
    2 ^ (2 ^ n - n - 1)
    theorem CryptBoolean.card_booleanFunctions_degree_le_n_sub_two_eq
  (n : ℕ) (hn : 2 ≤ n) :
  Nat.card
      { f //
        FABL.functionAlgebraicDegree f ≤
          n - 2 } =
    2 ^ (2 ^ n - n - 1)
    Carlet's simplified exact count of functions of degree at most `n - 2`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/DegreeCount.lean
    complete
    theorem CryptBoolean.natCard_booleanFunction (n : ℕ) :
  Nat.card (CryptBoolean.BooleanFunction n) = 2 ^ 2 ^ n
    theorem CryptBoolean.natCard_booleanFunction
  (n : ℕ) :
  Nat.card
      (CryptBoolean.BooleanFunction n) =
    2 ^ 2 ^ n
    The number of all `n`-variable Boolean functions is `2^(2^n)`.
  • defdefined in CryptBoolean/Carlet/Chapter04/DegreeCount.lean
    complete
    def CryptBoolean.highAlgebraicDegreeProbability (n : ℕ) : ℝ
    def CryptBoolean.highAlgebraicDegreeProbability
  (n : ℕ) : ℝ
    The proportion of `n`-variable Boolean functions having degree at least
`n - 1`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/DegreeCount.lean
    complete
    theorem CryptBoolean.highAlgebraicDegreeProbability_eq_card_ratio (n : ℕ)
  (hn : 2 ≤ n) :
  CryptBoolean.highAlgebraicDegreeProbability n =
    ↑(Nat.card { f // n - 1 ≤ FABL.functionAlgebraicDegree f }) /
      ↑(Nat.card (CryptBoolean.BooleanFunction n))
    theorem CryptBoolean.highAlgebraicDegreeProbability_eq_card_ratio
  (n : ℕ) (hn : 2 ≤ n) :
  CryptBoolean.highAlgebraicDegreeProbability
      n =
    ↑(Nat.card
          { f //
            n - 1 ≤
              FABL.functionAlgebraicDegree
                f }) /
      ↑(Nat.card
          (CryptBoolean.BooleanFunction
            n))
    The displayed probability is the exact uniform counting ratio.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/DegreeCount.lean
    complete
    theorem CryptBoolean.tendsto_highAlgebraicDegreeProbability :
  Filter.Tendsto CryptBoolean.highAlgebraicDegreeProbability
    Filter.atTop (nhds 1)
    theorem CryptBoolean.tendsto_highAlgebraicDegreeProbability :
  Filter.Tendsto
    CryptBoolean.highAlgebraicDegreeProbability
    Filter.atTop (nhds 1)
    A uniformly chosen Boolean function has degree at least `n - 1` with
probability tending to one.