4.4. Normal functions🔗

Theorem4.4.1

Group: Chapter 4: Classes with Provable Spectra and Weights (30)

Group member previews

Preview

Theorem 4.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Corollary 1.8.6

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Corollary 4.4.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagscarletchapter-5restrictionsnonlinearityrelation-42pages-71-72fidelity-exact-with-division-free-total-form

Restriction nonlinearity bound (Carlet, Relation (42), pp. 71--72). Let E,E' be complementary subspaces of V_n, let \dim(E)=k, and, for each a\in E', let h_a be the Boolean function on E obtained by restricting f to a+E. Then, for every a\in E', \operatorname{nl}(f) \le 2^{n-1}-2^{k-1}+\operatorname{nl}(h_a).

Lean code for Theorem4.4.1●10 declarations

defdefined in CryptBoolean/Carlet/Chapter02/AffineSubspaceRestrictions.lean

complete

def CryptBoolean.coordinateAffineSubspaceRestriction {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) : CryptBoolean.BooleanFunction k

def CryptBoolean.coordinateAffineSubspaceRestriction
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) :
  CryptBoolean.BooleanFunction k

The restriction to `a + E`, reindexed by binary coordinates on `E`.

theoremdefined in CryptBoolean/Carlet/Chapter05/RestrictionNonlinearity.lean

complete

theorem CryptBoolean.coordinateAffineSubspaceDimension_le {n k : ℕ}
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) : k ≤ n

theorem CryptBoolean.coordinateAffineSubspaceDimension_le
  {n k : ℕ}
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) :
  k ≤ n

A binary coordinate model of a subspace cannot have dimension larger
than the ambient cube.

theoremdefined in CryptBoolean/Carlet/Chapter05/RestrictionNonlinearity.lean

complete

theorem CryptBoolean.exists_ambientFrequency_restricts_to_subspace {n k : ℕ}
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) (c : FABL.F₂Cube k) :
  ∃ b,
    ∀ (y : FABL.F₂Cube k),
      FABL.f₂DotProduct b ↑(e y) = FABL.f₂DotProduct c y

theorem CryptBoolean.exists_ambientFrequency_restricts_to_subspace
  {n k : ℕ}
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E)
  (c : FABL.F₂Cube k) :
  ∃ b,
    ∀ (y : FABL.F₂Cube k),
      FABL.f₂DotProduct b ↑(e y) =
        FABL.f₂DotProduct c y

Every binary frequency on coordinates of a subspace extends to an
ambient dot-product frequency.

theoremdefined in CryptBoolean/Carlet/Chapter05/RestrictionNonlinearity.lean

complete

theorem CryptBoolean.sum_walshTransform_perpendicularCoset_eq_restriction
  {n k : ℕ} (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) (c : FABL.F₂Cube k)
  (b : FABL.F₂Cube n)
  (hb :
    ∀ (y : FABL.F₂Cube k),
      FABL.f₂DotProduct b ↑(e y) = FABL.f₂DotProduct c y) :
  ∑ u,
      (FABL.vectorWalshCharacter a) (b + ↑u) *
        ↑(CryptBoolean.walshTransform f (b + ↑u)) =
    ↑(Nat.card ↥(FABL.perpendicularSubspace E)) *
      ↑(CryptBoolean.walshTransform
          (CryptBoolean.coordinateAffineSubspaceRestriction f E a e) c)

theorem CryptBoolean.sum_walshTransform_perpendicularCoset_eq_restriction
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E)
  (c : FABL.F₂Cube k) (b : FABL.F₂Cube n)
  (hb :
    ∀ (y : FABL.F₂Cube k),
      FABL.f₂DotProduct b ↑(e y) =
        FABL.f₂DotProduct c y) :
  ∑ u,
      (FABL.vectorWalshCharacter a)
          (b + ↑u) *
        ↑(CryptBoolean.walshTransform f
            (b + ↑u)) =
    ↑(Nat.card
          ↥(FABL.perpendicularSubspace
              E)) *
      ↑(CryptBoolean.walshTransform
          (CryptBoolean.coordinateAffineSubspaceRestriction
            f E a e)
          c)

