theorem CryptBoolean.hammingDistance_comp_affineEquiv
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  CryptBoolean.hammingDistance (f ∘ ⇑L)
      (g ∘ ⇑L) =
    CryptBoolean.hammingDistance f g

theorem CryptBoolean.exists_affineFunction_comp_affineEquiv
  {n : ℕ} (b : FABL.𝔽₂)
  (a : FABL.F₂Cube n)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  ∃ c d,
    FABL.affineFunction b a ∘ ⇑L =
      FABL.affineFunction c d

theorem CryptBoolean.nonlinearity_comp_affineEquiv_le
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  CryptBoolean.nonlinearity (f ∘ ⇑L) ≤
    CryptBoolean.nonlinearity f

theorem CryptBoolean.nonlinearity_comp_affineEquiv
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  CryptBoolean.nonlinearity (f ∘ ⇑L) =
    CryptBoolean.nonlinearity f

theorem CryptBoolean.hammingDistance_cast_affineFunction
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.𝔽₂) (a : FABL.F₂Cube n) :
  ↑(CryptBoolean.hammingDistance f
        (FABL.affineFunction b a)) =
    2 ^ n *
      FABL.relativeHammingDist
        (CryptBoolean.realSignView f)
        (FABL.affineSignFunction
          (FABL.signEncode b) a)

theorem CryptBoolean.bitSignInt_cast
  (b : FABL.𝔽₂) :
  ↑(CryptBoolean.bitSignInt b) =
    FABL.binarySign b

theorem CryptBoolean.hammingDistance_cast_affineFunction_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.𝔽₂) (a : FABL.F₂Cube n) :
  ↑(CryptBoolean.hammingDistance f
        (FABL.affineFunction b a)) =
    2 ^ n / 2 -
      ↑(CryptBoolean.bitSignInt b) *
          ↑(CryptBoolean.walshTransform f
              a) /
        2

theorem CryptBoolean.hammingDistance_cast_linearFunction_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  ↑(CryptBoolean.hammingDistance f
        (FABL.affineFunction 0 a)) =
    2 ^ n / 2 -
      ↑(CryptBoolean.walshTransform f a) /
        2

theorem CryptBoolean.hammingDistance_cast_complementLinearFunction_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  ↑(CryptBoolean.hammingDistance f
        (FABL.affineFunction 1 a)) =
    2 ^ n / 2 +
      ↑(CryptBoolean.walshTransform f a) /
        2

theorem CryptBoolean.nonlinearity_cast_eq_distanceToAffineSigns
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) =
    2 ^ n *
      FABL.distanceToAffineSigns
        (CryptBoolean.realSignView f)

theorem CryptBoolean.maxWalshMagnitude_cast_eq_spectralInfinityNorm
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.maxWalshMagnitude f) =
    2 ^ n *
      FABL.spectralInfinityNorm
        (CryptBoolean.realSignView f)

theorem CryptBoolean.two_mul_nonlinearity_add_maxWalshMagnitude
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  2 * CryptBoolean.nonlinearity f +
      CryptBoolean.maxWalshMagnitude f =
    2 ^ n

theorem CryptBoolean.nonlinearity_cast_eq_relation_35
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) =
    2 ^ n / 2 -
      ↑(CryptBoolean.maxWalshMagnitude
            f) /
        2

theorem CryptBoolean.exists_inv_sqrt_card_le_vectorFourierCoeff_abs
  {n : ℕ} {f : FABL.F₂Cube n → ℝ}
  (hf : FABL.IsSignValued f) :
  ∃ γ,
    (√(2 ^ n))⁻¹ ≤
      |FABL.vectorFourierCoeff f γ|

theorem CryptBoolean.spectralInfinityNorm_ge_inv_sqrt_card
  {n : ℕ} {f : FABL.F₂Cube n → ℝ}
  (hf : FABL.IsSignValued f) :
  (√(2 ^ n))⁻¹ ≤
    FABL.spectralInfinityNorm f

theorem CryptBoolean.distanceToAffineSigns_le_coveringRadius
  {n : ℕ} {f : FABL.F₂Cube n → ℝ}
  (hf : FABL.IsSignValued f) :
  FABL.distanceToAffineSigns f ≤
    1 / 2 - (√(2 ^ n))⁻¹ / 2

theorem CryptBoolean.two_pow_mul_inv_sqrt
  {n : ℕ} :
  2 ^ n * (√(2 ^ n))⁻¹ = √(2 ^ n)

theorem CryptBoolean.sqrt_two_pow_eq_rpow
  {n : ℕ} : √(2 ^ n) = 2 ^ (↑n / 2)

theorem CryptBoolean.coveringRadius_eq_relation_36
  {n : ℕ} :
  2 ^ n / 2 - √(2 ^ n) / 2 =
    2 ^ (↑n - 1) - 2 ^ (↑n / 2 - 1)

theorem CryptBoolean.nonlinearity_cast_le_coveringRadius
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) ≤
    2 ^ n / 2 - √(2 ^ n) / 2

