Cryptographic Boolean Functions in Lean

9.2. Fourier and Walsh transforms🔗

Theorem9.2.1
Group: Chapter 9: Symmetric and rotation-symmetric functions (22)
Group member previews
Preview
Definition 9.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 1.7.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-10symmetric-functionsfourier-transformwalsh-transformkrawtchouk-polynomialsreferences-95-255page-143fidelity-explicit-raw-normalization

Krawtchouk formulas for symmetric functions (Carlet, p. 143). For 0\le r\le n, let \varphi_r be the indicator of the weight-r layer of V_n. If a\in V_n has Hamming weight \ell, then its raw pseudo-Boolean Fourier coefficient is \widehat{\varphi_r}(a)=K_{n,r}(\ell) =\sum_{j=0}^{n}(-1)^j\binom\ell j\binom{n-\ell}{r-j}. The Krawtchouk values are characterized by \sum_{r=0}^{n}K_{n,r}(\ell)z^r =(1-z)^\ell(1+z)^{n-\ell}. Consequently, if f is symmetric with weight profile f^\#, then every raw Fourier and Walsh coefficient depends only on \ell=w_H(a), and \widehat f(a)=\sum_{r=0}^{n}f^\#(r)K_{n,r}(\ell), \qquad W_f(a)=\sum_{r=0}^{n}(-1)^{f^\#(r)}K_{n,r}(\ell). Binomial coefficients outside their natural range are zero.

Lean code for Theorem9.2.1●14 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Krawtchouk.lean
    complete
    theorem CryptBoolean.sum_weightLayer_vectorWalshCharacter_eq_krawtchoukValue
  {n : ℕ} (j : ℕ) (a : FABL.F₂Cube n) :
  ∑ x with (FABL.f₂Support x).card = j,
      (FABL.vectorWalshCharacter a) x =
    FABL.krawtchoukValue j ((FABL.binaryCubeSignEquiv n) a)
    theorem CryptBoolean.sum_weightLayer_vectorWalshCharacter_eq_krawtchoukValue
  {n : ℕ} (j : ℕ) (a : FABL.F₂Cube n) :
  ∑ x with (FABL.f₂Support x).card = j,
      (FABL.vectorWalshCharacter a) x =
    FABL.krawtchoukValue j
      ((FABL.binaryCubeSignEquiv n) a)
    Summing a binary Walsh character over a Hamming-weight layer gives the