Poisson summation expresses a Walsh coefficient of a coset restriction
as the signed mean of an ambient Walsh coset.

theoremdefined in CryptBoolean/Carlet/Chapter05/RestrictionNonlinearity.lean

complete

theorem CryptBoolean.abs_walshTransform_coordinateAffineSubspaceRestriction_le
  {n k : ℕ} (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) (c : FABL.F₂Cube k) :
  |↑(CryptBoolean.walshTransform
          (CryptBoolean.coordinateAffineSubspaceRestriction f E a e)
          c)| ≤
    ↑(CryptBoolean.maxWalshMagnitude f)

theorem CryptBoolean.abs_walshTransform_coordinateAffineSubspaceRestriction_le
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E)
  (c : FABL.F₂Cube k) :
  |↑(CryptBoolean.walshTransform
          (CryptBoolean.coordinateAffineSubspaceRestriction
            f E a e)
          c)| ≤
    ↑(CryptBoolean.maxWalshMagnitude f)

Every Walsh magnitude of an affine-flat restriction is bounded by the
ambient maximum Walsh magnitude.

theoremdefined in CryptBoolean/Carlet/Chapter05/RestrictionNonlinearity.lean

complete

theorem CryptBoolean.maxWalshMagnitude_coordinateAffineSubspaceRestriction_le
  {n k : ℕ} (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) :
  CryptBoolean.maxWalshMagnitude
      (CryptBoolean.coordinateAffineSubspaceRestriction f E a e) ≤
    CryptBoolean.maxWalshMagnitude f

theorem CryptBoolean.maxWalshMagnitude_coordinateAffineSubspaceRestriction_le
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) :
  CryptBoolean.maxWalshMagnitude
      (CryptBoolean.coordinateAffineSubspaceRestriction
        f E a e) ≤
    CryptBoolean.maxWalshMagnitude f

Passing to an affine-flat restriction cannot increase the maximum raw
Walsh magnitude.

theoremdefined in CryptBoolean/Carlet/Chapter05/RestrictionNonlinearity.lean

complete

theorem CryptBoolean.two_mul_nonlinearity_add_two_pow_le_restriction {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) :
  2 * CryptBoolean.nonlinearity f + 2 ^ k ≤
    2 ^ n +
      2 *
        CryptBoolean.nonlinearity
          (CryptBoolean.coordinateAffineSubspaceRestriction f E a e)

theorem CryptBoolean.two_mul_nonlinearity_add_two_pow_le_restriction
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) :
  2 * CryptBoolean.nonlinearity f +
      2 ^ k ≤
    2 ^ n +
      2 *
        CryptBoolean.nonlinearity
          (CryptBoolean.coordinateAffineSubspaceRestriction
            f E a e)

The division-free, all-dimensions form of Carlet Relation (42).

theoremdefined in CryptBoolean/Carlet/Chapter05/RestrictionNonlinearity.lean

complete

theorem CryptBoolean.nonlinearity_cast_le_restriction_relation_42 {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) :
  ↑(CryptBoolean.nonlinearity f) ≤
    2 ^ n / 2 - 2 ^ k / 2 +
      ↑(CryptBoolean.nonlinearity
          (CryptBoolean.coordinateAffineSubspaceRestriction f E a e))

theorem CryptBoolean.nonlinearity_cast_le_restriction_relation_42
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) :
  ↑(CryptBoolean.nonlinearity f) ≤
    2 ^ n / 2 - 2 ^ k / 2 +
      ↑(CryptBoolean.nonlinearity
          (CryptBoolean.coordinateAffineSubspaceRestriction
            f E a e))