theorem CryptBoolean.nonlinearity_cast_le_relation_36
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) ≤
    2 ^ (↑n - 1) - 2 ^ (↑n / 2 - 1)

theorem CryptBoolean.vectorFourierCoeff_abs_eq_inv_sqrt_of_spectralInfinityNorm_eq
  {n : ℕ} {f : FABL.F₂Cube n → ℝ}
  (hf : FABL.IsSignValued f)
  (hspectral :
    FABL.spectralInfinityNorm f =
      (√(2 ^ n))⁻¹)
  (γ : FABL.F₂Cube n) :
  |FABL.vectorFourierCoeff f γ| =
    (√(2 ^ n))⁻¹

theorem CryptBoolean.spectralInfinityNorm_eq_inv_sqrt_of_forall_abs
  {n : ℕ} {f : FABL.F₂Cube n → ℝ}
  (hflat :
    ∀ (γ : FABL.F₂Cube n),
      |FABL.vectorFourierCoeff f γ| =
        (√(2 ^ n))⁻¹) :
  FABL.spectralInfinityNorm f =
    (√(2 ^ n))⁻¹

theorem CryptBoolean.distanceToAffineSigns_eq_coveringRadius_iff
  {n : ℕ} {f : FABL.F₂Cube n → ℝ}
  (hf : FABL.IsSignValued f) :
  FABL.distanceToAffineSigns f =
      1 / 2 - (√(2 ^ n))⁻¹ / 2 ↔
    ∀ (γ : FABL.F₂Cube n),
      |FABL.vectorFourierCoeff f γ| =
        (√(2 ^ n))⁻¹

theorem CryptBoolean.hasFlatWalshSpectrum_iff_vectorFourierCoeff
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.HasFlatWalshSpectrum f ↔
    ∀ (a : FABL.F₂Cube n),
      |FABL.vectorFourierCoeff
            (CryptBoolean.realSignView f)
            a| =
        (√(2 ^ n))⁻¹

theorem CryptBoolean.nonlinearity_eq_coveringRadius_iff_flatWalshSpectrum
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) =
      2 ^ n / 2 - √(2 ^ n) / 2 ↔
    CryptBoolean.HasFlatWalshSpectrum f

theorem CryptBoolean.nonlinearity_cast_eq_relation_36_iff_flatWalshSpectrum
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) =
      2 ^ (↑n - 1) - 2 ^ (↑n / 2 - 1) ↔
    CryptBoolean.HasFlatWalshSpectrum f

theorem CryptBoolean.even_of_hasFlatWalshSpectrum
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hflat :
    CryptBoolean.HasFlatWalshSpectrum f) :
  Even n

theorem CryptBoolean.sqrt_two_pow_eq_pow_half
  {n : ℕ} (hn : Even n) :
  √(2 ^ n) = 2 ^ (n / 2)

theorem CryptBoolean.even_of_isBent {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) : Even n

theorem CryptBoolean.hasFlatWalshSpectrum_iff_isBent
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.HasFlatWalshSpectrum f ↔
    CryptBoolean.IsBent f

theorem CryptBoolean.even_of_exists_isBent {n : ℕ}
  (h : ∃ f, CryptBoolean.IsBent f) :
  Even n

theorem CryptBoolean.not_isBalanced_of_isBent
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) :
  ¬CryptBoolean.IsBalanced f

theorem CryptBoolean.isBent_iff_nonlinearity_cast_eq_relation_36_of_even
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : Even n) :
  CryptBoolean.IsBent f ↔
    ↑(CryptBoolean.nonlinearity f) =
      2 ^ (↑n - 1) - 2 ^ (↑n / 2 - 1)

theorem CryptBoolean.nonlinearity_cast_eq_relation_36_iff_isBent
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) =
      2 ^ (↑n - 1) - 2 ^ (↑n / 2 - 1) ↔
    CryptBoolean.IsBent f

theorem CryptBoolean.carletRandomNonlinearityThreshold_eq_displayed
  (n : ℕ) :
  CryptBoolean.carletRandomNonlinearityThreshold
      n =
    2 ^ (↑n - 1) -
      √↑n * 2 ^ ((↑n - 1) / 2)

theorem CryptBoolean.carletRandomFourierThreshold_nonneg
  (n : ℕ) :
  0 ≤
    CryptBoolean.carletRandomFourierThreshold
      n

theorem CryptBoolean.card_mul_carletRandomFourierThreshold_sq_div_two
  (n : ℕ) :
  ↑(Fintype.card (FABL.SignCube n)) *
        CryptBoolean.carletRandomFourierThreshold
            n ^
          2 /
      2 =
    ↑n

theorem CryptBoolean.measure_fourierInfinityNorm_ge_carletThreshold_le
  (n : ℕ) :
  (FABL.uniformPMF
            (FABL.BooleanFunction
              n)).toMeasure.real
      {f |
        CryptBoolean.carletRandomFourierThreshold
            n ≤
          FABL.fourierInfinityNorm
            f.toReal} ≤
    2 ^ n * (2 * Real.exp (-↑n))