corresponding Krawtchouk value.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Krawtchouk.lean
    complete
    theorem CryptBoolean.rawFourierTransform_booleanRealEmbedding_weightLayerIndicator_eq_krawtchoukValue
  {n : ℕ} (r : Fin (n + 1)) (a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (FABL.booleanRealEmbedding (CryptBoolean.weightLayerIndicator r))
      a =
    FABL.krawtchoukValue (↑r) ((FABL.binaryCubeSignEquiv n) a)
    theorem CryptBoolean.rawFourierTransform_booleanRealEmbedding_weightLayerIndicator_eq_krawtchoukValue
  {n : ℕ} (r : Fin (n + 1))
  (a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (FABL.booleanRealEmbedding
        (CryptBoolean.weightLayerIndicator
          r))
      a =
    FABL.krawtchoukValue (↑r)
      ((FABL.binaryCubeSignEquiv n) a)
    The raw Fourier transform of a Hamming-weight layer is its Krawtchouk
value at the frequency weight.
  • theoremdefined in FABL/Chapter05/KrawtchoukPolynomials.lean
    complete
    theorem FABL.coeff_krawtchoukGeneratingPolynomial {n : ℕ} (j : ℕ)
  (x : FABL.SignCube n) :
  (FABL.krawtchoukGeneratingPolynomial x).coeff j =
    FABL.krawtchoukValue j x
    theorem FABL.coeff_krawtchoukGeneratingPolynomial
  {n : ℕ} (j : ℕ) (x : FABL.SignCube n) :
  (FABL.krawtchoukGeneratingPolynomial
          x).coeff
      j =
    FABL.krawtchoukValue j x
    The coefficient definition of the Krawtchouk layer sum.
  • theoremdefined in FABL/Chapter05/KrawtchoukPolynomials.lean
    complete
    theorem FABL.krawtchoukGeneratingPolynomial_eq_negativeCount {n : ℕ}
  (x : FABL.SignCube n) :
  FABL.krawtchoukGeneratingPolynomial x =
    (1 - Polynomial.X) ^ FABL.negativeCoordinateCount x *
      (1 + Polynomial.X) ^ (n - FABL.negativeCoordinateCount x)
    theorem FABL.krawtchoukGeneratingPolynomial_eq_negativeCount
  {n : ℕ} (x : FABL.SignCube n) :
  FABL.krawtchoukGeneratingPolynomial x =
    (1 - Polynomial.X) ^
        FABL.negativeCoordinateCount x *
      (1 + Polynomial.X) ^
        (n -
          FABL.negativeCoordinateCount x)
    Grouping the generating product by the negative and positive coordinates.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Krawtchouk.lean
    complete
    theorem CryptBoolean.krawtchoukValue_binaryCubeSignEquiv_eq_signedChooseSum
  {n : ℕ} (j : ℕ) (a : FABL.F₂Cube n) :
  FABL.krawtchoukValue j ((FABL.binaryCubeSignEquiv n) a) =
    ∑ k ∈ Finset.range (j + 1),
      (-1) ^ k * ↑((FABL.f₂Support a).card.choose k) *
        ↑((n - (FABL.f₂Support a).card).choose (j - k))
    theorem CryptBoolean.krawtchoukValue_binaryCubeSignEquiv_eq_signedChooseSum
  {n : ℕ} (j : ℕ) (a : FABL.F₂Cube n) :
  FABL.krawtchoukValue j
      ((FABL.binaryCubeSignEquiv n) a) =
    ∑ k ∈ Finset.range (j + 1),
      (-1) ^ k *
          ↑((FABL.f₂Support a).card.choose
              k) *
        ↑((n -
                (FABL.f₂Support
                    a).card).choose
            (j - k))
    The Krawtchouk value on a binary frequency is the signed binomial sum in
the frequency Hamming weight.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Krawtchouk.lean
    complete
    theorem CryptBoolean.rawFourierTransform_booleanRealEmbedding_weightLayerIndicator_eq_signedChooseSum
  {n : ℕ} (r : Fin (n + 1)) (a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (FABL.booleanRealEmbedding (CryptBoolean.weightLayerIndicator r))
      a =
    ∑ k ∈ Finset.range (↑r + 1),
      (-1) ^ k * ↑((FABL.f₂Support a).card.choose k) *
        ↑((n - (FABL.f₂Support a).card).choose (↑r - k))
    theorem CryptBoolean.rawFourierTransform_booleanRealEmbedding_weightLayerIndicator_eq_signedChooseSum
  {n : ℕ} (r : Fin (n + 1))
  (a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (FABL.booleanRealEmbedding
        (CryptBoolean.weightLayerIndicator
          r))
      a =
    ∑ k ∈ Finset.range (↑r + 1),
      (-1) ^ k *
          ↑((FABL.f₂Support a).card.choose
              k) *
        ↑((n -
                (FABL.f₂Support
                    a).card).choose
            (↑r - k))
    The raw Fourier transform of a Hamming-weight layer is the explicit
signed binomial sum.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Krawtchouk.lean
    complete
    theorem CryptBoolean.rawFourierTransform_booleanRealEmbedding_weightLayerIndicator_eq_coeff
  {n : ℕ} (r : Fin (n + 1)) (a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (FABL.booleanRealEmbedding (CryptBoolean.weightLayerIndicator r))
      a =
    ((1 - Polynomial.X) ^ (FABL.f₂Support a).card *
          (1 + Polynomial.X) ^ (n - (FABL.f₂Support a).card)).coeff
      ↑r
    theorem CryptBoolean.rawFourierTransform_booleanRealEmbedding_weightLayerIndicator_eq_coeff
  {n : ℕ} (r : Fin (n + 1))
  (a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (FABL.booleanRealEmbedding
        (CryptBoolean.weightLayerIndicator
          r))
      a =
    ((1 - Polynomial.X) ^
            (FABL.f₂Support a).card *
          (1 + Polynomial.X) ^
            (n -
              (FABL.f₂Support
                  a).card)).coeff
      ↑r
    The raw Fourier transform of a Hamming-weight layer is the indicated
coefficient of its Krawtchouk generating polynomial.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Krawtchouk.lean
    complete
    theorem CryptBoolean.rawFourierTransform_booleanRealEmbedding_weightLayerIndicator_eq_eval
  {n : ℕ} (r : Fin (n + 1)) (a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (FABL.booleanRealEmbedding (CryptBoolean.weightLayerIndicator r))
      a =
    Polynomial.eval (↑(FABL.f₂Support a).card)
      (FABL.krawtchoukPolynomial n ↑r)
    theorem CryptBoolean.rawFourierTransform_booleanRealEmbedding_weightLayerIndicator_eq_eval
  {n : ℕ} (r : Fin (n + 1))
  (a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (FABL.booleanRealEmbedding
        (CryptBoolean.weightLayerIndicator
          r))
      a =
    Polynomial.eval
      (↑(FABL.f₂Support a).card)
      (FABL.krawtchoukPolynomial n ↑r)
    The layer transform is the evaluation of FABL's representing Krawtchouk
polynomial at the frequency Hamming weight.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Krawtchouk.lean
    complete
    theorem CryptBoolean.walshTransform_weightLayerIndicator_cast_eq_krawtchoukValue
  {n : ℕ} (r : Fin (n + 1)) (a : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform (CryptBoolean.weightLayerIndicator r)
        a) =
    (if a = 0 then 2 ^ n else 0) -
      2 * FABL.krawtchoukValue (↑r) ((FABL.binaryCubeSignEquiv n) a)
    theorem CryptBoolean.walshTransform_weightLayerIndicator_cast_eq_krawtchoukValue
  {n : ℕ} (r : Fin (n + 1))
  (a : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform
        (CryptBoolean.weightLayerIndicator
          r)
        a) =
    (if a = 0 then 2 ^ n else 0) -
      2 *
        FABL.krawtchoukValue (↑r)
          ((FABL.binaryCubeSignEquiv n) a)
    The Walsh transform of a Hamming-weight layer is the constant spectrum
minus twice its Krawtchouk layer spectrum.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Krawtchouk.lean
    complete
    theorem CryptBoolean.IsSymmetricBooleanFunction.booleanRealEmbedding_eq_sum_weightLayerIndicator
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) :
  FABL.booleanRealEmbedding f =
    ∑ r, fun x =>
      CryptBoolean.symmetricRealWeightProfile f ↑r *
        FABL.booleanRealEmbedding (CryptBoolean.weightLayerIndicator r)
          x
    theorem CryptBoolean.IsSymmetricBooleanFunction.booleanRealEmbedding_eq_sum_weightLayerIndicator
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  FABL.booleanRealEmbedding f =
    ∑ r, fun x =>
      CryptBoolean.symmetricRealWeightProfile
          f ↑r *
        FABL.booleanRealEmbedding
          (CryptBoolean.weightLayerIndicator
            r)
          x
    The real embedding of a symmetric Boolean function is the ordinary real
sum of its disjoint profile-weighted layer indicators.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Krawtchouk.lean
    complete
    theorem CryptBoolean.IsSymmetricBooleanFunction.rawFourierTransform_eq_sum_krawtchoukValue
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) (a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform (FABL.booleanRealEmbedding f) a =
    ∑ r,
      CryptBoolean.symmetricRealWeightProfile f ↑r *
        FABL.krawtchoukValue (↑r) ((FABL.binaryCubeSignEquiv n) a)
    theorem CryptBoolean.IsSymmetricBooleanFunction.rawFourierTransform_eq_sum_krawtchoukValue
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (FABL.booleanRealEmbedding f) a =
    ∑ r,
      CryptBoolean.symmetricRealWeightProfile
          f ↑r *
        FABL.krawtchoukValue (↑r)
          ((FABL.binaryCubeSignEquiv n) a)
    The raw Fourier spectrum of a symmetric Boolean function is the
Krawtchouk linear combination determined by its weight profile.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Krawtchouk.lean
    complete
    theorem CryptBoolean.IsSymmetricBooleanFunction.walshTransform_cast_eq_sum_krawtchoukValue
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) (a : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform f a) =
    (if a = 0 then 2 ^ n else 0) -
      2 *
        ∑ r,
          CryptBoolean.symmetricRealWeightProfile f ↑r *
            FABL.krawtchoukValue (↑r) ((FABL.binaryCubeSignEquiv n) a)
    theorem CryptBoolean.IsSymmetricBooleanFunction.walshTransform_cast_eq_sum_krawtchoukValue
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (a : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform f a) =
    (if a = 0 then 2 ^ n else 0) -
      2 *
        ∑ r,
          CryptBoolean.symmetricRealWeightProfile
              f ↑r *
            FABL.krawtchoukValue (↑r)
              ((FABL.binaryCubeSignEquiv
                  n)
                a)
    The Walsh spectrum of a symmetric Boolean function is obtained from its
profile Krawtchouk combination by the zero-frequency correction.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Krawtchouk.lean
    complete
    theorem CryptBoolean.sum_krawtchoukValue_binaryCubeSignEquiv {n : ℕ}
  (a : FABL.F₂Cube n) :
  ∑ r, FABL.krawtchoukValue (↑r) ((FABL.binaryCubeSignEquiv n) a) =
    if a = 0 then 2 ^ n else 0
    theorem CryptBoolean.sum_krawtchoukValue_binaryCubeSignEquiv
  {n : ℕ} (a : FABL.F₂Cube n) :
  ∑ r,
      FABL.krawtchoukValue (↑r)
        ((FABL.binaryCubeSignEquiv n) a) =
    if a = 0 then 2 ^ n else 0
    Summing every Krawtchouk layer at a binary frequency gives the
zero-frequency point mass.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Krawtchouk.lean
    complete
    theorem CryptBoolean.IsSymmetricBooleanFunction.walshTransform_cast_eq_sum_signed_krawtchoukValue
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) (a : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform f a) =
    ∑ r,
      (-1) ^ ZMod.val (CryptBoolean.symmetricWeightProfile f r) *
        FABL.krawtchoukValue (↑r) ((FABL.binaryCubeSignEquiv n) a)
    theorem CryptBoolean.IsSymmetricBooleanFunction.walshTransform_cast_eq_sum_signed_krawtchoukValue
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (a : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform f a) =
    ∑ r,
      (-1) ^
          ZMod.val
            (CryptBoolean.symmetricWeightProfile
              f r) *
        FABL.krawtchoukValue (↑r)
          ((FABL.binaryCubeSignEquiv n) a)
    Carlet's Walsh formula is the signed Krawtchouk sum determined by the
binary weight profile.