theorem CryptBoolean.booleanFunctionF₂Encoding_signCubeView
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  FABL.booleanFunctionF₂Encoding
      (CryptBoolean.signCubeView f) =
    f

theorem CryptBoolean.functionAlgebraicDegree_le_sub_sub_one_of_isResilient
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ)
  (hf : CryptBoolean.IsResilient m f)
  (hm : m < n - 1) :
  FABL.functionAlgebraicDegree f ≤
    n - m - 1

theorem CryptBoolean.functionAlgebraicDegree_le_sub_of_isCorrelationImmune
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ)
  (hf :
    CryptBoolean.IsCorrelationImmune m f)
  (hm : m < n) :
  FABL.functionAlgebraicDegree f ≤ n - m

theorem CryptBoolean.functionAlgebraicDegree_le_one_of_isResilient_natPred
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n)
  (hf :
    CryptBoolean.IsResilient (n - 1) f) :
  FABL.functionAlgebraicDegree f ≤ 1

theorem CryptBoolean.exists_affineFunction_of_isResilient_natPred
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n)
  (hf :
    CryptBoolean.IsResilient (n - 1) f) :
  ∃ b a, f = FABL.affineFunction b a

theorem CryptBoolean.functionAlgebraicDegree_le_sub_sub_one_of_isCorrelationImmune_of_weight
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m < n)
  (hf :
    CryptBoolean.IsCorrelationImmune m f)
  (hweight :
    2 ^ (m + 1) ∣
      CryptBoolean.hammingWeight f) :
  FABL.functionAlgebraicDegree f ≤
    n - m - 1

theorem CryptBoolean.functionNumericalDegree_booleanRealEmbedding_eq_fourierDegree_signCubeView
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  FABL.functionNumericalDegree
      (FABL.booleanRealEmbedding f) =
    FABL.fourierDegree
      (CryptBoolean.signCubeView f).toReal

theorem CryptBoolean.functionNumericalDegree_booleanRealEmbedding_le_iff_walshTransform
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D : ℕ) :
  FABL.functionNumericalDegree
        (FABL.booleanRealEmbedding f) ≤
      D ↔
    ∀ (S : Finset (Fin n)),
      D < S.card →
        CryptBoolean.walshTransform f
            (FABL.f₂CubeOfFinset S) =
          0

theorem CryptBoolean.proposition_32_resilient_iff_functionNumericalDegree_le
  {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n) (hm : m < n) :
  CryptBoolean.IsResilient m f ↔
    FABL.functionNumericalDegree
        (FABL.booleanRealEmbedding
          (f +
            ⇑(FABL.coordinateSum
                Finset.univ))) ≤
      n - m - 1

theorem CryptBoolean.bitSignInt_cast_eq_realSignView
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  ↑(CryptBoolean.bitSignInt (f x)) =
    CryptBoolean.realSignView f x

theorem CryptBoolean.sum_walshTransform_submodule_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  ∑ u, CryptBoolean.walshTransform f ↑u =
    ↑(Nat.card ↥E) *
      ∑ x, CryptBoolean.bitSignInt (f ↑x)

theorem CryptBoolean.two_pow_m_add_two_dvd_walshTransform_of_isResilient
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hf : CryptBoolean.IsResilient m f)
  (a : FABL.F₂Cube n) :
  2 ^ (m + 2) ∣
    CryptBoolean.walshTransform f a

theorem CryptBoolean.two_pow_m_add_one_dvd_walshTransform_of_isCorrelationImmune
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hf :
    CryptBoolean.IsCorrelationImmune m f)
  (a : FABL.F₂Cube n) :
  2 ^ (m + 1) ∣
    CryptBoolean.walshTransform f a

theorem CryptBoolean.two_pow_m_dvd_hammingWeight_of_isCorrelationImmune
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hf :
    CryptBoolean.IsCorrelationImmune m
      f) :
  2 ^ m ∣ CryptBoolean.hammingWeight f

theorem CryptBoolean.two_pow_m_add_two_dvd_walshTransform_of_isCorrelationImmune_of_weight
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hf :
    CryptBoolean.IsCorrelationImmune m f)
  (hweight :
    2 ^ (m + 1) ∣
      CryptBoolean.hammingWeight f)
  (a : FABL.F₂Cube n) :
  2 ^ (m + 2) ∣
    CryptBoolean.walshTransform f a

theorem CryptBoolean.two_mul_nonlinearity_add_two_pow_m_add_two_le_of_isResilient
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hf : CryptBoolean.IsResilient m f) :
  2 * CryptBoolean.nonlinearity f +
      2 ^ (m + 2) ≤
    2 ^ n

theorem CryptBoolean.nonlinearity_add_two_pow_m_add_one_le_two_pow_sub_one_of_isResilient
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hf : CryptBoolean.IsResilient m f) :
  CryptBoolean.nonlinearity f +
      2 ^ (m + 1) ≤
    2 ^ (n - 1)

theorem CryptBoolean.nonlinearity_le_two_pow_sub_two_pow_of_isResilient
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hf : CryptBoolean.IsResilient m f) :
  CryptBoolean.nonlinearity f ≤
    2 ^ (n - 1) - 2 ^ (m + 1)

theorem CryptBoolean.nonlinearity_eq_sarkarMaitra_bound_iff_hasPlateauedWalshAmplitude
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hf : CryptBoolean.IsResilient m f) :
  CryptBoolean.nonlinearity f =
      2 ^ (n - 1) - 2 ^ (m + 1) ↔
    CryptBoolean.HasPlateauedWalshAmplitude
      f (2 ^ (m + 2))

