theorem CryptBoolean.binaryWeight_ofBits {n : ℕ}
  (f : Fin n → Bool) :
  CryptBoolean.binaryWeight
      (Nat.ofBits f) =
    ∑ i, (f i).toNat

theorem CryptBoolean.binaryWeight_two_pow_sub_one
  (n : ℕ) :
  CryptBoolean.binaryWeight (2 ^ n - 1) =
    n

theorem CryptBoolean.ofBits_eq_sum {n : ℕ}
  (f : Fin n → Bool) :
  Nat.ofBits f = ∑ i, (f i).toNat * 2 ^ ↑i

theorem CryptBoolean.testBit_rotateBinaryExponent
  (n k : ℕ) (i : Fin n) :
  (CryptBoolean.rotateBinaryExponent n
          k).testBit
      ↑i =
    k.testBit
      ↑((Equiv.symm (finRotate n)) i)

theorem CryptBoolean.binaryCyclicExponent_lt
  (n k : ℕ) (hn : 0 < n) (s : ℕ) :
  CryptBoolean.binaryCyclicExponent n k
      s <
    2 ^ n - 1

theorem CryptBoolean.binaryCyclicExponent_succ_eq_rotate
  (n k s : ℕ) (hn : 0 < n) :
  CryptBoolean.binaryCyclicExponent n k
      (s + 1) =
    CryptBoolean.rotateBinaryExponent n
      (CryptBoolean.binaryCyclicExponent n
        k s)

theorem CryptBoolean.binaryWeight_binaryCyclicExponent
  (n k s : ℕ) (hn : 0 < n)
  (hk : k < 2 ^ n - 1) :
  CryptBoolean.binaryWeight
      (CryptBoolean.binaryCyclicExponent n
        k s) =
    CryptBoolean.binaryWeight k

theorem CryptBoolean.binaryCyclicExponent_pos
  {n k : ℕ} (hn : 0 < n) (hk0 : 0 < k)
  (hk : k < 2 ^ n - 1) (s : ℕ) :
  0 <
    CryptBoolean.binaryCyclicExponent n k
      s

theorem CryptBoolean.pow_binaryCyclicExponent
  {n k : ℕ} (hn : 0 < n) (hk0 : 0 < k)
  (hk : k < 2 ^ n - 1)
  (x : CryptBoolean.BinaryGaloisField n)
  (s : ℕ) :
  x ^
      CryptBoolean.binaryCyclicExponent n
        k s =
    x ^ (k * 2 ^ s)

theorem CryptBoolean.functionAlgebraicDegree_traceMonomial_le_binaryWeight
  {n k : ℕ} (hn : 0 < n)
  (hk : k ≤ 2 ^ n - 1)
  (θ :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  (a : CryptBoolean.BinaryGaloisField n) :
  (FABL.functionAlgebraicDegree fun x =>
      (CryptBoolean.absoluteTrace n)
        (a * θ x ^ k)) ≤
    CryptBoolean.binaryWeight k

theorem CryptBoolean.cyclicOneRunCount_binaryCyclicExponent
  {n d s : ℕ} (hn : 0 < n)
  (hd : d < 2 ^ n - 1) :
  CryptBoolean.cyclicOneRunCount n
      (CryptBoolean.binaryCyclicExponent n
        d s) =
    CryptBoolean.cyclicOneRunCount n d

theorem CryptBoolean.cyclicOneRunCount_pos
  {n d : ℕ} (hn : 0 < n) (hd0 : 0 < d)
  (hd : d < 2 ^ n - 1) :
  0 < CryptBoolean.cyclicOneRunCount n d

theorem CryptBoolean.bitIndices_traceRunMultiplierExponent
  {n : ℕ} (hn : 0 < n) :
  (CryptBoolean.traceRunMultiplierExponent
        n).bitIndices =
    CryptBoolean.traceRunMultiplierPositions
      n

theorem CryptBoolean.testBit_traceRunMultiplierExponent
  {n i : ℕ} (hn : 0 < n) :
  (CryptBoolean.traceRunMultiplierExponent
            n).testBit
        i =
      true ↔
    i ∈
      CryptBoolean.traceRunMultiplierPositions
        n

theorem CryptBoolean.traceRunMultiplierExponent_lt_two_pow
  {n : ℕ} (hn : 0 < n) :
  CryptBoolean.traceRunMultiplierExponent
      n <
    2 ^ n

theorem CryptBoolean.binaryWeight_traceRunMultiplierExponent
  {n : ℕ} (hn : 0 < n) :
  CryptBoolean.binaryWeight
      (CryptBoolean.traceRunMultiplierExponent
        n) =
    n ⌈/⌉ n.sqrt

theorem CryptBoolean.pow_positiveCyclicSum
  {n x y : ℕ} (hn : 0 < n)
  (hxy : 0 < x + y)
  (z : CryptBoolean.BinaryGaloisField n) :
  z ^
      CryptBoolean.positiveCyclicSum n x
        y =
    z ^ (x + y)

theorem CryptBoolean.binaryWeight_positiveCyclicSum_traceRunMultiplier_le
  {n x : ℕ} (hn : 0 < n)
  (hx : x < 2 ^ n - 1) :
  CryptBoolean.binaryWeight
      (CryptBoolean.positiveCyclicSum n x
        (CryptBoolean.traceRunMultiplierExponent
          n)) ≤
    CryptBoolean.cyclicOneRunCount n x *
        (n.sqrt - 1) +
      n ⌈/⌉ n.sqrt

theorem CryptBoolean.binaryWeight_traceRunMultiplier_add_binaryCyclicExponent_le
  {n d s : ℕ} (hn : 0 < n) (hd0 : 0 < d)
  (hd : d < 2 ^ n - 1) :
  CryptBoolean.binaryWeight
      (CryptBoolean.positiveCyclicSum n
        (CryptBoolean.binaryCyclicExponent
          n d s)
        (CryptBoolean.traceRunMultiplierExponent
          n)) ≤
    CryptBoolean.cyclicOneRunCount n d *
          n.sqrt +
        n ⌈/⌉ n.sqrt -
      1

theorem CryptBoolean.algebraicImmunity_tracePowerFunction_le_runBound
  {n d : ℕ} (hn : 0 < n)
  (hd : d < 2 ^ n - 1)
  (θ :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  (a : CryptBoolean.BinaryGaloisField n)
  (_hrun :
    ↑(CryptBoolean.cyclicOneRunCount n
          d) <
      √↑n / 2) :
  CryptBoolean.algebraicImmunity
      (CryptBoolean.tracePowerFunction θ a
        d) ≤
    CryptBoolean.cyclicOneRunCount n d *
          n.sqrt +
        n ⌈/⌉ n.sqrt -
      1

theorem CryptBoolean.algebraicImmunity_eq_ceiling_half_of_odd_balanced_of_no_annihilator
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : Odd n)
  (hbalanced : CryptBoolean.IsBalanced f)
  (hnoAnnihilator :
    ∀
      (g :
        CryptBoolean.BooleanFunction n),
      g ≠ 0 →
        FABL.functionAlgebraicDegree g ≤
            (n - 1) / 2 →
          f * g ≠ 0) :
  CryptBoolean.algebraicImmunity f =
    (n + 1) / 2

theorem CryptBoolean.algebraicImmunity_le_sub_of_isKNormal
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsKNormal f k) :
  CryptBoolean.algebraicImmunity f ≤ n - k

