theorem FABL.briberySets_succ {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hn : 0 < n) (t : ℕ) :
  FABL.briberySets f hn (t + 1) =
    if
        FABL.mean
            (FABL.bribeFunction f
                (FABL.briberySets f hn t)
                1).toReal <
          99 / 100 then
      insert
        (FABL.maximumInfluenceCoordinate
          (FABL.bribeFunction f
            (FABL.briberySets f hn t) 1)
          hn)
        (FABL.briberySets f hn t)
    else FABL.briberySets f hn t

theorem FABL.card_briberySets_le {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hn : 0 < n) (t : ℕ) :
  (FABL.briberySets f hn t).card ≤ t

theorem FABL.briberyIncrement_nonneg (n : ℕ) :
  0 ≤ FABL.briberyIncrement n

theorem FABL.mean_briberySets_ge_initial_add_card_mul
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : Monotone f) (hn : 2 ≤ n)
  (hmean : -99 / 100 ≤ FABL.mean f.toReal)
  (t : ℕ) :
  FABL.mean
      (FABL.bribeFunction f
          (FABL.briberySets f ⋯ t)
          1).toReal ≥
    FABL.mean f.toReal +
      ↑(FABL.briberySets f ⋯ t).card *
        FABL.briberyIncrement n

theorem FABL.card_briberySets_eq_of_mean_lt_target
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : Monotone f) (hn : 2 ≤ n)
  (hmean : -99 / 100 ≤ FABL.mean f.toReal)
  {t : ℕ} (ht : t ≤ n)
  (hbelow :
    FABL.mean
        (FABL.bribeFunction f
            (FABL.briberySets f ⋯ t)
            1).toReal <
      99 / 100) :
  (FABL.briberySets f ⋯ t).card = t

theorem FABL.mean_bribeFunction_univ_one {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hf : Monotone f)
  (hmean :
    -99 / 100 ≤ FABL.mean f.toReal) :
  FABL.mean
      (FABL.bribeFunction f Finset.univ
          1).toReal =
    1

theorem FABL.mean_briberySets_final_ge_target
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : Monotone f) (hn : 2 ≤ n)
  (hmean :
    -99 / 100 ≤ FABL.mean f.toReal) :
  99 / 100 ≤
    FABL.mean
      (FABL.bribeFunction f
          (FABL.briberySets f ⋯ n)
          1).toReal

theorem FABL.proposition9_27_positive {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hf : Monotone f) (hn : 2 ≤ n)
  (hmean :
    -99 / 100 ≤ FABL.mean f.toReal) :
  ∃ J,
    99 / 100 ≤
        FABL.mean
          (FABL.bribeFunction f J
              1).toReal ∧
      ↑J.card ≤ 10000 * ↑n / Real.log ↑n

theorem FABL.monotone_dualBooleanFunction {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hf : Monotone f) :
  Monotone (FABL.dualBooleanFunction f)