Carlet Relation (42), written over the reals so the half-cardinality
terms remain total in dimensions zero and one.

theoremdefined in CryptBoolean/Carlet/Chapter05/RestrictionNonlinearity.lean

complete

theorem CryptBoolean.nonlinearity_le_restriction_relation_42 {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) (hk : 1 ≤ k) :
  CryptBoolean.nonlinearity f ≤
    2 ^ (n - 1) - 2 ^ (k - 1) +
      CryptBoolean.nonlinearity
        (CryptBoolean.coordinateAffineSubspaceRestriction f E a e)

theorem CryptBoolean.nonlinearity_le_restriction_relation_42
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E)
  (hk : 1 ≤ k) :
  CryptBoolean.nonlinearity f ≤
    2 ^ (n - 1) - 2 ^ (k - 1) +
      CryptBoolean.nonlinearity
        (CryptBoolean.coordinateAffineSubspaceRestriction
          f E a e)

The natural-number exponent form of Relation (42) in positive flat
dimension.

theoremdefined in CryptBoolean/Carlet/Chapter05/RestrictionNonlinearity.lean

complete

theorem CryptBoolean.nonlinearity_le_restriction_relation_42_of_isCompl
  {n k : ℕ} (f : CryptBoolean.BooleanFunction n)
  (E E' : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (_hcompl : IsCompl E E')
  (a : ↥E') (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) (hk : 1 ≤ k) :
  CryptBoolean.nonlinearity f ≤
    2 ^ (n - 1) - 2 ^ (k - 1) +
      CryptBoolean.nonlinearity
        (CryptBoolean.coordinateAffineSubspaceRestriction f E (↑a) e)

theorem CryptBoolean.nonlinearity_le_restriction_relation_42_of_isCompl
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E E' :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (_hcompl : IsCompl E E') (a : ↥E')
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E)
  (hk : 1 ≤ k) :
  CryptBoolean.nonlinearity f ≤
    2 ^ (n - 1) - 2 ^ (k - 1) +
      CryptBoolean.nonlinearity
        (CryptBoolean.coordinateAffineSubspaceRestriction
          f E (↑a) e)

Relation (42) in Carlet's complementary-subspace parameterization.

Carlet's alternative proof from the Poisson formula yields the displayed inequality. Its division-free form remains valid for k=0; the natural-exponent form assumes 1\le k.

Corollary4.4.2

Group: Chapter 4: Classes with Provable Spectra and Weights (30)

Group member previews

Preview

Theorem 4.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Definition 1.4.5

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 4

Reverse dependency previews

Preview

Proposition 5.5.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagscarletchapter-5affine-flatrestrictionsnonlinearitypage-72fidelity-exact-positive-dimension

Affine-flat restriction bound (Carlet, consequence of Relation (42), p. 72). If the restriction of f:V_n\to\mathbb F_2 to a k-dimensional affine flat A is affine, then \operatorname{nl}(f)\le2^{n-1}-2^{k-1}. If equality holds and \ell is any ambient affine extension of that restriction, then f+\ell is balanced on every other coset of the direction space of A.

Lean code for Corollary4.4.2●8 theorems

theoremdefined in CryptBoolean/Carlet/Chapter05/Affine.lean

complete

theorem CryptBoolean.walshTransform_add_affineFunction {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (b : FABL.𝔽₂)
  (a u : FABL.F₂Cube n) :
  CryptBoolean.walshTransform (f + FABL.affineFunction b a) u =
    CryptBoolean.bitSignInt b * CryptBoolean.walshTransform f (u + a)

theorem CryptBoolean.walshTransform_add_affineFunction
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.𝔽₂) (a u : FABL.F₂Cube n) :
  CryptBoolean.walshTransform
      (f + FABL.affineFunction b a) u =
    CryptBoolean.bitSignInt b *
      CryptBoolean.walshTransform f
        (u + a)

