theorem CryptBoolean.nonlinearity_eq_higherOrderNonlinearity_one
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.nonlinearity f =
    CryptBoolean.higherOrderNonlinearity 1
      f

theorem CryptBoolean.higherOrderNonlinearity_le_hammingDistance
  {n : ℕ} (r : ℕ)
  (f g : CryptBoolean.BooleanFunction n)
  (hg : g ∈ CryptBoolean.reedMuller r n) :
  CryptBoolean.higherOrderNonlinearity r
      f ≤
    CryptBoolean.hammingDistance f g

theorem CryptBoolean.exists_reedMuller_hammingDistance_eq_higherOrderNonlinearity
  {n : ℕ} (r : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  ∃ g ∈ CryptBoolean.reedMuller r n,
    CryptBoolean.hammingDistance f g =
      CryptBoolean.higherOrderNonlinearity
        r f

theorem CryptBoolean.higherOrderNonlinearity_antitone
  {n r s : ℕ} (hrs : r ≤ s)
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.higherOrderNonlinearity s
      f ≤
    CryptBoolean.higherOrderNonlinearity r
      f

theorem CryptBoolean.anfCoeff_eq_zero_of_coordinate_invariant
  {n : ℕ}
  (g : CryptBoolean.BooleanFunction n)
  (S : Finset (Fin n)) (i : Fin n)
  (hiS : i ∈ S)
  (hinvariant :
    ∀ (x : FABL.F₂Cube n),
      g (Function.update x i 1) =
        g (Function.update x i 0)) :
  FABL.anfCoeff g S = 0

theorem CryptBoolean.anfCoeff_eq_zero_of_dependsOn_of_not_subset
  {n : ℕ}
  (g : CryptBoolean.BooleanFunction n)
  {I S : Finset (Fin n)}
  (hdepends : DependsOn g ↑I)
  (hS : ¬S ⊆ I) : FABL.anfCoeff g S = 0

theorem CryptBoolean.functionAlgebraicDegree_le_card_of_dependsOn
  {n : ℕ}
  (g : CryptBoolean.BooleanFunction n)
  (I : Finset (Fin n))
  (hdepends : DependsOn g ↑I) :
  FABL.functionAlgebraicDegree g ≤ I.card

theorem CryptBoolean.higherOrderNonlinearity_le_hammingDistance_of_dependsOn
  {n : ℕ} (r : ℕ)
  (f g : CryptBoolean.BooleanFunction n)
  (I : Finset (Fin n)) (hI : I.card = r)
  (hdepends : DependsOn g ↑I) :
  CryptBoolean.higherOrderNonlinearity r
      f ≤
    CryptBoolean.hammingDistance f g

theorem CryptBoolean.exists_higherOrderNonlinearity_gt_of_counting
  (r n t : ℕ)
  (hcount :
    (2 ^
          ∑ j ∈ Finset.range (r + 1),
            n.choose j) *
        CryptBoolean.hammingBallVolume
          (2 ^ n) t <
      2 ^ 2 ^ n) :
  ∃ f,
    t <
      CryptBoolean.higherOrderNonlinearity
        r f

theorem CryptBoolean.exists_higherOrderNonlinearity_gt_of_hammingBallVolume_lt
  (r n t : ℕ)
  (hdimension :
    ∑ j ∈ Finset.range (r + 1),
        n.choose j ≤
      2 ^ n)
  (hvolume :
    CryptBoolean.hammingBallVolume (2 ^ n)
        t <
      2 ^
        (2 ^ n -
          ∑ j ∈ Finset.range (r + 1),
            n.choose j)) :
  ∃ f,
    t <
      CryptBoolean.higherOrderNonlinearity
        r f

theorem CryptBoolean.exists_higherOrderNonlinearity_gt_lower_bound_of_dimension
  (r n : ℕ)
  (hdimension :
    2 *
        ∑ j ∈ Finset.range (r + 1),
          n.choose j ≤
      2 ^ n) :
  ∃ f,
    2 ^ n / 2 -
        √(2 ^ n / 2 *
            ↑(∑ j ∈ Finset.range (r + 1),
                n.choose j)) <
      ↑(CryptBoolean.higherOrderNonlinearity
          r f)

theorem CryptBoolean.eventually_twice_sum_choose_le_two_pow
  (r : ℕ) :
  ∀ᶠ (n : ℕ) in Filter.atTop,
    2 *
        ∑ j ∈ Finset.range (r + 1),
          n.choose j ≤
      2 ^ n

theorem CryptBoolean.eventually_exists_higherOrderNonlinearity_gt_carlet_lower_bound
  (r : ℕ) :
  ∀ᶠ (n : ℕ) in Filter.atTop,
    ∃ f,
      2 ^ (↑n - 1) -
          √(2 ^ (↑n - 1) *
              ↑(∑
                  j ∈
                    Finset.range (r + 1),
                  n.choose j)) <
        ↑(CryptBoolean.higherOrderNonlinearity
            r f)

theorem CryptBoolean.higherOrderNonlinearity_le_maximum
  {n : ℕ} (r : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.higherOrderNonlinearity r
      f ≤
    CryptBoolean.maximumHigherOrderNonlinearity
      r n

theorem CryptBoolean.exists_higherOrderNonlinearity_eq_maximum
  (r n : ℕ) :
  ∃ f,
    CryptBoolean.higherOrderNonlinearity r
        f =
      CryptBoolean.maximumHigherOrderNonlinearity
        r n

theorem CryptBoolean.maximumHigherOrderNonlinearity_succ_le
  (r n : ℕ) (hr : 1 ≤ r) :
  CryptBoolean.maximumHigherOrderNonlinearity
      r (n + 1) ≤
    CryptBoolean.maximumHigherOrderNonlinearity
        r n +
      CryptBoolean.maximumHigherOrderNonlinearity
        (r - 1) n

theorem CryptBoolean.maximumHigherOrderNonlinearity_self
  (n : ℕ) :
  CryptBoolean.maximumHigherOrderNonlinearity
      n n =
    0

theorem CryptBoolean.maximumHigherOrderNonlinearity_le_sum_Ico
  (r n : ℕ) (hr : 1 ≤ r) (hrn : r ≤ n) :
  CryptBoolean.maximumHigherOrderNonlinearity
      r n ≤
    ∑ j ∈ Finset.Ico r n,
      CryptBoolean.maximumHigherOrderNonlinearity
        (r - 1) j

theorem CryptBoolean.maximumHigherOrderNonlinearity_cast_le_sum_Ico_of_le
  (r n : ℕ) (hr : 1 ≤ r) (hrn : r ≤ n)
  (bound : ℕ → ℝ)
  (hbound :
    ∀ j ∈ Finset.Ico r n,
      ↑(CryptBoolean.maximumHigherOrderNonlinearity
            (r - 1) j) ≤
        bound j) :
  ↑(CryptBoolean.maximumHigherOrderNonlinearity
        r n) ≤
    ∑ j ∈ Finset.Ico r n, bound j

theorem CryptBoolean.maximumHigherOrderNonlinearity_cast_le_carlet_step
  (r n : ℕ) (hr : 1 ≤ r) (hrn : r ≤ n)
  (A : ℝ) (error : ℕ → ℝ)
  (hlower :
    ∀ j ∈ Finset.Ico r n,
      ↑(CryptBoolean.maximumHigherOrderNonlinearity
            (r - 1) j) ≤
        2 ^ j / 2 - A * √2 ^ j +
          error j) :
  ↑(CryptBoolean.maximumHigherOrderNonlinearity
        r n) ≤
    (2 ^ n - 2 ^ r) / 2 -
        A * (1 + √2) * (√2 ^ n - √2 ^ r) +
      ∑ j ∈ Finset.Ico r n, error j

theorem CryptBoolean.orderTwoCorrelation_eq_two_pow_sub_two_hammingDistance
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  CryptBoolean.orderTwoCorrelation f g =
    2 ^ n -
      2 *
        ↑(CryptBoolean.hammingDistance f
            g)

theorem CryptBoolean.maximumOrderTwoCorrelation_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.maximumOrderTwoCorrelation
      f =
    2 ^ n -
      2 *
        ↑(CryptBoolean.higherOrderNonlinearity
            2 f)

theorem CryptBoolean.orderTwoCorrelation_le_maximum
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (hg : g ∈ CryptBoolean.reedMuller 2 n) :
  CryptBoolean.orderTwoCorrelation f g ≤
    CryptBoolean.maximumOrderTwoCorrelation
      f

theorem CryptBoolean.exists_orderTwoCorrelation_eq_maximum
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∃ g ∈ CryptBoolean.reedMuller 2 n,
    CryptBoolean.orderTwoCorrelation f g =
      CryptBoolean.maximumOrderTwoCorrelation
        f

theorem CryptBoolean.maximumOrderTwoCorrelation_nonneg
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  0 ≤
    CryptBoolean.maximumOrderTwoCorrelation
      f

theorem CryptBoolean.abs_orderTwoCorrelation_le_maximum
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (hg : g ∈ CryptBoolean.reedMuller 2 n) :
  |CryptBoolean.orderTwoCorrelation f g| ≤
    CryptBoolean.maximumOrderTwoCorrelation
      f

theorem CryptBoolean.orderTwoCorrelationPowerSum_nonneg
  {n : ℕ} (k : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  0 ≤
    CryptBoolean.orderTwoCorrelationPowerSum
      k f

theorem CryptBoolean.orderTwoCorrelationPowerSum_pos
  {n : ℕ} (k : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  0 <
    CryptBoolean.orderTwoCorrelationPowerSum
      k f

theorem CryptBoolean.orderTwoCorrelationPowerSum_succ_le
  {n : ℕ} (k : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.orderTwoCorrelationPowerSum
      (k + 1) f ≤
    CryptBoolean.maximumOrderTwoCorrelation
          f ^
        2 *
      CryptBoolean.orderTwoCorrelationPowerSum
        k f

theorem CryptBoolean.sqrt_orderTwoCorrelationPowerSum_ratio_le
  {n : ℕ} (k : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  √(CryptBoolean.orderTwoCorrelationPowerSum
          (k + 1) f /
        CryptBoolean.orderTwoCorrelationPowerSum
          k f) ≤
    CryptBoolean.maximumOrderTwoCorrelation
      f

theorem CryptBoolean.maximumHigherOrderNonlinearity_two_cast_le_momentRatio
  (k n : ℕ) :
  ↑(CryptBoolean.maximumHigherOrderNonlinearity
        2 n) ≤
    2 ^ n / 2 -
      CryptBoolean.minimumOrderTwoMomentRatio
          k n /
        2

theorem CryptBoolean.booleanFunctionPairing_tuplePointParity
  {n m : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x : Fin m → FABL.F₂Cube n) :
  ((CryptBoolean.booleanFunctionPairing n)
        f)
      (CryptBoolean.tuplePointParity x) =
    ∑ i, f (x i)

theorem CryptBoolean.reedMullerTwoPairingCharacterSum_eq_card_of_mem_dual
  {n : ℕ}
  (h : CryptBoolean.BooleanFunction n)
  (hdual :
    h ∈ CryptBoolean.reedMullerDual 2 n) :
  CryptBoolean.reedMullerTwoPairingCharacterSum
      h =
    ↑(Nat.card
        ↥(CryptBoolean.reedMuller 2 n))

theorem CryptBoolean.reedMullerTwoPairingCharacterSum_eq_zero_of_not_mem_dual
  {n : ℕ}
  (h : CryptBoolean.BooleanFunction n)
  (hdual :
    h ∉ CryptBoolean.reedMullerDual 2 n) :
  CryptBoolean.reedMullerTwoPairingCharacterSum
      h =
    0

theorem CryptBoolean.orderTwoCorrelationPowerSum_eq_admissibleTupleCharacterSum
  {n : ℕ} (k : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (hn : 3 ≤ n) :
  CryptBoolean.orderTwoCorrelationPowerSum
      k f =
    ↑(Nat.card
          ↥(CryptBoolean.reedMuller 2
              n)) *
      ∑
        x ∈
          CryptBoolean.orderTwoAdmissibleTuples
            k n,
        FABL.binarySign
          (((CryptBoolean.booleanFunctionPairing
                n)
              f)
            (CryptBoolean.tuplePointParity
              x))

theorem CryptBoolean.tuplePointParityMultiplicity_comp_perm
  {n : ℕ} (k : ℕ)
  (h : CryptBoolean.BooleanFunction n)
  (σ : Equiv.Perm (FABL.F₂Cube n)) :
  CryptBoolean.tuplePointParityMultiplicity
      k h =
    CryptBoolean.tuplePointParityMultiplicity
      k (h ∘ ⇑(Equiv.symm σ))

theorem CryptBoolean.tuplePointParityMultiplicity_eq_of_hammingWeight_eq
  {n : ℕ} (k : ℕ)
  (h₁ h₂ : CryptBoolean.BooleanFunction n)
  (hweight :
    CryptBoolean.hammingWeight h₁ =
      CryptBoolean.hammingWeight h₂) :
  CryptBoolean.tuplePointParityMultiplicity
      k h₁ =
    CryptBoolean.tuplePointParityMultiplicity
      k h₂

theorem CryptBoolean.tuplePointParityMultiplicity_eq_byWeight
  {n : ℕ} (k : ℕ)
  (h : CryptBoolean.BooleanFunction n) :
  CryptBoolean.tuplePointParityMultiplicity
      k h =
    CryptBoolean.tuplePointParityMultiplicityByWeight
      k n (CryptBoolean.hammingWeight h)

theorem CryptBoolean.tuplePointParityMultiplicityByWeight_eq_fourierSum
  {n : ℕ} (k : ℕ)
  (h : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.tuplePointParityMultiplicityByWeight
        k n
        (CryptBoolean.hammingWeight h)) =
    (∑ g,
        FABL.binarySign
            (((CryptBoolean.booleanFunctionPairing
                  n)
                g)
              h) *
          (2 ^ n -
              2 *
                ↑(CryptBoolean.hammingWeight
                    g)) ^
            (2 * k)) /
      2 ^ 2 ^ n

theorem CryptBoolean.tuplePointParityMultiplicityByWeight_eq_krawtchoukSum
  {n : ℕ} (k : ℕ)
  (h : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.tuplePointParityMultiplicityByWeight
        k n
        (CryptBoolean.hammingWeight h)) =
    CryptBoolean.tuplePointParityKrawtchoukMultiplicity
      k n (CryptBoolean.hammingWeight h)