theorem FABL.fourierWeightAboveReal_natCast
  {n : ℕ} (k : ℕ)
  (f : FABL.SignCube n → ℝ) :
  FABL.fourierWeightAboveReal (↑k) f =
    FABL.fourierWeightAbove k f

theorem FABL.spectralSample_tailMass_eq_fourierWeightAboveReal
  {n : ℕ} (f : FABL.BooleanFunction n)
  (k : ℝ) :
  ∑ S with k < ↑S.card,
      ((FABL.spectralSample f) S).toReal =
    FABL.fourierWeightAboveReal k f.toReal

theorem FABL.isFourierSpectrumConcentratedUpTo_totalInfluence_div
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  {ε : ℝ} (hε : 0 < ε) :
  FABL.IsFourierSpectrumConcentratedUpTo f
    ε (FABL.totalInfluence f / ε)

theorem FABL.one_sub_two_mul_pow_le_exp_neg_two
  {δ : ℝ} (hδpos : 0 < δ)
  (hδhalf : δ ≤ 1 / 2) {m : ℕ}
  (hm : 1 / δ ≤ ↑m) :
  (1 - 2 * δ) ^ m ≤ Real.exp (-2)

theorem FABL.one_sub_one_sub_two_mul_pow_nonneg
  {δ : ℝ} (hδnonneg : 0 ≤ δ)
  (hδhalf : δ ≤ 1 / 2) (m : ℕ) :
  0 ≤ 1 - (1 - 2 * δ) ^ m

theorem FABL.monotone_one_sub_one_sub_two_mul_pow
  {δ : ℝ} (hδnonneg : 0 ≤ δ)
  (hδhalf : δ ≤ 1 / 2) :
  Monotone fun m => 1 - (1 - 2 * δ) ^ m

theorem FABL.two_div_one_sub_exp_neg_two_le_three :
  2 / (1 - Real.exp (-2)) ≤ 3

theorem FABL.two_mul_noiseSensitivity_eq_sum_fourier
  {n : ℕ} (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1)
  (f : FABL.BooleanFunction n) :
  2 * FABL.noiseSensitivity δ hδ f =
    ∑ S,
      (1 - (1 - 2 * δ) ^ S.card) *
        FABL.fourierCoeff f.toReal S ^ 2

theorem FABL.noiseSensitivity_nonneg {n : ℕ}
  (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1)
  (f : FABL.BooleanFunction n) :
  0 ≤ FABL.noiseSensitivity δ hδ f

theorem FABL.isFourierSpectrumConcentratedUpTo_noiseSensitivity
  {n : ℕ} (f : FABL.BooleanFunction n)
  {δ : ℝ} (hδpos : 0 < δ)
  (hδhalf : δ ≤ 1 / 2) :
  FABL.IsFourierSpectrumConcentratedUpTo
    f.toReal
    (2 / (1 - Real.exp (-2)) *
      FABL.noiseSensitivity δ ⋯ f)
    (1 / δ)

theorem FABL.two_div_one_sub_exp_neg_two_mul_noiseSensitivity_le_three
  {n : ℕ} (f : FABL.BooleanFunction n)
  {δ : ℝ} (hδ : δ ∈ Set.Icc 0 1) :
  2 / (1 - Real.exp (-2)) *
      FABL.noiseSensitivity δ hδ f ≤
    3 * FABL.noiseSensitivity δ hδ f

theorem FABL.monomial_tailFrequency_fin_cons
  {n : ℕ} (S : Finset (Fin n))
  (b : FABL.Sign) (x : FABL.SignCube n) :
  FABL.monomial (FABL.tailFrequency S)
      (Fin.cons b x) =
    FABL.monomial S x

theorem FABL.monomial_insert_zero_tailFrequency_fin_cons
  {n : ℕ} (S : Finset (Fin n))
  (b : FABL.Sign) (x : FABL.SignCube n) :
  FABL.monomial
      (insert 0 (FABL.tailFrequency S))
      (Fin.cons b x) =
    FABL.signValue b * FABL.monomial S x