Adding an affine Boolean function translates the raw Walsh spectrum and
multiplies it by the sign of the constant term.

theoremdefined in CryptBoolean/Carlet/Chapter05/Affine.lean

complete

theorem CryptBoolean.walshTransform_add_affineFunction_natAbs {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (b : FABL.𝔽₂)
  (a u : FABL.F₂Cube n) :
  (CryptBoolean.walshTransform (f + FABL.affineFunction b a) u).natAbs =
    (CryptBoolean.walshTransform f (u + a)).natAbs

theorem CryptBoolean.walshTransform_add_affineFunction_natAbs
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.𝔽₂) (a u : FABL.F₂Cube n) :
  (CryptBoolean.walshTransform
        (f + FABL.affineFunction b a)
        u).natAbs =
    (CryptBoolean.walshTransform f
        (u + a)).natAbs

Adding an affine Boolean function preserves every raw Walsh magnitude up
to the corresponding frequency translation.

theoremdefined in CryptBoolean/Carlet/Chapter05/RestrictionNonlinearity.lean

complete

theorem CryptBoolean.maxWalshMagnitude_add_affineFunction {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (b : FABL.𝔽₂)
  (a : FABL.F₂Cube n) :
  CryptBoolean.maxWalshMagnitude (f + FABL.affineFunction b a) =
    CryptBoolean.maxWalshMagnitude f

theorem CryptBoolean.maxWalshMagnitude_add_affineFunction
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.𝔽₂) (a : FABL.F₂Cube n) :
  CryptBoolean.maxWalshMagnitude
      (f + FABL.affineFunction b a) =
    CryptBoolean.maxWalshMagnitude f

Adding an affine Boolean function preserves maximum raw Walsh magnitude.

theoremdefined in CryptBoolean/Carlet/Chapter05/RestrictionNonlinearity.lean

complete

theorem CryptBoolean.sum_vectorWalshCharacter_perpendicular_eq_zero_of_not_mem
  {n : ℕ} (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (x : FABL.F₂Cube n)
  (hx : x ∉ E) : ∑ u, (FABL.vectorWalshCharacter x) ↑u = 0

theorem CryptBoolean.sum_vectorWalshCharacter_perpendicular_eq_zero_of_not_mem
  {n : ℕ}
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (x : FABL.F₂Cube n) (hx : x ∉ E) :
  ∑ u, (FABL.vectorWalshCharacter x) ↑u =
    0

A Walsh character indexed outside a subspace sums to zero over the
perpendicular subspace.

theoremdefined in CryptBoolean/Carlet/Chapter05/RestrictionNonlinearity.lean

complete

theorem CryptBoolean.exists_affineFunction_eq_coordinateAffineSubspaceRestriction_of_isAffineOnAffineFlat
  {n k : ℕ} (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E)
  (hflat : CryptBoolean.IsAffineOnAffineFlat f E a) :
  ∃ b c,
    CryptBoolean.coordinateAffineSubspaceRestriction f E a e =
      FABL.affineFunction b c

theorem CryptBoolean.exists_affineFunction_eq_coordinateAffineSubspaceRestriction_of_isAffineOnAffineFlat
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E)
  (hflat :
    CryptBoolean.IsAffineOnAffineFlat f E
      a) :
  ∃ b c,
    CryptBoolean.coordinateAffineSubspaceRestriction
        f E a e =
      FABL.affineFunction b c

An affine restriction on an ambient flat becomes an affine Boolean
function in any binary coordinate model of its direction space.

theoremdefined in CryptBoolean/Carlet/Chapter05/RestrictionNonlinearity.lean

complete

theorem CryptBoolean.nonlinearity_coordinateAffineSubspaceRestriction_eq_zero_of_isAffineOnAffineFlat
  {n k : ℕ} (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E)
  (hflat : CryptBoolean.IsAffineOnAffineFlat f E a) :
  CryptBoolean.nonlinearity
      (CryptBoolean.coordinateAffineSubspaceRestriction f E a e) =
    0

