theorem FABL.uniformProbability_andFunction_eq_neg_one
  (w : ℕ) :
  (FABL.uniformProbability fun x =>
      FABL.andFunction w x = -1) =
    (2 ^ w)⁻¹

theorem FABL.uniformProbability_andFunction_eq_one
  (w : ℕ) :
  (FABL.uniformProbability fun x =>
      FABL.andFunction w x = 1) =
    1 - (2 ^ w)⁻¹

theorem FABL.tribes_zero (w : ℕ) :
  FABL.tribes w 0 = fun x => 1

theorem FABL.tribes_neg_one_probability_zero
  (w : ℕ) :
  (FABL.uniformProbability fun x =>
      FABL.tribes w 0 x = -1) =
    1 - (1 - (2 ^ w)⁻¹) ^ 0

theorem FABL.tribes_neg_one_probability
  (w s : ℕ) :
  (FABL.uniformProbability fun x =>
      FABL.tribes w s x = -1) =
    1 - (1 - (2 ^ w)⁻¹) ^ s

theorem FABL.tribesCriticalSize_spec (w : ℕ) :
  FABL.IsTribesCriticalSizeCandidate w
    (FABL.tribesCriticalSize w)

theorem FABL.tribesCriticalSize_eq_floor_threshold
  (w : ℕ) (hw : 0 < w) :
  FABL.tribesCriticalSize w =
    ⌊FABL.tribesCriticalThreshold w⌋₊

theorem FABL.tribesCriticalSize_eq_main_sub_error
  (w : ℕ) :
  ↑(FABL.tribesCriticalSize w) =
    Real.log 2 * 2 ^ w -
      FABL.tribesCriticalSizeError w

theorem FABL.tribesCriticalSizeError_mem_Icc
  (w : ℕ) (hw : 0 < w) :
  FABL.tribesCriticalSizeError w ∈
    Set.Icc (Real.log 2 / 4) 2

theorem FABL.tribesCriticalSizeError_isTheta_one :
  FABL.tribesCriticalSizeError =Θ[Filter.atTop]
    fun _w => 1

theorem FABL.tribesCriticalDimension_eq_main_sub_error
  (w : ℕ) :
  ↑(FABL.tribesCriticalDimension w) =
    Real.log 2 * ↑w * 2 ^ w -
      FABL.tribesCriticalDimensionError w

theorem FABL.tribesCriticalDimensionError_eq
  (w : ℕ) :
  FABL.tribesCriticalDimensionError w =
    ↑w * FABL.tribesCriticalSizeError w

theorem FABL.tribesCriticalDimensionError_isTheta_natCast :
  FABL.tribesCriticalDimensionError =Θ[Filter.atTop]
    fun w => ↑w

theorem FABL.tribesCriticalSizeError_isLittleO_two_pow :
  FABL.tribesCriticalSizeError =o[Filter.atTop]
    fun w => 2 ^ w

theorem FABL.tribesCriticalDimension_isEquivalent_main :
  Asymptotics.IsEquivalent Filter.atTop
    (fun w =>
      ↑(FABL.tribesCriticalDimension w))
    fun w => Real.log 2 * ↑w * 2 ^ w

theorem FABL.tendsto_tribesCriticalDimension_succ_div :
  Filter.Tendsto
    (fun w =>
      ↑(FABL.tribesCriticalDimension
            (w + 1)) /
        ↑(FABL.tribesCriticalDimension w))
    Filter.atTop (nhds 2)

theorem FABL.tribesCriticalWidth_eq_log_sub_loglog_add_error
  (w : ℕ) :
  ↑w =
    Real.logb 2
          ↑(FABL.tribesCriticalDimension
              w) -
        Real.logb 2
          (Real.log
            ↑(FABL.tribesCriticalDimension
                w)) +
      FABL.tribesCriticalWidthError w

theorem FABL.tendsto_log_tribesCriticalDimension_div_width :
  Filter.Tendsto
    (fun w =>
      Real.log
          ↑(FABL.tribesCriticalDimension
              w) /
        (↑w * Real.log 2))
    Filter.atTop (nhds 1)

theorem FABL.tribesCriticalWidthError_isLittleO_one :
  FABL.tribesCriticalWidthError =o[Filter.atTop]
    fun _w => 1

theorem FABL.tendsto_tribesCriticalDimension_atTop :
  Filter.Tendsto
    (fun w =>
      ↑(FABL.tribesCriticalDimension w))
    Filter.atTop Filter.atTop

theorem FABL.tendsto_two_pow_mul_log_tribesCriticalDimension_div :
  Filter.Tendsto
    (fun w =>
      2 ^ w *
          Real.log
            ↑(FABL.tribesCriticalDimension
                w) /
        ↑(FABL.tribesCriticalDimension w))
    Filter.atTop (nhds 1)

