Cryptographic Boolean Functions in Lean

3.8. Autocorrelation indicators🔗

Definition3.8.1
Group: Chapter 3: Boolean functions and cryptography (72)
Group member previews
Preview
Theorem 3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 3
Reverse dependency previews
Preview
Theorem 3.8.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-4relation-38autocorrelationpage-64fidelity-exact-with-zero-dimensional-convention

Relation (38) (Carlet, p. 64). Define the sum-of-squares indicator and absolute indicator by \mathcal V(f)=\sum_{e\in V_n}\Delta_f(e)^2, \qquad \Delta(f)=\max_{e\ne0}|\Delta_f(e)|. Both quantities are invariant under affine equivalence.

Lean code for Definition3.8.1●7 declarations
  • defdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationIndicators.lean
    complete
    def CryptBoolean.sumOfSquaresIndicator {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : ℝ
    def CryptBoolean.sumOfSquaresIndicator {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : ℝ
    Carlet's sum-of-squares indicator `V(f)`.
  • defdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationIndicators.lean
    complete
    def CryptBoolean.absoluteIndicator {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : ℝ
    def CryptBoolean.absoluteIndicator {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : ℝ
    Carlet's absolute indicator. In dimension zero the empty supremum is defined to be zero.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationIndicators.lean
    complete
    theorem CryptBoolean.booleanDerivative_comp_affineEquiv {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (L : FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂] FABL.F₂Cube n) (e x : FABL.F₂Cube n) :
  FABL.booleanDerivative (f ∘ ⇑L) e x =
    FABL.booleanDerivative f (L.linear e) (L x)
    theorem CryptBoolean.booleanDerivative_comp_affineEquiv
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n)
  (e x : FABL.F₂Cube n) :
  FABL.booleanDerivative (f ∘ ⇑L) e x =
    FABL.booleanDerivative f (L.linear e)
      (L x)
    Binary differentiation commutes with an affine input equivalence, with directions transformed
by its linear part.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationIndicators.lean
    complete
    theorem CryptBoolean.autocorrelation_comp_affineEquiv {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (L : FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂] FABL.F₂Cube n) (e : FABL.F₂Cube n) :
  CryptBoolean.autocorrelation (f ∘ ⇑L) e =
    CryptBoolean.autocorrelation f (L.linear e)
    theorem CryptBoolean.autocorrelation_comp_affineEquiv
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n)
  (e : FABL.F₂Cube n) :
  CryptBoolean.autocorrelation (f ∘ ⇑L)
      e =
    CryptBoolean.autocorrelation f
      (L.linear e)
    Autocorrelation is reindexed by the linear part of an affine input equivalence.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationIndicators.lean
    complete
    theorem CryptBoolean.sumOfSquaresIndicator_comp_affineEquiv {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (L : FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂] FABL.F₂Cube n) :
  CryptBoolean.sumOfSquaresIndicator (f ∘ ⇑L) =
    CryptBoolean.sumOfSquaresIndicator f
    theorem CryptBoolean.sumOfSquaresIndicator_comp_affineEquiv
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  CryptBoolean.sumOfSquaresIndicator
      (f ∘ ⇑L) =
    CryptBoolean.sumOfSquaresIndicator f
    The sum-of-squares indicator is invariant under affine equivalence.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationIndicators.lean
    complete
    theorem CryptBoolean.absoluteIndicator_comp_affineEquiv {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (L : FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂] FABL.F₂Cube n) :
  CryptBoolean.absoluteIndicator (f ∘ ⇑L) =
    CryptBoolean.absoluteIndicator f
    theorem CryptBoolean.absoluteIndicator_comp_affineEquiv
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  CryptBoolean.absoluteIndicator
      (f ∘ ⇑L) =
    CryptBoolean.absoluteIndicator f
    The absolute indicator is invariant under affine equivalence.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationIndicators.lean
    complete
    theorem CryptBoolean.absoluteIndicator_zero_dimension
  (f : CryptBoolean.BooleanFunction 0) :
  CryptBoolean.absoluteIndicator f = 0
    theorem CryptBoolean.absoluteIndicator_zero_dimension
  (f : CryptBoolean.BooleanFunction 0) :
  CryptBoolean.absoluteIndicator f = 0
    The absolute indicator of a zero-variable Boolean function follows the empty-family
convention.
Theorem3.8.2
Group: Chapter 3: Boolean functions and cryptography (72)
Group member previews
Preview
Theorem 3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 1.7.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-4autocorrelationindicatorspages-64-65fidelity-exact

Bounds for autocorrelation indicators (Carlet, pp. 64--65). One has \mathcal V(f)\ge2^{2n}, \qquad \Delta(f)\ge \sqrt{\frac{\mathcal V(f)-2^{2n}}{2^n-1}}. The second inequality is asserted for n>0. Equality \mathcal V(f)=2^{2n} holds exactly when every nonzero derivative is balanced. If \dim\ker_{\mathrm{lin}}(f)=k, then \mathcal V(f)\ge2^{2n+k}.

Lean code for Theorem3.8.2●8 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationBounds.lean
    complete
    theorem CryptBoolean.autocorrelation_zero {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.autocorrelation f 0 = 2 ^ n
    theorem CryptBoolean.autocorrelation_zero {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.autocorrelation f 0 = 2 ^ n
    The zero-direction autocorrelation is the cardinality of the Boolean cube.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationBounds.lean
    complete
    theorem CryptBoolean.sumOfSquaresIndicator_lower_bound {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  2 ^ (2 * n) ≤ CryptBoolean.sumOfSquaresIndicator f
    theorem CryptBoolean.sumOfSquaresIndicator_lower_bound
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  2 ^ (2 * n) ≤
    CryptBoolean.sumOfSquaresIndicator f
    Carlet's universal lower bound `V(f) ≥ 2^(2n)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationBounds.lean
    complete
    theorem CryptBoolean.sumOfSquaresIndicator_eq_two_pow_iff {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.sumOfSquaresIndicator f = 2 ^ (2 * n) ↔
    ∀ (e : FABL.F₂Cube n),
      e ≠ 0 → CryptBoolean.IsBalanced (FABL.booleanDerivative f e)
    theorem CryptBoolean.sumOfSquaresIndicator_eq_two_pow_iff
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.sumOfSquaresIndicator f =
      2 ^ (2 * n) ↔
    ∀ (e : FABL.F₂Cube n),
      e ≠ 0 →
        CryptBoolean.IsBalanced
          (FABL.booleanDerivative f e)
    Equality in the universal indicator bound holds exactly when every nonzero derivative is
balanced.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationBounds.lean
    complete
    theorem CryptBoolean.absoluteIndicator_sq_lower_bound {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hn : 0 < n) :
  (CryptBoolean.sumOfSquaresIndicator f - 2 ^ (2 * n)) / (2 ^ n - 1) ≤
    CryptBoolean.absoluteIndicator f ^ 2
    theorem CryptBoolean.absoluteIndicator_sq_lower_bound
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n) :
  (CryptBoolean.sumOfSquaresIndicator f -
        2 ^ (2 * n)) /
      (2 ^ n - 1) ≤
    CryptBoolean.absoluteIndicator f ^ 2
    The square of the absolute indicator dominates the mean squared nonzero autocorrelation.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationBounds.lean
    complete
    theorem CryptBoolean.absoluteIndicator_lower_bound {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hn : 0 < n) :
  √((CryptBoolean.sumOfSquaresIndicator f - 2 ^ (2 * n)) /
        (2 ^ n - 1)) ≤
    CryptBoolean.absoluteIndicator f
    theorem CryptBoolean.absoluteIndicator_lower_bound
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n) :
  √((CryptBoolean.sumOfSquaresIndicator
            f -
          2 ^ (2 * n)) /
        (2 ^ n - 1)) ≤
    CryptBoolean.absoluteIndicator f
    In positive dimension, the absolute indicator is at least the square root of the mean squared
nonzero autocorrelation.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationBounds.lean
    complete
    theorem CryptBoolean.autocorrelation_sq_of_mem_linearKernel {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (e : FABL.F₂Cube n)
  (he : e ∈ CryptBoolean.linearKernel f) :
  CryptBoolean.autocorrelation f e ^ 2 = 2 ^ (2 * n)
    theorem CryptBoolean.autocorrelation_sq_of_mem_linearKernel
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (e : FABL.F₂Cube n)
  (he : e ∈ CryptBoolean.linearKernel f) :
  CryptBoolean.autocorrelation f e ^ 2 =
    2 ^ (2 * n)
    A linear-structure direction contributes the full squared cube cardinality to the indicator.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationBounds.lean
    complete
    theorem CryptBoolean.sumOfSquaresIndicator_lower_bound_linearKernel {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  2 ^ (2 * n + Module.finrank FABL.𝔽₂ ↥(CryptBoolean.linearKernel f)) ≤
    CryptBoolean.sumOfSquaresIndicator f
    theorem CryptBoolean.sumOfSquaresIndicator_lower_bound_linearKernel
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  2 ^
      (2 * n +
        Module.finrank FABL.𝔽₂
          ↥(CryptBoolean.linearKernel
              f)) ≤
    CryptBoolean.sumOfSquaresIndicator f
    A `k`-dimensional linear kernel strengthens Carlet's indicator bound to `2^(2n+k)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationBounds.lean
    complete
    theorem CryptBoolean.sumOfSquaresIndicator_lower_bound_of_finrank_eq {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (k : ℕ)
  (hk : Module.finrank FABL.𝔽₂ ↥(CryptBoolean.linearKernel f) = k) :
  2 ^ (2 * n + k) ≤ CryptBoolean.sumOfSquaresIndicator f
    theorem CryptBoolean.sumOfSquaresIndicator_lower_bound_of_finrank_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (k : ℕ)
  (hk :
    Module.finrank FABL.𝔽₂
        ↥(CryptBoolean.linearKernel f) =
      k) :
  2 ^ (2 * n + k) ≤
    CryptBoolean.sumOfSquaresIndicator f
    Source-form specialization of the linear-kernel bound when its dimension is named `k`.
Theorem3.8.3
Group: Chapter 3: Boolean functions and cryptography (72)
Group member previews
Preview
Theorem 3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Corollary 1.10.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-4second-derivativepage-65fidelity-exact

Second-derivative expression for the indicator (Carlet, p. 65). With D_aD_ef(x)=f(x)+f(x+a)+f(x+e)+f(x+a+e), one has \mathcal V(f)=\sum_{a,e\in V_n}\mathcal F(D_aD_ef), where \mathcal F(h)=\sum_x(-1)^{h(x)}.

Lean code for Theorem3.8.3●3 declarations
  • defdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationIdentities.lean
    complete
    def CryptBoolean.secondBooleanDerivative {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (a e : FABL.F₂Cube n) :
  CryptBoolean.BooleanFunction n
    def CryptBoolean.secondBooleanDerivative
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a e : FABL.F₂Cube n) :
  CryptBoolean.BooleanFunction n
    Carlet's second-order derivative `D_a D_e f`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationIdentities.lean
    complete
    theorem CryptBoolean.secondBooleanDerivative_apply {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (a e x : FABL.F₂Cube n) :
  CryptBoolean.secondBooleanDerivative f a e x =
    f x + f (x + a) + f (x + e) + f (x + a + e)
    theorem CryptBoolean.secondBooleanDerivative_apply
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a e x : FABL.F₂Cube n) :
  CryptBoolean.secondBooleanDerivative f a
      e x =
    f x + f (x + a) + f (x + e) +
      f (x + a + e)
    The second-order derivative is the four-term binary difference displayed by Carlet.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationIdentities.lean
    complete
    theorem CryptBoolean.sumOfSquaresIndicator_eq_sum_secondBooleanDerivative
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.sumOfSquaresIndicator f =
    ∑ a,
      ∑ e,
        ∑ x,
          CryptBoolean.realSignView
            (CryptBoolean.secondBooleanDerivative f a e) x
    theorem CryptBoolean.sumOfSquaresIndicator_eq_sum_secondBooleanDerivative
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.sumOfSquaresIndicator f =
    ∑ a,
      ∑ e,
        ∑ x,
          CryptBoolean.realSignView
            (CryptBoolean.secondBooleanDerivative
              f a e)
            x
    Carlet's second-derivative expression for the sum-of-squares indicator.
Theorem3.8.4
Group: Chapter 3: Boolean functions and cryptography (72)
Group member previews
Preview
Theorem 3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 1.8.9
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-4relation-39fourth-momentpages-65-66fidelity-exact

Relation (39) (Carlet, pp. 65--66). For every a\in V_n, \sum_{e\in V_n}W_f(e)^2W_f(a+e)^2 =2^n\sum_{e\in V_n}\Delta_f(e)^2(-1)^{e\mathbin\cdot a}. In particular, \sum_{e\in V_n}W_f(e)^4=2^n\mathcal V(f).

Lean code for Theorem3.8.4●2 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationIdentities.lean
    complete
    theorem CryptBoolean.sum_walshTransform_sq_mul_add_sq_eq {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n) :
  ∑ e,
      ↑(CryptBoolean.walshTransform f e) ^ 2 *
        ↑(CryptBoolean.walshTransform f (a + e)) ^ 2 =
    2 ^ n *
      ∑ e,
        CryptBoolean.autocorrelation f e ^ 2 *
          (FABL.vectorWalshCharacter a) e
    theorem CryptBoolean.sum_walshTransform_sq_mul_add_sq_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  ∑ e,
      ↑(CryptBoolean.walshTransform f e) ^
          2 *
        ↑(CryptBoolean.walshTransform f
              (a + e)) ^
          2 =
    2 ^ n *
      ∑ e,
        CryptBoolean.autocorrelation f e ^
            2 *
          (FABL.vectorWalshCharacter a) e
    Carlet Relation (39): shifted Walsh-spectrum squares are the transform of squared
autocorrelation.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/AutocorrelationIdentities.lean
    complete
    theorem CryptBoolean.sum_walshTransform_fourth_eq_two_pow_mul_sumOfSquaresIndicator
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  ∑ e, ↑(CryptBoolean.walshTransform f e) ^ 4 =
    2 ^ n * CryptBoolean.sumOfSquaresIndicator f
    theorem CryptBoolean.sum_walshTransform_fourth_eq_two_pow_mul_sumOfSquaresIndicator
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∑ e,
      ↑(CryptBoolean.walshTransform f e) ^
        4 =
    2 ^ n *
      CryptBoolean.sumOfSquaresIndicator f
    The zero-shift specialization of Relation (39): the fourth Walsh moment is `2^n V(f)`.
Theorem3.8.5
Group: Chapter 3: Boolean functions and cryptography (72)
Group member previews
Preview
Theorem 3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 5
Statement dependency previews
Preview
Theorem 1.9.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-4autocorrelationnonlinearityplateauedpages-65-66fidelity-exact-equality-cases

Indicator, nonlinearity, and Walsh-support bounds (Carlet, pp. 65--66). The fourth-moment identities imply \operatorname{nl}(f) \le2^{n-1}-2^{-n/2-1}\sqrt{\mathcal V(f)} \le2^{n-1}-\frac12\mathcal V(f)^{1/4}. If N_W=|\operatorname{supp}(W_f)|, then \mathcal V(f)N_W\ge2^{3n}. Equality in the first nonlinearity bound or in the product bound occurs exactly when all nonzero Walsh values have one common magnitude; equality in the fourth-root bound occurs exactly for bent functions.

Lean code for Theorem3.8.5●16 declarations
  • defdefined in CryptBoolean/Carlet/Chapter04/IndicatorSpectralBounds.lean
    complete
    def CryptBoolean.HasPlateauedWalshSpectrum {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : Prop
    def CryptBoolean.HasPlateauedWalshSpectrum
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    A Boolean function is plateaued when all nonzero raw Walsh coefficients have one magnitude.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/IndicatorSpectralBounds.lean
    complete
    theorem CryptBoolean.abs_walshTransform_le_maxWalshMagnitude {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n) :
  |↑(CryptBoolean.walshTransform f a)| ≤
    ↑(CryptBoolean.maxWalshMagnitude f)
    theorem CryptBoolean.abs_walshTransform_le_maxWalshMagnitude
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  |↑(CryptBoolean.walshTransform f a)| ≤
    ↑(CryptBoolean.maxWalshMagnitude f)
    Every raw Walsh coefficient is bounded by Carlet's maximum Walsh magnitude.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/IndicatorSpectralBounds.lean
    complete
    theorem CryptBoolean.sum_walshTransform_fourth_le_sum_sq_mul_maxWalshMagnitude_sq
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  ∑ a, ↑(CryptBoolean.walshTransform f a) ^ 4 ≤
    (∑ a, ↑(CryptBoolean.walshTransform f a) ^ 2) *
      ↑(CryptBoolean.maxWalshMagnitude f) ^ 2
    theorem CryptBoolean.sum_walshTransform_fourth_le_sum_sq_mul_maxWalshMagnitude_sq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∑ a,
      ↑(CryptBoolean.walshTransform f a) ^
        4 ≤
    (∑ a,
        ↑(CryptBoolean.walshTransform f
              a) ^
          2) *
      ↑(CryptBoolean.maxWalshMagnitude
            f) ^
        2
    The fourth Walsh moment is bounded by the second moment times the squared peak magnitude.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/IndicatorSpectralBounds.lean
    complete
    theorem CryptBoolean.sum_walshTransform_fourth_le_two_pow_mul_maxWalshMagnitude_fourth
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  ∑ a, ↑(CryptBoolean.walshTransform f a) ^ 4 ≤
    2 ^ n * ↑(CryptBoolean.maxWalshMagnitude f) ^ 4
    theorem CryptBoolean.sum_walshTransform_fourth_le_two_pow_mul_maxWalshMagnitude_fourth
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∑ a,
      ↑(CryptBoolean.walshTransform f a) ^
        4 ≤
    2 ^ n *
      ↑(CryptBoolean.maxWalshMagnitude
            f) ^
        4
    The fourth Walsh moment is bounded by the cube cardinality times the fourth power of its
peak magnitude.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/IndicatorSpectralBounds.lean
    complete
    theorem CryptBoolean.sumOfSquaresIndicator_div_two_pow_le_maxWalshMagnitude_sq
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.sumOfSquaresIndicator f / 2 ^ n ≤
    ↑(CryptBoolean.maxWalshMagnitude f) ^ 2
    theorem CryptBoolean.sumOfSquaresIndicator_div_two_pow_le_maxWalshMagnitude_sq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.sumOfSquaresIndicator f /
      2 ^ n ≤
    ↑(CryptBoolean.maxWalshMagnitude f) ^
      2
    The squared peak Walsh magnitude is at least `V(f) / 2^n`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/IndicatorSpectralBounds.lean
    complete
    theorem CryptBoolean.sumOfSquaresIndicator_le_maxWalshMagnitude_fourth {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.sumOfSquaresIndicator f ≤
    ↑(CryptBoolean.maxWalshMagnitude f) ^ 4
    theorem CryptBoolean.sumOfSquaresIndicator_le_maxWalshMagnitude_fourth
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.sumOfSquaresIndicator f ≤
    ↑(CryptBoolean.maxWalshMagnitude f) ^
      4
    The fourth power of the peak Walsh magnitude is at least `V(f)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/IndicatorSpectralBounds.lean
    complete
    theorem CryptBoolean.inv_sqrt_two_pow_mul_sqrt_sumOfSquaresIndicator_le_maxWalshMagnitude
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  (√(2 ^ n))⁻¹ * √(CryptBoolean.sumOfSquaresIndicator f) ≤
    ↑(CryptBoolean.maxWalshMagnitude f)
    theorem CryptBoolean.inv_sqrt_two_pow_mul_sqrt_sumOfSquaresIndicator_le_maxWalshMagnitude
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  (√(2 ^ n))⁻¹ *
      √(CryptBoolean.sumOfSquaresIndicator
          f) ≤
    ↑(CryptBoolean.maxWalshMagnitude f)
    The peak Walsh magnitude dominates the square-root expression in Carlet's first indicator
bound.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/IndicatorSpectralBounds.lean
    complete
    theorem CryptBoolean.rpow_one_fourth_sumOfSquaresIndicator_le_maxWalshMagnitude
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.sumOfSquaresIndicator f ^ (1 / 4) ≤
    ↑(CryptBoolean.maxWalshMagnitude f)
    theorem CryptBoolean.rpow_one_fourth_sumOfSquaresIndicator_le_maxWalshMagnitude
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.sumOfSquaresIndicator f ^
      (1 / 4) ≤
    ↑(CryptBoolean.maxWalshMagnitude f)
    The peak Walsh magnitude dominates the real fourth root of `V(f)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/IndicatorSpectralBounds.lean
    complete
    theorem CryptBoolean.nonlinearity_cast_le_sqrt_sumOfSquaresIndicator_bound
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) ≤
    2 ^ n / 2 -
      (√(2 ^ n))⁻¹ * √(CryptBoolean.sumOfSquaresIndicator f) / 2
    theorem CryptBoolean.nonlinearity_cast_le_sqrt_sumOfSquaresIndicator_bound
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) ≤
    2 ^ n / 2 -
      (√(2 ^ n))⁻¹ *
          √(CryptBoolean.sumOfSquaresIndicator
              f) /
        2
    Carlet's first fourth-moment nonlinearity bound.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/IndicatorSpectralBounds.lean
    complete
    theorem CryptBoolean.nonlinearity_cast_le_fourthRoot_sumOfSquaresIndicator_bound
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) ≤
    2 ^ n / 2 - CryptBoolean.sumOfSquaresIndicator f ^ (1 / 4) / 2
    theorem CryptBoolean.nonlinearity_cast_le_fourthRoot_sumOfSquaresIndicator_bound
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) ≤
    2 ^ n / 2 -
      CryptBoolean.sumOfSquaresIndicator
            f ^
          (1 / 4) /
        2
    Carlet's second fourth-moment nonlinearity bound.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/IndicatorSpectralBounds.lean
    complete
    theorem CryptBoolean.sum_walshTransform_fourth_eq_sum_sq_mul_maxWalshMagnitude_sq_iff_plateaued
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  ∑ a, ↑(CryptBoolean.walshTransform f a) ^ 4 =
      (∑ a, ↑(CryptBoolean.walshTransform f a) ^ 2) *
        ↑(CryptBoolean.maxWalshMagnitude f) ^ 2 ↔
    CryptBoolean.HasPlateauedWalshSpectrum f
    theorem CryptBoolean.sum_walshTransform_fourth_eq_sum_sq_mul_maxWalshMagnitude_sq_iff_plateaued
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∑ a,
        ↑(CryptBoolean.walshTransform f
              a) ^
          4 =
      (∑ a,
          ↑(CryptBoolean.walshTransform f
                a) ^
            2) *
        ↑(CryptBoolean.maxWalshMagnitude
              f) ^
          2 ↔
    CryptBoolean.HasPlateauedWalshSpectrum
      f
    Equality in the first fourth-moment estimate is equivalent to plateauedness.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/IndicatorSpectralBounds.lean
    complete
    theorem CryptBoolean.sum_walshTransform_fourth_eq_two_pow_mul_maxWalshMagnitude_fourth_iff_flat
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  ∑ a, ↑(CryptBoolean.walshTransform f a) ^ 4 =
      2 ^ n * ↑(CryptBoolean.maxWalshMagnitude f) ^ 4 ↔
    CryptBoolean.HasFlatWalshSpectrum f
    theorem CryptBoolean.sum_walshTransform_fourth_eq_two_pow_mul_maxWalshMagnitude_fourth_iff_flat
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∑ a,
        ↑(CryptBoolean.walshTransform f
              a) ^
          4 =
      2 ^ n *
        ↑(CryptBoolean.maxWalshMagnitude
              f) ^
          4 ↔
    CryptBoolean.HasFlatWalshSpectrum f
    Equality in the second fourth-moment estimate is equivalent to a flat Walsh spectrum.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/IndicatorSpectralBounds.lean
    complete
    theorem CryptBoolean.nonlinearity_cast_eq_sqrt_sumOfSquaresIndicator_bound_iff_plateaued
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) =
      2 ^ n / 2 -
        (√(2 ^ n))⁻¹ * √(CryptBoolean.sumOfSquaresIndicator f) / 2 ↔
    CryptBoolean.HasPlateauedWalshSpectrum f
    theorem CryptBoolean.nonlinearity_cast_eq_sqrt_sumOfSquaresIndicator_bound_iff_plateaued
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) =
      2 ^ n / 2 -
        (√(2 ^ n))⁻¹ *
            √(CryptBoolean.sumOfSquaresIndicator
                f) /
          2 ↔
    CryptBoolean.HasPlateauedWalshSpectrum
      f
    Equality in Carlet's first indicator nonlinearity bound holds exactly for plateaued
functions.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/IndicatorSpectralBounds.lean
    complete
    theorem CryptBoolean.nonlinearity_cast_eq_fourthRoot_sumOfSquaresIndicator_bound_iff_bent
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) =
      2 ^ n / 2 - CryptBoolean.sumOfSquaresIndicator f ^ (1 / 4) / 2 ↔
    CryptBoolean.IsBent f
    theorem CryptBoolean.nonlinearity_cast_eq_fourthRoot_sumOfSquaresIndicator_bound_iff_bent
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) =
      2 ^ n / 2 -
        CryptBoolean.sumOfSquaresIndicator
              f ^
            (1 / 4) /
          2 ↔
    CryptBoolean.IsBent f
    Equality in Carlet's fourth-root nonlinearity bound holds exactly for bent functions.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/IndicatorSpectralBounds.lean
    complete
    theorem CryptBoolean.two_pow_three_mul_n_le_sumOfSquaresIndicator_mul_card_walshSupport
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  2 ^ (3 * n) ≤
    CryptBoolean.sumOfSquaresIndicator f *
      ↑(CryptBoolean.walshSupport f).card
    theorem CryptBoolean.two_pow_three_mul_n_le_sumOfSquaresIndicator_mul_card_walshSupport
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  2 ^ (3 * n) ≤
    CryptBoolean.sumOfSquaresIndicator f *
      ↑(CryptBoolean.walshSupport f).card
    Carlet's Walsh-support product bound `2^(3n) ≤ V(f) |supp(W_f)|`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/IndicatorSpectralBounds.lean
    complete
    theorem CryptBoolean.sumOfSquaresIndicator_mul_card_walshSupport_eq_two_pow_three_mul_n_iff_plateaued
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.sumOfSquaresIndicator f *
        ↑(CryptBoolean.walshSupport f).card =
      2 ^ (3 * n) ↔
    CryptBoolean.HasPlateauedWalshSpectrum f
    theorem CryptBoolean.sumOfSquaresIndicator_mul_card_walshSupport_eq_two_pow_three_mul_n_iff_plateaued
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.sumOfSquaresIndicator f *
        ↑(CryptBoolean.walshSupport
              f).card =
      2 ^ (3 * n) ↔
    CryptBoolean.HasPlateauedWalshSpectrum
      f
    Equality in the Walsh-support product bound holds exactly for plateaued functions.