theorem CryptBoolean.nonlinearity_coordinateAffineSubspaceRestriction_eq_zero_of_isAffineOnAffineFlat
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E)
  (hflat :
    CryptBoolean.IsAffineOnAffineFlat f E
      a) :
  CryptBoolean.nonlinearity
      (CryptBoolean.coordinateAffineSubspaceRestriction
        f E a e) =
    0

An affine affine-flat restriction has zero nonlinearity in subspace
coordinates.

theoremdefined in CryptBoolean/Carlet/Chapter05/RestrictionNonlinearity.lean

complete

theorem CryptBoolean.nonlinearity_le_of_isAffineOnAffineFlat {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) (hk : 1 ≤ k)
  (hflat : CryptBoolean.IsAffineOnAffineFlat f E a) :
  CryptBoolean.nonlinearity f ≤ 2 ^ (n - 1) - 2 ^ (k - 1)

theorem CryptBoolean.nonlinearity_le_of_isAffineOnAffineFlat
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E)
  (hk : 1 ≤ k)
  (hflat :
    CryptBoolean.IsAffineOnAffineFlat f E
      a) :
  CryptBoolean.nonlinearity f ≤
    2 ^ (n - 1) - 2 ^ (k - 1)

If a Boolean function is affine on a positive-dimensional affine flat,
its nonlinearity satisfies Carlet's affine-flat bound.

theoremdefined in CryptBoolean/Carlet/Chapter05/RestrictionNonlinearity.lean

complete

theorem CryptBoolean.isBalanced_coordinateAffineSubspaceRestriction_add_affineFunction_of_eq_bound
  {n k : ℕ} (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) (hk : 1 ≤ k) (b : FABL.𝔽₂)
  (c : FABL.F₂Cube n)
  (hextension :
    ∀ x ∈ FABL.binaryAffineSubspace E a,
      f x = FABL.affineFunction b c x)
  (hequality : CryptBoolean.nonlinearity f = 2 ^ (n - 1) - 2 ^ (k - 1))
  (z : FABL.F₂Cube n) (hz : z + a ∉ E) :
  CryptBoolean.IsBalanced
    (CryptBoolean.coordinateAffineSubspaceRestriction
      (f + FABL.affineFunction b c) E z e)

theorem CryptBoolean.isBalanced_coordinateAffineSubspaceRestriction_add_affineFunction_of_eq_bound
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E)
  (hk : 1 ≤ k) (b : FABL.𝔽₂)
  (c : FABL.F₂Cube n)
  (hextension :
    ∀ x ∈ FABL.binaryAffineSubspace E a,
      f x = FABL.affineFunction b c x)
  (hequality :
    CryptBoolean.nonlinearity f =
      2 ^ (n - 1) - 2 ^ (k - 1))
  (z : FABL.F₂Cube n) (hz : z + a ∉ E) :
  CryptBoolean.IsBalanced
    (CryptBoolean.coordinateAffineSubspaceRestriction
      (f + FABL.affineFunction b c) E z e)

Equality in the affine-flat nonlinearity bound forces the sum with any
ambient affine extension to be balanced on every other coset.

The natural-exponent bound assumes 1\le k. In the equality case, z+a\notin E says exactly that z+E is a coset other than a+E.

Definition4.4.3

Group: Chapter 4: Classes with Provable Spectra and Weights (30)

Group member previews

Preview

Theorem 4.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 7

Reverse dependency previews

Preview

Theorem 4.4.4

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagscarletchapter-5definition-4normalityweak-normalitypage-72fidelity-exact-fixed-dimension

Normal and weakly normal functions (Carlet, Definition 4, p. 72). A Boolean function is k-weakly normal when its restriction to some k-dimensional affine flat is affine, and it is k-normal when its restriction to some k-dimensional affine flat is constant. For even n, the unqualified term normal means (n/2)-normal.