theorem CryptBoolean.walshTransform_eq_zero_or_eq_neg_two_pow_or_eq_two_pow_of_sarkarMaitra_equality
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hf : CryptBoolean.IsResilient m f)
  (hnonlinearity :
    CryptBoolean.nonlinearity f =
      2 ^ (n - 1) - 2 ^ (m + 1))
  (a : FABL.F₂Cube n) :
  CryptBoolean.walshTransform f a = 0 ∨
    CryptBoolean.walshTransform f a =
        -2 ^ (m + 2) ∨
      CryptBoolean.walshTransform f a =
        2 ^ (m + 2)

theorem CryptBoolean.isPlateaued_of_sarkarMaitra_equality
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hf : CryptBoolean.IsResilient m f)
  (hnonlinearity :
    CryptBoolean.nonlinearity f =
      2 ^ (n - 1) - 2 ^ (m + 1)) :
  CryptBoolean.IsPlateaued f

theorem CryptBoolean.two_pow_m_add_two_add_degree_quotient_dvd_walshTransform_of_isResilient
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hd :
    0 < FABL.functionAlgebraicDegree f)
  (hf : CryptBoolean.IsResilient m f)
  (a : FABL.F₂Cube n) :
  2 ^
      (m + 2 +
        (n - m - 2) /
          FABL.functionAlgebraicDegree
            f) ∣
    CryptBoolean.walshTransform f a

theorem CryptBoolean.two_pow_m_add_one_add_degree_quotient_dvd_nonlinearity_of_isResilient
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hd :
    0 < FABL.functionAlgebraicDegree f)
  (hf : CryptBoolean.IsResilient m f) :
  2 ^
      (m + 1 +
        (n - m - 2) /
          FABL.functionAlgebraicDegree
            f) ∣
    CryptBoolean.nonlinearity f

theorem CryptBoolean.two_pow_m_add_one_add_degree_quotient_dvd_walshTransform_of_isCorrelationImmune
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 1 ≤ n)
  (hd :
    0 < FABL.functionAlgebraicDegree f)
  (hf :
    CryptBoolean.IsCorrelationImmune m f)
  (a : FABL.F₂Cube n) :
  2 ^
      (m + 1 +
        (n - m - 1) /
          FABL.functionAlgebraicDegree
            f) ∣
    CryptBoolean.walshTransform f a

theorem CryptBoolean.two_pow_m_add_two_add_degree_quotient_dvd_walshTransform_of_isCorrelationImmune_of_weight
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hd :
    0 < FABL.functionAlgebraicDegree f)
  (hf :
    CryptBoolean.IsCorrelationImmune m f)
  (hweight :
    2 ^
        (m + 1 +
          (n - m - 2) /
            FABL.functionAlgebraicDegree
              f) ∣
      CryptBoolean.hammingWeight f)
  (a : FABL.F₂Cube n) :
  2 ^
      (m + 2 +
        (n - m - 2) /
          FABL.functionAlgebraicDegree
            f) ∣
    CryptBoolean.walshTransform f a

theorem CryptBoolean.nonlinearity_le_two_pow_sub_two_pow_degree_quotient_of_isResilient
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hd :
    0 < FABL.functionAlgebraicDegree f)
  (hf : CryptBoolean.IsResilient m f) :
  CryptBoolean.nonlinearity f ≤
    2 ^ (n - 1) -
      2 ^
        (m + 1 +
          (n - m - 2) /
            FABL.functionAlgebraicDegree
              f)

theorem CryptBoolean.functionAlgebraicDegree_eq_sub_sub_one_of_sarkarMaitra_equality
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hd :
    0 < FABL.functionAlgebraicDegree f)
  (hf : CryptBoolean.IsResilient m f)
  (hnonlinearity :
    CryptBoolean.nonlinearity f =
      2 ^ (n - 1) - 2 ^ (m + 1)) :
  FABL.functionAlgebraicDegree f =
    n - m - 1

theorem CryptBoolean.nonlinearity_le_even_dimension_resilient_bound
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hn : 0 < n) (heven : Even n)
  (hm : m ≤ n / 2 - 2)
  (hf : CryptBoolean.IsResilient m f) :
  CryptBoolean.nonlinearity f ≤
    2 ^ (n - 1) - 2 ^ (n / 2 - 1) -
      2 ^ (m + 1)

theorem CryptBoolean.nonlinearity_le_parseval_resilient_bound
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hf : CryptBoolean.IsResilient m f) :
  CryptBoolean.nonlinearity f ≤
    2 ^ (n - 1) -
      2 ^ (m + 1) *
        ⌈2 ^ (n - m - 2) /
            √↑(2 ^ n -
                  ∑
                    i ∈
                      Finset.range
                        (m + 1),
                    n.choose i)⌉₊

theorem CryptBoolean.entropyPower_div_sqrt_le_choose
  (m n : ℕ) (hm : 1 ≤ m)
  (hmhalf : m ≤ n / 2) :
  2 ^
        (↑n *
          CryptBoolean.binaryEntropyBaseTwo
            (↑m / ↑n)) /
      √(8 * ↑m * (1 - ↑m / ↑n)) ≤
    ↑(n.choose m)

theorem CryptBoolean.nonlinearity_le_entropy_resilient_bound
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : 1 ≤ m)
  (hmhalf : m ≤ n / 2)
  (hf : CryptBoolean.IsResilient m f) :
  CryptBoolean.nonlinearity f ≤
    2 ^ (n - 1) -
      2 ^ (m + 1) *
        ⌈2 ^ (↑n - ↑m - 2) /
            √(2 ^ n -
                2 ^
                    (↑n *
                      CryptBoolean.binaryEntropyBaseTwo
                        (↑m / ↑n)) /
                  √(8 * ↑m *
                      (1 - ↑m / ↑n)))⌉₊