theorem FABL.tribesCriticalPowerRelativeError_isLittleO_one :
  FABL.tribesCriticalPowerRelativeError =o[Filter.atTop]
    fun _w => 1

theorem FABL.eventually_two_pow_eq_dimension_div_log_mul_one_add_error :
  ∀ᶠ (w : ℕ) in Filter.atTop,
    2 ^ w =
      ↑(FABL.tribesCriticalDimension w) /
          Real.log
            ↑(FABL.tribesCriticalDimension
                w) *
        (1 +
          FABL.tribesCriticalPowerRelativeError
            w)

theorem FABL.tribesCritical_neg_one_probability_eq_half_sub_deficit
  (w : ℕ) :
  (FABL.uniformProbability fun x =>
      FABL.tribesCritical w x = -1) =
    1 / 2 -
      FABL.tribesCriticalProbabilityDeficit
        w

theorem FABL.tribesCriticalProbabilityDeficit_eq_pow
  (w : ℕ) :
  FABL.tribesCriticalProbabilityDeficit
      w =
    (1 - (2 ^ w)⁻¹) ^
        FABL.tribesCriticalSize w -
      1 / 2

theorem FABL.tribesCriticalProbabilityDeficit_mem_Icc
  (w : ℕ) (hw : 0 < w) :
  FABL.tribesCriticalProbabilityDeficit
      w ∈
    Set.Icc 0 (2 ^ w)⁻¹

theorem FABL.tribesCriticalProbabilityDeficit_isBigO_log_dimension_div_dimension :
  FABL.tribesCriticalProbabilityDeficit =O[Filter.atTop]
    fun w =>
    Real.log
        ↑(FABL.tribesCriticalDimension
            w) /
      ↑(FABL.tribesCriticalDimension w)

theorem FABL.isPivotal_tribes_iff (w s : ℕ)
  (i : Fin (s * w))
  (x : FABL.SignCube (s * w)) :
  FABL.IsPivotal (FABL.tribes w s) i x ↔
    FABL.TribesRestTrue w s i x ∧
      FABL.TribesOthersFalse w s i x

theorem FABL.card_andFunction_eq_one (w : ℕ) :
  {z | FABL.andFunction w z = 1}.card =
    2 ^ w - 1

theorem FABL.booleanInfluence_tribes (w s : ℕ)
  (hw : 0 < w) (hs : 0 < s)
  (i : Fin (s * w)) :
  FABL.booleanInfluence (FABL.tribes w s)
      i =
    (2 ^ (w - 1))⁻¹ *
      (1 - (2 ^ w)⁻¹) ^ (s - 1)

theorem FABL.totalInfluence_tribes (w s : ℕ)
  (hw : 0 < w) (hs : 0 < s) :
  FABL.totalInfluence
      (FABL.tribes w s).toReal =
    ↑(s * w) *
      ((2 ^ (w - 1))⁻¹ *
        (1 - (2 ^ w)⁻¹) ^ (s - 1))

theorem FABL.tribesCriticalSize_pos (w : ℕ)
  (hw : 0 < w) :
  0 < FABL.tribesCriticalSize w

theorem FABL.booleanInfluence_tribesCritical
  (w : ℕ) (hw : 0 < w)
  (i :
    Fin
      (FABL.tribesCriticalDimension w)) :
  FABL.booleanInfluence
      (FABL.tribesCritical w) i =
    FABL.tribesCriticalCoordinateInfluence
      w

theorem FABL.totalInfluence_tribesCritical (w : ℕ)
  (hw : 0 < w) :
  FABL.totalInfluence
      (FABL.tribesCritical w).toReal =
    ↑(FABL.tribesCriticalDimension w) *
      FABL.tribesCriticalCoordinateInfluence
        w

theorem FABL.tendsto_tribesCriticalCoordinateInfluence_mul_dimension_div_log :
  Filter.Tendsto
    (fun w =>
      FABL.tribesCriticalCoordinateInfluence
            w *
          ↑(FABL.tribesCriticalDimension
              w) /
        Real.log
          ↑(FABL.tribesCriticalDimension
              w))
    Filter.atTop (nhds 1)

theorem FABL.tribesCriticalCoordinateInfluenceRelativeError_isLittleO_one :
  FABL.tribesCriticalCoordinateInfluenceRelativeError =o[Filter.atTop]
    fun _w => 1