theorem CryptBoolean.fourier_union_bound_eq_failureBound
  (n : ℕ) :
  2 ^ n * (2 * Real.exp (-↑n)) =
    CryptBoolean.carletRandomNonlinearityFailureBound
      n

theorem CryptBoolean.tendsto_carletRandomNonlinearityFailureBound :
  Filter.Tendsto
    CryptBoolean.carletRandomNonlinearityFailureBound
    Filter.atTop (nhds 0)

theorem CryptBoolean.spectralInfinityNorm_encoding_eq_fourierInfinityNorm
  {n : ℕ} (g : FABL.BooleanFunction n) :
  FABL.spectralInfinityNorm
      (CryptBoolean.realSignView
        (FABL.booleanFunctionF₂Encoding
          g)) =
    FABL.fourierInfinityNorm g.toReal

theorem CryptBoolean.nonlinearity_encoding_eq_fourierInfinityNorm
  {n : ℕ} (g : FABL.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity
        (FABL.booleanFunctionF₂Encoding
          g)) =
    2 ^ n / 2 -
      2 ^ n *
          FABL.fourierInfinityNorm
            g.toReal /
        2

theorem CryptBoolean.carletRandomNonlinearityThreshold_lt_of_fourierInfinityNorm_lt
  {n : ℕ} (g : FABL.BooleanFunction n)
  (h :
    FABL.fourierInfinityNorm g.toReal <
      CryptBoolean.carletRandomFourierThreshold
        n) :
  CryptBoolean.carletRandomNonlinearityThreshold
      n <
    ↑(CryptBoolean.nonlinearity
        (FABL.booleanFunctionF₂Encoding
          g))

theorem CryptBoolean.one_sub_failureBound_le_carletRandomNonlinearityProbability
  (n : ℕ) :
  1 -
      CryptBoolean.carletRandomNonlinearityFailureBound
        n ≤
    CryptBoolean.carletRandomNonlinearityProbability
      n

theorem CryptBoolean.tendsto_carletRandomNonlinearityProbability :
  Filter.Tendsto
    CryptBoolean.carletRandomNonlinearityProbability
    Filter.atTop (nhds 1)

theorem CryptBoolean.rodierRandomNonlinearityLowerThreshold_eq_displayed
  (n : ℕ) :
  CryptBoolean.rodierRandomNonlinearityLowerThreshold
      n =
    2 ^ (↑n - 1) -
      2 ^ (↑n / 2 - 1) * √↑n *
        (√(2 * Real.log 2) +
          4 * Real.log ↑n / ↑n)

theorem CryptBoolean.rodierRandomFourierUpperThreshold_nonneg
  (n : ℕ) :
  0 ≤
    CryptBoolean.rodierRandomFourierUpperThreshold
      n

theorem CryptBoolean.card_mul_rodierRandomFourierUpperThreshold_sq_div_two_ge
  {n : ℕ} (hn : 1 ≤ n) :
  ↑n * Real.log 2 + Real.log ↑n ≤
    ↑(Fintype.card (FABL.SignCube n)) *
        CryptBoolean.rodierRandomFourierUpperThreshold
            n ^
          2 /
      2

theorem CryptBoolean.measure_fourierInfinityNorm_ge_rodierUpperThreshold_le
  {n : ℕ} (hn : 1 ≤ n) :
  (FABL.uniformPMF
            (FABL.BooleanFunction
              n)).toMeasure.real
      {f |
        CryptBoolean.rodierRandomFourierUpperThreshold
            n ≤
          FABL.fourierInfinityNorm
            f.toReal} ≤
    2 * (↑n)⁻¹

theorem CryptBoolean.tendsto_rodierRandomNonlinearityLowerFailureBound :
  Filter.Tendsto
    CryptBoolean.rodierRandomNonlinearityLowerFailureBound
    Filter.atTop (nhds 0)

theorem CryptBoolean.rodierRandomNonlinearityLowerThreshold_lt_of_fourierInfinityNorm_lt
  {n : ℕ} (g : FABL.BooleanFunction n)
  (h :
    FABL.fourierInfinityNorm g.toReal <
      CryptBoolean.rodierRandomFourierUpperThreshold
        n) :
  CryptBoolean.rodierRandomNonlinearityLowerThreshold
      n <
    ↑(CryptBoolean.nonlinearity
        (FABL.booleanFunctionF₂Encoding
          g))

theorem CryptBoolean.one_sub_rodierLowerFailureBound_le_probability
  {n : ℕ} (hn : 1 ≤ n) :
  1 -
      CryptBoolean.rodierRandomNonlinearityLowerFailureBound
        n ≤
    CryptBoolean.rodierRandomNonlinearityLowerProbability
      n

theorem CryptBoolean.tendsto_rodierRandomNonlinearityLowerProbability :
  Filter.Tendsto
    CryptBoolean.rodierRandomNonlinearityLowerProbability
    Filter.atTop (nhds 1)