theorem FABL.mean_dualBooleanFunction {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.mean
      (FABL.dualBooleanFunction
          f).toReal =
    -FABL.mean f.toReal

theorem FABL.mean_bribeFunction_dual_one {n : ℕ}
  (f : FABL.BooleanFunction n)
  (J : Finset (Fin n)) :
  FABL.mean
      (FABL.bribeFunction
          (FABL.dualBooleanFunction f) J
          1).toReal =
    -FABL.mean
        (FABL.bribeFunction f J
            (-1)).toReal

theorem FABL.proposition9_27_negative {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hf : Monotone f) (hn : 2 ≤ n)
  (hmean :
    FABL.mean f.toReal ≤ 99 / 100) :
  ∃ J,
    FABL.mean
          (FABL.bribeFunction f J
              (-1)).toReal ≤
        -99 / 100 ∧
      ↑J.card ≤ 10000 * ↑n / Real.log ↑n

theorem FABL.proposition9_27 {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hf : Monotone f) (hn : 2 ≤ n) :
  (-99 / 100 ≤ FABL.mean f.toReal →
      ∃ J,
        99 / 100 ≤
            FABL.mean
              (FABL.bribeFunction f J
                  1).toReal ∧
          ↑J.card ≤
            10000 * ↑n / Real.log ↑n) ∧
    (FABL.mean f.toReal ≤ 99 / 100 →
      ∃ J,
        FABL.mean
              (FABL.bribeFunction f J
                  (-1)).toReal ≤
            -99 / 100 ∧
          ↑J.card ≤
            10000 * ↑n / Real.log ↑n)

theorem FABL.bribeInput_insert {n : ℕ}
  (J : Finset (Fin n)) (i : Fin n)
  (b : FABL.Sign) (x : FABL.SignCube n) :
  FABL.bribeInput (insert i J) b x =
    FABL.bribeInput J b
      (FABL.setCoordinate x i b)

theorem FABL.bribeFunction_insert {n : ℕ}
  (f : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (i : Fin n)
  (b : FABL.Sign) :
  FABL.bribeFunction f (insert i J) b =
    fun x =>
    FABL.bribeFunction f J b
      (FABL.setCoordinate x i b)

theorem FABL.monotone_bribeFunction {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hf : Monotone f) (J : Finset (Fin n))
  (b : FABL.Sign) :
  Monotone (FABL.bribeFunction f J b)

theorem FABL.booleanInfluence_bribeFunction_eq_zero_of_mem
  {n : ℕ} (f : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (b : FABL.Sign)
  {i : Fin n} (hi : i ∈ J) :
  FABL.booleanInfluence
      (FABL.bribeFunction f J b) i =
    0

theorem FABL.mean_toReal_mem_Icc {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.mean f.toReal ∈ Set.Icc (-1) 1

theorem FABL.mean_coordinateExpectation {n : ℕ}
  (f : FABL.SignCube n → ℝ) (i : Fin n) :
  FABL.mean
      ((FABL.coordinateExpectation i) f) =
    FABL.mean f

theorem FABL.mean_fixCoordinate_one {n : ℕ}
  (f : FABL.SignCube n → ℝ) (i : Fin n) :
  (FABL.mean fun x =>
      f (FABL.setCoordinate x i 1)) =
    FABL.mean f + FABL.fourierCoeff f {i}

theorem FABL.mean_bribeFunction_insert_one {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hf : Monotone f) (J : Finset (Fin n))
  (i : Fin n) :
  FABL.mean
      (FABL.bribeFunction f (insert i J)
          1).toReal =
    FABL.mean
        (FABL.bribeFunction f J
            1).toReal +
      FABL.booleanInfluence
        (FABL.bribeFunction f J 1) i

theorem FABL.variance_ge_of_mean_mem_bribery_window
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hlower :
    -99 / 100 ≤ FABL.mean f.toReal)
  (hupper :
    FABL.mean f.toReal ≤ 99 / 100) :
  199 / 10000 ≤ FABL.variance f.toReal

theorem FABL.exists_fresh_bribery_step {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hf : Monotone f) (J : Finset (Fin n))
  (hn : 2 ≤ n)
  (hlower :
    -99 / 100 ≤
      FABL.mean
        (FABL.bribeFunction f J 1).toReal)
  (hupper :
    FABL.mean
        (FABL.bribeFunction f J
            1).toReal <
      99 / 100) :
  ∃ i ∉ J,
    FABL.mean
        (FABL.bribeFunction f (insert i J)
            1).toReal ≥
      FABL.mean
          (FABL.bribeFunction f J
              1).toReal +
        FABL.briberyIncrement n

theorem FABL.booleanInfluence_maximumInfluenceCoordinate
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hn : 0 < n) :
  FABL.booleanInfluence f
      (FABL.maximumInfluenceCoordinate f
        hn) =
    FABL.maximumInfluence f

theorem FABL.maximumInfluenceCoordinate_bribery_step
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : Monotone f) (J : Finset (Fin n))
  (hn : 2 ≤ n)
  (hlower :
    -99 / 100 ≤
      FABL.mean
        (FABL.bribeFunction f J 1).toReal)
  (hupper :
    FABL.mean
        (FABL.bribeFunction f J
            1).toReal <
      99 / 100) :
  have i :=
    FABL.maximumInfluenceCoordinate
      (FABL.bribeFunction f J 1) ⋯;
  i ∉ J ∧
    FABL.mean
        (FABL.bribeFunction f (insert i J)
            1).toReal ≥
      FABL.mean
          (FABL.bribeFunction f J
              1).toReal +
        FABL.briberyIncrement n

theorem FABL.three_mul_variance_mul_rpow_le_totalStableInfluence_one_third
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hvar : 0 < FABL.variance f.toReal) :
  3 * FABL.variance f.toReal *
      (1 / 3).rpow
        (FABL.totalInfluence f.toReal /
          FABL.variance f.toReal) ≤
    FABL.totalStableInfluence (1 / 3)
      f.toReal