theorem CryptBoolean.tendsto_carletNonnormalityDimension_div
  {α : ℝ} (hα : 1 < α) :
  Filter.Tendsto
    (fun n =>
      ↑(CryptBoolean.carletNonnormalityDimension
            α n) /
        ↑n)
    Filter.atTop (nhds 0)

theorem CryptBoolean.eventually_ceilingHalf_le_sub_carletNonnormalityDimension
  {α : ℝ} (hα : 1 < α) :
  ∀ᶠ (n : ℕ) in Filter.atTop,
    (n + 1) / 2 ≤
      n -
        CryptBoolean.carletNonnormalityDimension
          α n

theorem CryptBoolean.eventually_exists_algebraicImmunity_le_sub_not_isKNormal
  {α : ℝ} (hα : 1 < α) :
  ∀ᶠ (n : ℕ) in Filter.atTop,
    ∃ f,
      CryptBoolean.algebraicImmunity f ≤
          n -
            CryptBoolean.carletNonnormalityDimension
              α n ∧
        ¬CryptBoolean.IsKNormal f
            (CryptBoolean.carletNonnormalityDimension
              α n)

theorem CryptBoolean.algebraicImmunity_add_constant_one
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.algebraicImmunity (f + 1) =
    CryptBoolean.algebraicImmunity f

theorem CryptBoolean.sum_choose_below_algebraicImmunity_le_hammingWeight
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∑
      i ∈
        Finset.range
          (CryptBoolean.algebraicImmunity
            f),
      n.choose i ≤
    CryptBoolean.hammingWeight f

theorem CryptBoolean.hammingWeight_le_sum_choose_to_sub_algebraicImmunity
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.hammingWeight f ≤
    ∑
      i ∈
        Finset.range
          (n -
              CryptBoolean.algebraicImmunity
                f +
            1),
      n.choose i

theorem CryptBoolean.isBalanced_of_odd_of_algebraicImmunity_eq_ceiling_half
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : Odd n)
  (hAI :
    CryptBoolean.algebraicImmunity f =
      (n + 1) / 2) :
  CryptBoolean.IsBalanced f

theorem CryptBoolean.algebraicImmunity_add_le_add_functionAlgebraicDegree
  {n : ℕ}
  (f h : CryptBoolean.BooleanFunction n) :
  CryptBoolean.algebraicImmunity (f + h) ≤
    CryptBoolean.algebraicImmunity f +
      FABL.functionAlgebraicDegree h

theorem CryptBoolean.algebraicImmunity_sub_functionAlgebraicDegree_le_add
  {n : ℕ}
  (f h : CryptBoolean.BooleanFunction n) :
  CryptBoolean.algebraicImmunity f -
      FABL.functionAlgebraicDegree h ≤
    CryptBoolean.algebraicImmunity (f + h)