theorem FABL.fourierCoeff_tailFrequency {n : ℕ}
  (f : FABL.SignCube (n + 1) → ℝ)
  (S : Finset (Fin n)) :
  FABL.fourierCoeff f
      (FABL.tailFrequency S) =
    (FABL.fourierCoeff
          (FABL.firstCoordinateSlice f 1)
          S +
        FABL.fourierCoeff
          (FABL.firstCoordinateSlice f
            (-1))
          S) /
      2

theorem FABL.fourierCoeff_insert_zero_tailFrequency
  {n : ℕ} (f : FABL.SignCube (n + 1) → ℝ)
  (S : Finset (Fin n)) :
  FABL.fourierCoeff f
      (insert 0 (FABL.tailFrequency S)) =
    (FABL.fourierCoeff
          (FABL.firstCoordinateSlice f 1)
          S -
        FABL.fourierCoeff
          (FABL.firstCoordinateSlice f
            (-1))
          S) /
      2

theorem FABL.uniformProbability_ne_zero_eq_firstCoordinateSlices
  {n : ℕ}
  (f : FABL.SignCube (n + 1) → ℝ) :
  (FABL.uniformProbability fun x =>
      f x ≠ 0) =
    ((FABL.uniformProbability fun x =>
          FABL.firstCoordinateSlice f 1
              x ≠
            0) +
        FABL.uniformProbability fun x =>
          FABL.firstCoordinateSlice f (-1)
              x ≠
            0) /
      2

theorem FABL.exists_fourierCoeff_ne_zero_of_ne_zero
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (hf : f ≠ 0) :
  ∃ S, FABL.fourierCoeff f S ≠ 0

theorem FABL.fourierDegree_firstCoordinateSlice_le
  {n : ℕ} (f : FABL.SignCube (n + 1) → ℝ)
  (b : FABL.Sign) {k : ℕ}
  (hdegree : FABL.fourierDegree f ≤ k) :
  FABL.fourierDegree
      (FABL.firstCoordinateSlice f b) ≤
    k

theorem FABL.fourierDegree_firstCoordinateSlice_one_le_pred_of_neg_one_eq_zero
  {n : ℕ} (f : FABL.SignCube (n + 1) → ℝ)
  {k : ℕ} (hk : 0 < k)
  (hdegree : FABL.fourierDegree f ≤ k)
  (hminus :
    FABL.firstCoordinateSlice f (-1) =
      0) :
  FABL.fourierDegree
      (FABL.firstCoordinateSlice f 1) ≤
    k - 1

theorem FABL.fourierDegree_firstCoordinateSlice_neg_one_le_pred_of_one_eq_zero
  {n : ℕ} (f : FABL.SignCube (n + 1) → ℝ)
  {k : ℕ} (hk : 0 < k)
  (hdegree : FABL.fourierDegree f ≤ k)
  (hplus :
    FABL.firstCoordinateSlice f 1 = 0) :
  FABL.fourierDegree
      (FABL.firstCoordinateSlice f (-1)) ≤
    k - 1

theorem FABL.degreeBound_pos_of_firstCoordinateSlice_one_ne_zero_of_neg_one_eq_zero
  {n : ℕ} (f : FABL.SignCube (n + 1) → ℝ)
  {k : ℕ}
  (hdegree : FABL.fourierDegree f ≤ k)
  (hplus :
    FABL.firstCoordinateSlice f 1 ≠ 0)
  (hminus :
    FABL.firstCoordinateSlice f (-1) =
      0) :
  0 < k

theorem FABL.degreeBound_pos_of_firstCoordinateSlice_neg_one_ne_zero_of_one_eq_zero
  {n : ℕ} (f : FABL.SignCube (n + 1) → ℝ)
  {k : ℕ}
  (hdegree : FABL.fourierDegree f ≤ k)
  (hminus :
    FABL.firstCoordinateSlice f (-1) ≠ 0)
  (hplus :
    FABL.firstCoordinateSlice f 1 = 0) :
  0 < k

theorem FABL.inv_two_pow_le_uniformProbability_ne_zero_of_fourierDegree_le
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (hf : f ≠ 0) {k : ℕ}
  (hdegree : FABL.fourierDegree f ≤ k) :
  2⁻¹ ^ k ≤
    FABL.uniformProbability fun x =>
      f x ≠ 0

theorem FABL.fourierDegree_discreteDerivative_le_pred
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (i : Fin n) {k : ℕ}
  (hdegree : FABL.fourierDegree f ≤ k) :
  FABL.fourierDegree
      ((FABL.discreteDerivative i) f) ≤
    k - 1