theorem FABL.card_theorem9_28_influentialCoordinates_le
  {n : ℕ} (f : FABL.BooleanFunction n)
  {ε : ℝ} (hε : 0 < ε) (k : ℕ)
  (hI :
    0 < FABL.totalInfluence f.toReal) :
  ↑(FABL.influentialCoordinates f
          (FABL.theorem9_28Threshold f ε
            k)).card ≤
    FABL.totalInfluence f.toReal ^ 3 /
        ε ^ 2 *
      9 ^ k

theorem FABL.theorem9_28_spectrum_concentrated
  {n : ℕ} (f : FABL.BooleanFunction n)
  {ε : ℝ} (hε : 0 < ε) (k : ℕ)
  (hI :
    0 < FABL.totalInfluence f.toReal) :
  FABL.IsFourierSpectrumConcentratedOn
    f.toReal ε
    (FABL.theorem9_28Family f ε k)

theorem FABL.theorem9_28_small_spectrum_concentrated
  {n : ℕ} (f : FABL.BooleanFunction n)
  {ε : ℝ} (hε : 0 < ε) (k : ℕ)
  (hI : 0 < FABL.totalInfluence f.toReal)
  (hdegree :
    FABL.IsFourierSpectrumConcentratedUpTo
      f.toReal ε ↑k) :
  FABL.IsFourierSpectrumConcentratedOn
    f.toReal (2 * ε)
    (FABL.theorem9_28SmallFamily f ε k)

theorem FABL.coordinateJuntaApproximation_isKJunta
  {n : ℕ} (f : FABL.BooleanFunction n)
  (J : Finset (Fin n)) :
  FABL.IsKJunta
    (FABL.coordinateJuntaApproximation f
      J)
    J.card

theorem FABL.two_mul_relativeHammingDist_coordinateJuntaApproximation_le
  {n : ℕ} (f : FABL.BooleanFunction n)
  (J : Finset (Fin n)) :
  2 *
      FABL.relativeHammingDist f
        (FABL.coordinateJuntaApproximation
          f J) ≤
    FABL.fourierWeightOutside f.toReal
      {S | S ⊆ J}

theorem FABL.theorem9_28_close_to_coordinateJunta
  {n : ℕ} (f : FABL.BooleanFunction n)
  {ε : ℝ} (hε : 0 < ε) (k : ℕ)
  (hI : 0 < FABL.totalInfluence f.toReal)
  (hdegree :
    FABL.IsFourierSpectrumConcentratedUpTo
      f.toReal ε ↑k) :
  FABL.relativeHammingDist f
      (FABL.coordinateJuntaApproximation f
        (FABL.influentialCoordinates f
          (FABL.theorem9_28Threshold f ε
            k))) ≤
    ε