Lean code for Definition4.4.3●5 declarations

defdefined in CryptBoolean/Carlet/Chapter05/Normality.lean

complete

def CryptBoolean.IsKNormal {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (k : ℕ) : Prop

def CryptBoolean.IsKNormal {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (k : ℕ) : Prop

A Boolean function is `k`-normal when it is constant on a `k`-dimensional affine flat.

defdefined in CryptBoolean/Carlet/Chapter05/Normality.lean

complete

def CryptBoolean.IsKWeaklyNormal {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (k : ℕ) : Prop

def CryptBoolean.IsKWeaklyNormal {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (k : ℕ) : Prop

A Boolean function is `k`-weakly normal when it is affine on a `k`-dimensional affine flat.

theoremdefined in CryptBoolean/Carlet/Chapter05/Normality.lean

complete

theorem CryptBoolean.IsKNormal.isKWeaklyNormal {n k : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (h : CryptBoolean.IsKNormal f k) : CryptBoolean.IsKWeaklyNormal f k

theorem CryptBoolean.IsKNormal.isKWeaklyNormal
  {n k : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (h : CryptBoolean.IsKNormal f k) :
  CryptBoolean.IsKWeaklyNormal f k

Every `k`-normal Boolean function is `k`-weakly normal.

theoremdefined in CryptBoolean/Carlet/Chapter05/Normality.lean

complete

theorem CryptBoolean.IsKNormal.le_normality {n k : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (h : CryptBoolean.IsKNormal f k) : k ≤ CryptBoolean.normality f

theorem CryptBoolean.IsKNormal.le_normality
  {n k : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (h : CryptBoolean.IsKNormal f k) :
  k ≤ CryptBoolean.normality f

A `k`-normal flat witnesses that `k` is bounded by Carlet's normality parameter.

theoremdefined in CryptBoolean/Carlet/Chapter05/Normality.lean

complete

theorem CryptBoolean.IsKWeaklyNormal.le_weakNormality {n k : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (h : CryptBoolean.IsKWeaklyNormal f k) :
  k ≤ CryptBoolean.weakNormality f

theorem CryptBoolean.IsKWeaklyNormal.le_weakNormality
  {n k : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (h : CryptBoolean.IsKWeaklyNormal f k) :
  k ≤ CryptBoolean.weakNormality f

A `k`-weakly-normal flat witnesses that `k` is bounded by weak normality.

Theorem4.4.4

Group: Chapter 4: Classes with Provable Spectra and Weights (30)

Group member previews

Preview

Theorem 4.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 3.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagscarletchapter-5normalityrandom-functionsasymptoticreference-65page-72fidelity-exact

Random nonnormality (Carlet, p. 72). For every real \alpha>1, as n\to\infty the uniform probability that an n-variable Boolean function is not \lfloor\alpha\log_2 n\rfloor-normal tends to one.

Lean code for Theorem4.4.4●12 declarations

defdefined in CryptBoolean/Carlet/Chapter05/RandomNonnormality.lean

complete

def CryptBoolean.weakNormalityProbability (n k : ℕ) : ℝ

def CryptBoolean.weakNormalityProbability
  (n k : ℕ) : ℝ

The exact uniform probability that an `n`-variable Boolean function is
`k`-weakly normal.

theoremdefined in CryptBoolean/Carlet/Chapter05/RandomNonnormality.lean

complete

theorem CryptBoolean.weakNormalityProbability_le_of_le {n k : ℕ} (hk : k ≤ n) :
  CryptBoolean.weakNormalityProbability n k ≤
    2 ^ (n * k + 2 * n + 1) / 2 ^ 2 ^ k

theorem CryptBoolean.weakNormalityProbability_le_of_le
  {n k : ℕ} (hk : k ≤ n) :
  CryptBoolean.weakNormalityProbability n
      k ≤
    2 ^ (n * k + 2 * n + 1) / 2 ^ 2 ^ k

A finite union bound for weak normality.

theoremdefined in CryptBoolean/Carlet/Chapter05/RandomNonnormality.lean

complete

theorem CryptBoolean.weakNormalityProbability_le (n k : ℕ) :
  CryptBoolean.weakNormalityProbability n k ≤
    2 ^ (n * k + 2 * n + 1) / 2 ^ 2 ^ k

theorem CryptBoolean.weakNormalityProbability_le
  (n k : ℕ) :
  CryptBoolean.weakNormalityProbability n
      k ≤
    2 ^ (n * k + 2 * n + 1) / 2 ^ 2 ^ k

The finite weak-normality union bound is total in `k`; dimensions larger
than the ambient dimension have probability zero.

defdefined in CryptBoolean/Carlet/Chapter05/RandomNonnormality.lean

complete

def CryptBoolean.normalityProbability (n k : ℕ) : ℝ

def CryptBoolean.normalityProbability
  (n k : ℕ) : ℝ

The exact uniform probability that an `n`-variable Boolean function is
`k`-normal.

theoremdefined in CryptBoolean/Carlet/Chapter05/RandomNonnormality.lean

complete

theorem CryptBoolean.normalityProbability_le_weakNormalityProbability
  (n k : ℕ) :
  CryptBoolean.normalityProbability n k ≤
    CryptBoolean.weakNormalityProbability n k

theorem CryptBoolean.normalityProbability_le_weakNormalityProbability
  (n k : ℕ) :
  CryptBoolean.normalityProbability n k ≤
    CryptBoolean.weakNormalityProbability
      n k

Normality is no more likely than weak normality.

theoremdefined in CryptBoolean/Carlet/Chapter05/RandomNonnormality.lean

complete

theorem CryptBoolean.tendsto_weakNormalityProbability_zero_of_ratio (k : ℕ → ℕ)
  (hk : ∀ᶠ (n : ℕ) in Filter.atTop, 2 < k n)
  (hratio :
    Filter.Tendsto (fun n => 2 ^ k n / (↑n * ↑(k n))) Filter.atTop
      Filter.atTop) :
  Filter.Tendsto
    (fun n => CryptBoolean.weakNormalityProbability n (k n))
    Filter.atTop (nhds 0)

theorem CryptBoolean.tendsto_weakNormalityProbability_zero_of_ratio
  (k : ℕ → ℕ)
  (hk :
    ∀ᶠ (n : ℕ) in Filter.atTop, 2 < k n)
  (hratio :
    Filter.Tendsto
      (fun n => 2 ^ k n / (↑n * ↑(k n)))
      Filter.atTop Filter.atTop) :
  Filter.Tendsto
    (fun n =>
      CryptBoolean.weakNormalityProbability
        n (k n))
    Filter.atTop (nhds 0)

The cited general asymptotic theorem: if `k n > 2` eventually and
`2^(k n) / (n * k n)` diverges, then a uniformly random Boolean function is
`k n`-weakly normal with probability tending to zero.

defdefined in CryptBoolean/Carlet/Chapter05/RandomNonnormality.lean

complete

def CryptBoolean.nonWeakNormalityProbability (n k : ℕ) : ℝ

def CryptBoolean.nonWeakNormalityProbability
  (n k : ℕ) : ℝ

The probability that a uniformly random Boolean function is not
`k`-weakly normal.

theoremdefined in CryptBoolean/Carlet/Chapter05/RandomNonnormality.lean

complete

theorem CryptBoolean.tendsto_nonWeakNormalityProbability_one_of_ratio
  (k : ℕ → ℕ) (hk : ∀ᶠ (n : ℕ) in Filter.atTop, 2 < k n)
  (hratio :
    Filter.Tendsto (fun n => 2 ^ k n / (↑n * ↑(k n))) Filter.atTop
      Filter.atTop) :
  Filter.Tendsto
    (fun n => CryptBoolean.nonWeakNormalityProbability n (k n))
    Filter.atTop (nhds 1)

theorem CryptBoolean.tendsto_nonWeakNormalityProbability_one_of_ratio
  (k : ℕ → ℕ)
  (hk :
    ∀ᶠ (n : ℕ) in Filter.atTop, 2 < k n)
  (hratio :
    Filter.Tendsto
      (fun n => 2 ^ k n / (↑n * ↑(k n)))
      Filter.atTop Filter.atTop) :
  Filter.Tendsto
    (fun n =>
      CryptBoolean.nonWeakNormalityProbability
        n (k n))
    Filter.atTop (nhds 1)

Under the cited ratio hypothesis, random functions are almost surely not
weakly normal at the prescribed dimensions.

defdefined in CryptBoolean/Carlet/Chapter05/RandomNonnormality.lean

complete

def CryptBoolean.nonnormalityProbability (n k : ℕ) : ℝ

def CryptBoolean.nonnormalityProbability
  (n k : ℕ) : ℝ

The probability that a uniformly random Boolean function is not
`k`-normal.

theoremdefined in CryptBoolean/Carlet/Chapter05/RandomNonnormality.lean

complete

theorem CryptBoolean.tendsto_nonnormalityProbability_one_of_ratio (k : ℕ → ℕ)
  (hk : ∀ᶠ (n : ℕ) in Filter.atTop, 2 < k n)
  (hratio :
    Filter.Tendsto (fun n => 2 ^ k n / (↑n * ↑(k n))) Filter.atTop
      Filter.atTop) :
  Filter.Tendsto (fun n => CryptBoolean.nonnormalityProbability n (k n))
    Filter.atTop (nhds 1)

theorem CryptBoolean.tendsto_nonnormalityProbability_one_of_ratio
  (k : ℕ → ℕ)
  (hk :
    ∀ᶠ (n : ℕ) in Filter.atTop, 2 < k n)
  (hratio :
    Filter.Tendsto
      (fun n => 2 ^ k n / (↑n * ↑(k n)))
      Filter.atTop Filter.atTop) :
  Filter.Tendsto
    (fun n =>
      CryptBoolean.nonnormalityProbability
        n (k n))
    Filter.atTop (nhds 1)

Under the cited ratio hypothesis, random functions are almost surely not
normal at the prescribed dimensions.

defdefined in CryptBoolean/Carlet/Chapter05/RandomNonnormality.lean

complete

def CryptBoolean.carletNonnormalityDimension (α : ℝ) (n : ℕ) : ℕ

def CryptBoolean.carletNonnormalityDimension
  (α : ℝ) (n : ℕ) : ℕ

Carlet's logarithmic dimension `floor (α log₂ n)`.

theoremdefined in CryptBoolean/Carlet/Chapter05/RandomNonnormality.lean

complete

theorem CryptBoolean.tendsto_carletNonnormalityProbability {α : ℝ}
  (hα : 1 < α) :
  Filter.Tendsto
    (fun n =>
      CryptBoolean.nonnormalityProbability n
        (CryptBoolean.carletNonnormalityDimension α n))
    Filter.atTop (nhds 1)

theorem CryptBoolean.tendsto_carletNonnormalityProbability
  {α : ℝ} (hα : 1 < α) :
  Filter.Tendsto
    (fun n =>
      CryptBoolean.nonnormalityProbability
        n
        (CryptBoolean.carletNonnormalityDimension
          α n))
    Filter.atTop (nhds 1)

Carlet's random-nonnormality corollary: for every `α > 1`, the uniform
probability that an `n`-variable Boolean function is not
`floor (α log₂ n)`-normal tends to one.

The proof first establishes the general criterion 2^{k_n}/(nk_n)\to\infty, then verifies it for the displayed floored logarithmic dimension.