6.2. Correlation and propagation criteria
Theorem6.2.1
Maximum correlation on a coordinate set (Carlet, p. 115). Let
f:V_n\to\mathbb F_2 be m-resilient and let I\subseteq[n].
Among the Walsh frequencies supported in I, at most
\sum_{j=m+1}^{|I|}\binom{|I|}{j}
have nonzero coefficients. If |I|=m+1 and u_I is the unique
frequency with support I, then the maximum correlation of f with
functions depending only on I is
2^{-n}|W_f(u_I)|.
Lean code for Theorem6.2.1●3 theorems
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter07/MaximumCorrelation.leancomplete
theorem CryptBoolean.card_highWeightFrequenciesSupportedIn_eq_sum_choose {n : ℕ} (I : Finset (Fin n)) (m : ℕ) : {u | FABL.f₂Support u ⊆ I ∧ m < (FABL.f₂Support u).card}.card = ∑ j ∈ Finset.Icc (m + 1) I.card, I.card.choose j
theorem CryptBoolean.card_highWeightFrequenciesSupportedIn_eq_sum_choose {n : ℕ} (I : Finset (Fin n)) (m : ℕ) : {u | FABL.f₂Support u ⊆ I ∧ m < (FABL.f₂Support u).card}.card = ∑ j ∈ Finset.Icc (m + 1) I.card, I.card.choose j
The number of frequencies supported in `I` whose weight exceeds `m`.
-
theoremdefined in CryptBoolean/Carlet/Chapter07/MaximumCorrelation.leancomplete
theorem CryptBoolean.card_walshSupport_filter_subset_le_sum_choose_of_isResilient {n : ℕ} (f : CryptBoolean.BooleanFunction n) (I : Finset (Fin n)) (m : ℕ) (hm : m < n) (hf : CryptBoolean.IsResilient m f) : {u ∈ CryptBoolean.walshSupport f | FABL.f₂Support u ⊆ I}.card ≤ ∑ j ∈ Finset.Icc (m + 1) I.card, I.card.choose j
theorem CryptBoolean.card_walshSupport_filter_subset_le_sum_choose_of_isResilient {n : ℕ} (f : CryptBoolean.BooleanFunction n) (I : Finset (Fin n)) (m : ℕ) (hm : m < n) (hf : CryptBoolean.IsResilient m f) : {u ∈ CryptBoolean.walshSupport f | FABL.f₂Support u ⊆ I}.card ≤ ∑ j ∈ Finset.Icc (m + 1) I.card, I.card.choose j
An `m`-resilient function has at most the high-weight binomial tail of nonzero Walsh frequencies supported inside a prescribed coordinate set.
-
theoremdefined in CryptBoolean/Carlet/Chapter07/MaximumCorrelation.leancomplete
theorem CryptBoolean.maximumCorrelation_eq_abs_walshTransform_f₂CubeOfFinset_div_of_isResilient {n : ℕ} (f : CryptBoolean.BooleanFunction n) (I : Finset (Fin n)) (m : ℕ) (hm : m < n) (hI : I.card = m + 1) (hf : CryptBoolean.IsResilient m f) : CryptBoolean.maximumCorrelation f I = |↑(CryptBoolean.walshTransform f (FABL.f₂CubeOfFinset I))| / 2 ^ n
theorem CryptBoolean.maximumCorrelation_eq_abs_walshTransform_f₂CubeOfFinset_div_of_isResilient {n : ℕ} (f : CryptBoolean.BooleanFunction n) (I : Finset (Fin n)) (m : ℕ) (hm : m < n) (hI : I.card = m + 1) (hf : CryptBoolean.IsResilient m f) : CryptBoolean.maximumCorrelation f I = |↑(CryptBoolean.walshTransform f (FABL.f₂CubeOfFinset I))| / 2 ^ n
For an `m`-resilient function and `|I| = m+1`, maximum correlation with functions on `I` is the normalized magnitude of the unique possible Walsh coefficient supported on all of `I`.
Theorem6.2.2
Resiliency--propagation tradeoff (Carlet, p. 116). If an n-variable
Boolean function is m-resilient and satisfies \mathrm{PC}(\ell), then
m+\ell\le n-1.
Lean code for Theorem6.2.2●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter07/PropagationTradeoff.leancomplete
theorem CryptBoolean.resilient_propagationCriterion_parameter_tradeoff {n : ℕ} (f : CryptBoolean.BooleanFunction n) (m l : ℕ) (hm : m < n) (hresilient : CryptBoolean.IsResilient m f) (hpc : CryptBoolean.SatisfiesPropagationCriterion l f) : m + l ≤ n - 1
theorem CryptBoolean.resilient_propagationCriterion_parameter_tradeoff {n : ℕ} (f : CryptBoolean.BooleanFunction n) (m l : ℕ) (hm : m < n) (hresilient : CryptBoolean.IsResilient m f) (hpc : CryptBoolean.SatisfiesPropagationCriterion l f) : m + l ≤ n - 1
An `m`-resilient `PC(l)` Boolean function satisfies `m+l ≤ n-1`.
Theorem6.2.3
Equality in the resiliency--propagation tradeoff (Carlet, p. 116). Let
\ell>0. If an n-variable m-resilient Boolean function satisfies
\mathrm{PC}(\ell) and
m+\ell=n-1,
then n is odd, \ell=n-1, and m=0.
Lean code for Theorem6.2.3●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter07/PropagationEquality.leancomplete
theorem CryptBoolean.resilient_propagationCriterion_equality_classification {n : ℕ} (f : CryptBoolean.BooleanFunction n) (m l : ℕ) (hl : 0 < l) (hresilient : CryptBoolean.IsResilient m f) (hpc : CryptBoolean.SatisfiesPropagationCriterion l f) (hequality : m + l = n - 1) : Odd n ∧ l = n - 1 ∧ m = 0
theorem CryptBoolean.resilient_propagationCriterion_equality_classification {n : ℕ} (f : CryptBoolean.BooleanFunction n) (m l : ℕ) (hl : 0 < l) (hresilient : CryptBoolean.IsResilient m f) (hpc : CryptBoolean.SatisfiesPropagationCriterion l f) (hequality : m + l = n - 1) : Odd n ∧ l = n - 1 ∧ m = 0
Equality in the resiliency--propagation tradeoff at positive propagation order is possible only in odd dimension, with balancedness and `PC(n-1)`.