1.10. Derivatives and autocorrelation
Definition1.10.1
uses 1
✓L∃∀N
Associated Lean declarations
-
FABL.booleanDerivative[complete] -
CryptBoolean.realSignView_booleanDerivative[complete]
Definition 2 (Carlet, p. 27). Let f:V_n\to\mathbb F_2 and b\in V_n.
The derivative of f in direction b is the Boolean function
D_bf(x)=f(x)+f(x+b)
\qquad(x\in V_n),
where addition is in \mathbb F_2. Its sign function satisfies
(D_bf)_\chi(x)=f_\chi(x)f_\chi(x+b).
Lean code for Definition1.10.1●2 declarations
Associated Lean declarations
-
FABL.booleanDerivative[complete]
-
CryptBoolean.realSignView_booleanDerivative[complete]
Associated Lean declarations
-
FABL.booleanDerivative[complete] -
CryptBoolean.realSignView_booleanDerivative[complete]
-
defdefined in FABL/Chapter06/FoolingF₂Polynomials/DirectionalDerivatives.leancomplete
def FABL.booleanDerivative {n : ℕ} (f : FABL.F₂BooleanFunction n) (y : FABL.F₂Cube n) : FABL.F₂BooleanFunction n
def FABL.booleanDerivative {n : ℕ} (f : FABL.F₂BooleanFunction n) (y : FABL.F₂Cube n) : FABL.F₂BooleanFunction n
The binary directional derivative in direction `y`.
-
theoremdefined in CryptBoolean/Carlet/Chapter02/Derivatives.leancomplete
theorem CryptBoolean.realSignView_booleanDerivative {n : ℕ} (f : CryptBoolean.BooleanFunction n) (b x : FABL.F₂Cube n) : CryptBoolean.realSignView (FABL.booleanDerivative f b) x = CryptBoolean.realSignView f x * CryptBoolean.realSignView f (x + b)
theorem CryptBoolean.realSignView_booleanDerivative {n : ℕ} (f : CryptBoolean.BooleanFunction n) (b x : FABL.F₂Cube n) : CryptBoolean.realSignView (FABL.booleanDerivative f b) x = CryptBoolean.realSignView f x * CryptBoolean.realSignView f (x + b)
The derivative sign is the product of the two translated function signs.
Definition1.10.2
✓L∃∀N
Associated Lean declarations
Autocorrelation (Carlet, Relations (24)--(25), p. 27). For
f:V_n\to\mathbb F_2, define
\Delta_f(b)
=\sum_{x\in V_n}(-1)^{D_bf(x)}
=\sum_{x\in V_n}f_\chi(x)f_\chi(x+b)
=(f_\chi\otimes f_\chi)(b).
Lean code for Definition1.10.2●2 declarations
Associated Lean declarations
Associated Lean declarations
-
defdefined in CryptBoolean/Carlet/Chapter02/Derivatives.leancomplete
def CryptBoolean.autocorrelation {n : ℕ} (f : CryptBoolean.BooleanFunction n) (b : FABL.F₂Cube n) : ℝ
def CryptBoolean.autocorrelation {n : ℕ} (f : CryptBoolean.BooleanFunction n) (b : FABL.F₂Cube n) : ℝ
Carlet's autocorrelation value `Δ_f(b) = ∑ₓ (-1)^(D_b f(x))`.
-
theoremdefined in CryptBoolean/Carlet/Chapter02/Derivatives.leancomplete
theorem CryptBoolean.autocorrelation_eq_rawConvolution_realSignView {n : ℕ} (f : CryptBoolean.BooleanFunction n) (b : FABL.F₂Cube n) : CryptBoolean.autocorrelation f b = CryptBoolean.rawConvolution (CryptBoolean.realSignView f) (CryptBoolean.realSignView f) b
theorem CryptBoolean.autocorrelation_eq_rawConvolution_realSignView {n : ℕ} (f : CryptBoolean.BooleanFunction n) (b : FABL.F₂Cube n) : CryptBoolean.autocorrelation f b = CryptBoolean.rawConvolution (CryptBoolean.realSignView f) (CryptBoolean.realSignView f) b
Autocorrelation is the raw self-convolution of the sign view.
Theorem1.10.3
✓L∃∀N
Associated Lean declarations
Wiener--Khinchin identity (Carlet, Relation (25), p. 27). For every
f:V_n\to\mathbb F_2 and u\in V_n,
\widehat{\Delta_f}(u)
=\sum_{b\in V_n}\Delta_f(b)(-1)^{u\mathbin\cdot b}
=W_f(u)^2.
Lean code for Theorem1.10.3●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter02/Derivatives.leancomplete
theorem CryptBoolean.rawFourierTransform_autocorrelation {n : ℕ} (f : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n) : CryptBoolean.rawFourierTransform (CryptBoolean.autocorrelation f) a = ↑(CryptBoolean.walshTransform f a) ^ 2
theorem CryptBoolean.rawFourierTransform_autocorrelation {n : ℕ} (f : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n) : CryptBoolean.rawFourierTransform (CryptBoolean.autocorrelation f) a = ↑(CryptBoolean.walshTransform f a) ^ 2
Wiener--Khintchine: the raw transform of autocorrelation is the squared Walsh spectrum.
Corollary1.10.4
Relation (26) (Carlet, p. 28). For every f:V_n\to\mathbb F_2,
\sum_{b\in V_n}\Delta_f(b)=W_f(0)^2.
Lean code for Corollary1.10.4●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter02/Derivatives.leancomplete
theorem CryptBoolean.sum_autocorrelation_eq_walshTransform_zero_sq {n : ℕ} (f : CryptBoolean.BooleanFunction n) : ∑ b, CryptBoolean.autocorrelation f b = ↑(CryptBoolean.walshTransform f 0) ^ 2
theorem CryptBoolean.sum_autocorrelation_eq_walshTransform_zero_sq {n : ℕ} (f : CryptBoolean.BooleanFunction n) : ∑ b, CryptBoolean.autocorrelation f b = ↑(CryptBoolean.walshTransform f 0) ^ 2
The total autocorrelation is the square of the zero-frequency Walsh value.
Proposition1.10.5
Proposition 9 (Carlet, Relation (28), p. 28). Let E,E' be complementary
subspaces of V_n. For every Boolean function f:V_n\to\mathbb F_2,
\sum_{u\in E^\perp}W_f(u)^2
=|E^\perp|\sum_{a\in E'}
\left(\sum_{x\in a+E}(-1)^{f(x)}\right)^2.
Lean code for Proposition1.10.5●3 declarations
Associated Lean declarations
Associated Lean declarations
-
defdefined in CryptBoolean/Carlet/Chapter02/RestrictionSquareIdentity.leancomplete
def CryptBoolean.affineSubspaceRestrictionImbalance {n : ℕ} (f : CryptBoolean.BooleanFunction n) (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n) : ℝ
def CryptBoolean.affineSubspaceRestrictionImbalance {n : ℕ} (f : CryptBoolean.BooleanFunction n) (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n) : ℝ
The unnormalized sign imbalance of the restriction of `f` to `a + E`.
-
theoremdefined in CryptBoolean/Carlet/Chapter02/RestrictionSquareIdentity.leancomplete
theorem CryptBoolean.sum_autocorrelation_submodule_eq_sum_affineSubspaceRestrictionImbalance_sq {n : ℕ} (f : CryptBoolean.BooleanFunction n) (E E' : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (hcompl : IsCompl E E') : ∑ e, CryptBoolean.autocorrelation f ↑e = ∑ a, CryptBoolean.affineSubspaceRestrictionImbalance f E ↑a ^ 2
theorem CryptBoolean.sum_autocorrelation_submodule_eq_sum_affineSubspaceRestrictionImbalance_sq {n : ℕ} (f : CryptBoolean.BooleanFunction n) (E E' : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (hcompl : IsCompl E E') : ∑ e, CryptBoolean.autocorrelation f ↑e = ∑ a, CryptBoolean.affineSubspaceRestrictionImbalance f E ↑a ^ 2
Summing ambient autocorrelation over `E` separates into the squared imbalances of the restrictions on the cosets indexed by a complement `E'`.
-
theoremdefined in CryptBoolean/Carlet/Chapter02/RestrictionSquareIdentity.leancomplete
theorem CryptBoolean.sum_walshTransform_sq_perpendicular_eq_card_mul_sum_restrictionImbalance_sq {n : ℕ} (f : CryptBoolean.BooleanFunction n) (E E' : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (hcompl : IsCompl E E') : ∑ u, ↑(CryptBoolean.walshTransform f ↑u) ^ 2 = ↑(Nat.card ↥(FABL.perpendicularSubspace E)) * ∑ a, CryptBoolean.affineSubspaceRestrictionImbalance f E ↑a ^ 2
theorem CryptBoolean.sum_walshTransform_sq_perpendicular_eq_card_mul_sum_restrictionImbalance_sq {n : ℕ} (f : CryptBoolean.BooleanFunction n) (E E' : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (hcompl : IsCompl E E') : ∑ u, ↑(CryptBoolean.walshTransform f ↑u) ^ 2 = ↑(Nat.card ↥(FABL.perpendicularSubspace E)) * ∑ a, CryptBoolean.affineSubspaceRestrictionImbalance f E ↑a ^ 2
Carlet Proposition 9, Relation (28): the Walsh square mass on `E`'s perpendicular is the perpendicular cardinality times the second moment of the imbalances of the restrictions to the cosets indexed by a complement `E'`.