theorem FABL.booleanInfluence_eq_uniformProbability_discreteDerivative_ne_zero
  {n : ℕ} (f : FABL.BooleanFunction n)
  (i : Fin n) :
  FABL.booleanInfluence f i =
    FABL.uniformProbability fun x =>
      (FABL.discreteDerivative i) f.toReal
          x ≠
        0

theorem FABL.booleanInfluence_eq_zero_of_fourierDegree_le_zero
  {n : ℕ} (f : FABL.BooleanFunction n)
  (i : Fin n)
  (hdegree :
    FABL.fourierDegree f.toReal ≤ 0) :
  FABL.booleanInfluence f i = 0

theorem FABL.booleanInfluence_eq_zero_or_two_mul_inv_two_pow_le
  {n : ℕ} (f : FABL.BooleanFunction n)
  {k : ℕ}
  (hdegree :
    FABL.fourierDegree f.toReal ≤ k)
  (i : Fin n) :
  FABL.booleanInfluence f i = 0 ∨
    2 * 2⁻¹ ^ k ≤
      FABL.booleanInfluence f i

theorem FABL.totalInfluence_toReal_le_fourierDegree
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.totalInfluence f.toReal ≤
    ↑(FABL.fourierDegree f.toReal)

theorem FABL.isRelevant_of_fourierCoeff_ne_zero
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  {S : Finset (Fin n)} {i : Fin n}
  (hcoeff : FABL.fourierCoeff f S ≠ 0)
  (hiS : i ∈ S) : FABL.IsRelevant f i

theorem FABL.mem_relevantCoordinates {n : ℕ}
  (f : FABL.SignCube n → ℝ) (i : Fin n) :
  i ∈ FABL.relevantCoordinates f ↔
    FABL.IsRelevant f i

theorem FABL.dependsOn_relevantCoordinates {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  DependsOn f
    ↑(FABL.relevantCoordinates f)

theorem FABL.sum_influence_relevantCoordinates_eq_totalInfluence
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  ∑ i ∈ FABL.relevantCoordinates f,
      FABL.influence f i =
    FABL.totalInfluence f

theorem FABL.mul_card_relevantCoordinates_le_totalInfluence
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  {a : ℝ}
  (hlower :
    ∀ (i : Fin n),
      FABL.IsRelevant f i →
        a ≤ FABL.influence f i) :
  a * ↑(FABL.relevantCoordinates f).card ≤
    FABL.totalInfluence f

theorem FABL.isKJunta_of_card_relevantCoordinates_le
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  {r : ℕ}
  (hcard :
    (FABL.relevantCoordinates f).card ≤
      r) :
  FABL.IsKJunta f r

theorem FABL.dependsOn_toReal_iff {n : ℕ}
  (f : FABL.BooleanFunction n)
  (S : Set (Fin n)) :
  DependsOn f.toReal S ↔ DependsOn f S

theorem FABL.isKJunta_toReal_iff {n : ℕ}
  (f : FABL.BooleanFunction n) (r : ℕ) :
  FABL.IsKJunta f.toReal r ↔
    FABL.IsKJunta f r

theorem FABL.isKJunta_of_card_relevantCoordinates_toReal_le
  {n : ℕ} (f : FABL.BooleanFunction n)
  {r : ℕ}
  (hcard :
    (FABL.relevantCoordinates
          f.toReal).card ≤
      r) :
  FABL.IsKJunta f r

theorem FABL.relevantCoordinates_toReal_eq_empty_of_fourierDegree_eq_zero
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hdegree :
    FABL.fourierDegree f.toReal = 0) :
  FABL.relevantCoordinates f.toReal = ∅

theorem FABL.isKJunta_zero_of_fourierDegree_eq_zero
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hdegree :
    FABL.fourierDegree f.toReal = 0) :
  FABL.IsKJunta f 0

theorem FABL.isKJunta_mul_two_pow_pred_of_fourierDegree_le
  {n : ℕ} (f : FABL.BooleanFunction n)
  {k : ℕ}
  (hdegree :
    FABL.fourierDegree f.toReal ≤ k) :
  FABL.IsKJunta f (k * 2 ^ (k - 1))