theorem FABL.eventually_booleanInfluence_tribesCritical_eq_log_dimension_div_mul_one_add_error :
  ∀ᶠ (w : ℕ) in Filter.atTop,
    ∀
      (i :
        Fin
          (FABL.tribesCriticalDimension
            w)),
      FABL.booleanInfluence
          (FABL.tribesCritical w) i =
        Real.log
              ↑(FABL.tribesCriticalDimension
                  w) /
            ↑(FABL.tribesCriticalDimension
                w) *
          (1 +
            FABL.tribesCriticalCoordinateInfluenceRelativeError
              w)

theorem FABL.eventually_totalInfluence_tribesCritical_eq_log_dimension_mul_one_add_error :
  ∀ᶠ (w : ℕ) in Filter.atTop,
    FABL.totalInfluence
        (FABL.tribesCritical w).toReal =
      Real.log
          ↑(FABL.tribesCriticalDimension
              w) *
        (1 +
          FABL.tribesCriticalCoordinateInfluenceRelativeError
            w)

theorem FABL.exists_booleanInfluence_eq_maximumInfluence
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hn : 0 < n) :
  ∃ i,
    FABL.booleanInfluence f i =
      FABL.maximumInfluence f

theorem FABL.edgeKKL {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hvar : 0 < FABL.variance f.toReal) :
  9 *
        Real.rpow 9
          (-(FABL.totalInfluence
                f.toReal /
              FABL.variance f.toReal)) /
      (FABL.totalInfluence f.toReal /
          FABL.variance f.toReal) ^
        2 ≤
    FABL.maximumInfluence f

theorem FABL.kkl {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.variance f.toReal * Real.log ↑n /
      (100 * ↑n) ≤
    FABL.maximumInfluence f

theorem FABL.mean_booleanFunction_eq_prob_one_sub_prob_neg_one
  {m : ℕ} (f : FABL.BooleanFunction m) :
  FABL.mean f.toReal =
    (FABL.uniformProbability fun x =>
        f x = 1) -
      FABL.uniformProbability fun x =>
        f x = -1

theorem FABL.fourierCoeff_tribes_empty (w s : ℕ) :
  FABL.fourierCoeff
      (FABL.tribes w s).toReal ∅ =
    2 * (1 - (2 ^ w)⁻¹) ^ s - 1

theorem FABL.signValue_andFunction (w : ℕ)
  (x : FABL.SignCube w) :
  FABL.signValue (FABL.andFunction w x) =
    1 -
      2 *
        ∏ i,
          (1 - FABL.signValue (x i)) / 2

theorem FABL.signValue_orFunction (s : ℕ)
  (v : FABL.SignCube s) :
  FABL.signValue (FABL.orFunction s v) =
    2 *
        ∏ i,
          (1 + FABL.signValue (v i)) / 2 -
      1

theorem FABL.mem_tribeFrequencyPart (w s : ℕ)
  (T : Finset (Fin (s * w))) (i : Fin s)
  (o : Fin w) :
  o ∈ FABL.tribeFrequencyPart w s T i ↔
    finProdFinEquiv (i, o) ∈ T

theorem FABL.tribes_toReal_eq (w s : ℕ)
  (x : FABL.SignCube (s * w)) :
  (FABL.tribes w s).toReal x =
    2 *
        ∏ i,
          (1 +
              FABL.signValue
                (FABL.andFunction w
                  (FABL.inputBlock x
                    i))) /
            2 -
      1

theorem FABL.fourierCoeff_andFunction_empty
  (w : ℕ) :
  FABL.fourierCoeff
      (FABL.andFunction w).toReal ∅ =
    1 - 2 * (2 ^ w)⁻¹

theorem FABL.fourierCoeff_andFunction_of_ne_empty
  (w : ℕ) (S : Finset (Fin w))
  (hS : S ≠ ∅) :
  FABL.fourierCoeff
      (FABL.andFunction w).toReal S =
    -2 * (2 ^ w)⁻¹ * (-1) ^ S.card

theorem FABL.fourierCoeff_andFunction (w : ℕ)
  (S : Finset (Fin w)) :
  FABL.fourierCoeff
      (FABL.andFunction w).toReal S =
    if S = ∅ then 1 - 2 * (2 ^ w)⁻¹
    else -2 * (2 ^ w)⁻¹ * (-1) ^ S.card

theorem FABL.expect_one_add_andFunction_mul_monomial
  (w : ℕ) (S : Finset (Fin w)) :
  (Finset.univ.expect fun y =>
      (1 +
          FABL.signValue
            (FABL.andFunction w y)) *
        FABL.monomial S y) =
    if S = ∅ then 2 * (1 - (2 ^ w)⁻¹)
    else
      2 * (2 ^ w)⁻¹ * (-1) ^ (S.card + 1)