theorem FABL.deltaRandomSubsetWeight_nonneg
  (n : ℕ) {δ : ℝ} (hδ0 : 0 ≤ δ)
  (hδ1 : δ ≤ 1) (J : Finset (Fin n)) :
  0 ≤ FABL.deltaRandomSubsetWeight n δ J

theorem FABL.sum_deltaRandomSubsetWeight (n : ℕ)
  (δ : ℝ) :
  ∑ J,
      FABL.deltaRandomSubsetWeight n δ J =
    1

theorem FABL.sum_coordRestrictionWeight :
  ∑ c, FABL.coordRestrictionWeight c = 1

theorem FABL.sum_restrictionAssignmentWeight
  {n : ℕ} :
  ∑ ρ,
      FABL.restrictionAssignmentWeight ρ =
    1

theorem FABL.extendedSignRestriction_apply.{u_1}
  {n : ℕ} {α : Type u_1}
  (f : FABL.SignCube n → α)
  (J : Finset (Fin n))
  (z : FABL.FixedSignCube J)
  (x : FABL.SignCube n) :
  FABL.extendedSignRestriction f J z x =
    f
      (FABL.combineSignCube J
        (fun i => x ↑i) z)

theorem FABL.extendedSignRestriction_setCoordinate_of_not_mem.{u_1}
  {n : ℕ} {α : Type u_1}
  (f : FABL.SignCube n → α)
  (J : Finset (Fin n))
  (z : FABL.FixedSignCube J) (i : Fin n)
  (hi : i ∉ J) (x : FABL.SignCube n)
  (b : FABL.Sign) :
  FABL.extendedSignRestriction f J z
      (FABL.setCoordinate x i b) =
    FABL.extendedSignRestriction f J z x

theorem FABL.expect_fourierCoeff_empty_randomRestriction
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (δ : ℝ) :
  (FABL.expectRandomRestriction n δ
      fun J z =>
      FABL.restrictionFourierCoeff f J ∅
        z) =
    FABL.fourierCoeff f ∅

theorem FABL.sum_deltaRandomSubsetWeight_supset
  (n : ℕ) (δ : ℝ) (S : Finset (Fin n)) :
  (∑ J,
      if S ⊆ J then
        FABL.deltaRandomSubsetWeight n δ J
      else 0) =
    δ ^ S.card

theorem FABL.ambientRestrictionFourierCoeff_eq
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J S : Finset (Fin n))
  (z : FABL.FixedSignCube J) :
  FABL.ambientRestrictionFourierCoeff f J
      S z =
    if S ⊆ J then
      FABL.restrictionFourierCoeff f J
        (FABL.freeFrequencyPart J S) z
    else 0

theorem FABL.expect_ambientRestrictionFourierCoeff
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J S : Finset (Fin n)) :
  (Finset.univ.expect fun z =>
      FABL.ambientRestrictionFourierCoeff
        f J S z) =
    (if S ⊆ J then 1 else 0) *
      FABL.fourierCoeff f S

theorem FABL.expect_fourierCoeff_randomRestriction
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (δ : ℝ) (S : Finset (Fin n)) :
  (FABL.expectRandomRestriction n δ
      fun J z =>
      FABL.ambientRestrictionFourierCoeff
        f J S z) =
    δ ^ S.card * FABL.fourierCoeff f S

theorem FABL.liftFreeFrequency_freeFrequencyPart_of_subset
  {n : ℕ} {J S : Finset (Fin n)}
  (hS : S ⊆ J) :
  FABL.liftFreeFrequency
      (FABL.freeFrequencyPart J S) =
    S

theorem FABL.expect_sq_ambientRestrictionFourierCoeff
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J S : Finset (Fin n)) :
  (Finset.univ.expect fun z =>
      FABL.ambientRestrictionFourierCoeff
          f J S z ^
        2) =
    if S ⊆ J then
      ∑ T,
        FABL.fourierCoeff f
            (FABL.liftFreeFrequency
                (FABL.freeFrequencyPart J
                  S) ∪
              FABL.liftFixedFrequency T) ^
          2
    else 0

theorem FABL.subset_of_inter_eq {n : ℕ}
  {S U J : Finset (Fin n)}
  (h : U ∩ J = S) : S ⊆ J

theorem FABL.subset_of_inter_eq_left {n : ℕ}
  {S U J : Finset (Fin n)}
  (h : U ∩ J = S) : S ⊆ U

theorem FABL.sum_deltaRandomSubsetWeight_inter_eq
  (n : ℕ) (δ : ℝ) (S U : Finset (Fin n)) :
  (∑ J,
      if U ∩ J = S then
        FABL.deltaRandomSubsetWeight n δ J
      else 0) =
    if S ⊆ U then
      δ ^ S.card * (1 - δ) ^ (U \ S).card
    else 0

theorem FABL.sum_sq_fourier_of_inter_eq {n : ℕ}
  (f : FABL.SignCube n → ℝ)
  (J S : Finset (Fin n)) (hS : S ⊆ J) :
  ∑ T,
      FABL.fourierCoeff f
          (FABL.liftFreeFrequency
              (FABL.freeFrequencyPart J
                S) ∪
            FABL.liftFixedFrequency T) ^
        2 =
    ∑ U,
      if U ∩ J = S then
        FABL.fourierCoeff f U ^ 2
      else 0

theorem FABL.expect_sq_fourierCoeff_randomRestriction
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (δ : ℝ) (S : Finset (Fin n)) :
  (FABL.expectRandomRestriction n δ
      fun J z =>
      FABL.ambientRestrictionFourierCoeff
          f J S z ^
        2) =
    ∑ U,
      (if S ⊆ U then
          δ ^ S.card *
            (1 - δ) ^ (U \ S).card
        else 0) *
        FABL.fourierCoeff f U ^ 2

theorem FABL.sum_deltaRandomSubsetWeight_mem
  (n : ℕ) (δ : ℝ) (i : Fin n) :
  (∑ J,
      if i ∈ J then
        FABL.deltaRandomSubsetWeight n δ J
      else 0) =
    δ

theorem FABL.discreteDerivative_extendedSignRestriction_of_mem
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n))
  (z : FABL.FixedSignCube J) (i : Fin n)
  (hi : i ∈ J) (x : FABL.SignCube n) :
  (FABL.discreteDerivative i)
      (FABL.extendedSignRestriction f J z)
      x =
    (FABL.discreteDerivative i) f
      (FABL.combineSignCube J
        (fun j => x ↑j) z)

theorem FABL.expect_sq_discreteDerivative_combine
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (i : Fin n)
  (z : FABL.FixedSignCube J) :
  (Finset.univ.expect fun x =>
      (FABL.discreteDerivative i) f
          (FABL.combineSignCube J
            (FABL.freePart J x) z) ^
        2) =
    Finset.univ.expect fun y =>
      (FABL.discreteDerivative i) f
          (FABL.combineSignCube J y z) ^
        2

theorem FABL.expect_sq_discreteDerivative_product
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (i : Fin n) :
  (Finset.univ.expect fun y =>
      Finset.univ.expect fun z =>
        (FABL.discreteDerivative i) f
            (FABL.combineSignCube J y z) ^
          2) =
    FABL.influence f i

theorem FABL.expect_influence_extendedSignRestriction_of_mem
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (i : Fin n)
  (hi : i ∈ J) :
  (Finset.univ.expect fun z =>
      FABL.influence
        (FABL.extendedSignRestriction f J
          z)
        i) =
    FABL.influence f i

theorem FABL.expect_influence_extended_randomRestriction
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (δ : ℝ) (i : Fin n) :
  (FABL.expectRandomRestriction n δ
      fun J z =>
      FABL.influence
        (FABL.extendedSignRestriction f J
          z)
        i) =
    δ * FABL.influence f i

theorem FABL.expect_totalInfluence_extended_randomRestriction
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (δ : ℝ) :
  (FABL.expectRandomRestriction n δ
      fun J z =>
      FABL.totalInfluence
        (FABL.extendedSignRestriction f J
          z)) =
    δ * FABL.totalInfluence f

theorem FABL.literal_not_falsified_local_weight
  {n : ℕ} (ℓ : FABL.Literal n) :
  (∑ c,
      FABL.coordRestrictionWeight c *
        if
            (ℓ.isFalsified fun x => c) =
              true then
          0
        else 1) =
    3 / 4

theorem FABL.term_not_falsified_weight {n : ℕ}
  (T : FABL.DNFTerm n) :
  (∑ ρ,
      FABL.restrictionAssignmentWeight ρ *
        if T.notFalsified ρ = true then 1
        else 0) =
    (3 / 4) ^ T.width

theorem FABL.restrictedWidth_ge_probability_le
  {n : ℕ} (T : FABL.DNFTerm n) (w : ℕ) :
  (∑ ρ,
      FABL.restrictionAssignmentWeight ρ *
        if w ≤ T.restrictedWidthOf ρ then
          1
        else 0) ≤
    (3 / 4) ^ w

theorem FABL.sum_inverse_two_pow_succ_Ico_le
  (m n : ℕ) :
  ∑ k ∈ Finset.Ico m n, (2 ^ (k + 1))⁻¹ ≤
    (2 ^ m)⁻¹

theorem FABL.DNFFormula.selectedTerm_mem {n : ℕ}
  (φ : FABL.DNFFormula n)
  (x : FABL.SignCube n)
  (hx : φ.eval x = -1) :
  φ.selectedTerm x ∈ φ.terms

theorem FABL.DNFFormula.selectedTerm_eval {n : ℕ}
  (φ : FABL.DNFFormula n)
  (x : FABL.SignCube n)
  (hx : φ.eval x = -1) :
  (φ.selectedTerm x).eval x = -1

theorem FABL.DNFFormula.selectedWidth_eq_zero_of_eval_ne
  {n : ℕ} (φ : FABL.DNFFormula n)
  (x : FABL.SignCube n)
  (hx : φ.eval x ≠ -1) :
  φ.selectedWidth x = 0

theorem FABL.DNFFormula.selectedWidth_le_dimension
  {n : ℕ} (φ : FABL.DNFFormula n)
  (x : FABL.SignCube n) :
  φ.selectedWidth x ≤ n

theorem FABL.card_negOnePivotal_le_selectedWidth
  {n : ℕ} (φ : FABL.DNFFormula n)
  (x : FABL.SignCube n) :
  {i |
        FABL.IsNegOnePivotal
          φ.toBooleanFunction i x}.card ≤
    φ.selectedWidth x

theorem FABL.selectedWidth_tail_probability_le
  {n : ℕ} (φ : FABL.DNFFormula n) (k : ℕ)
  (hk : 0 < k) :
  (FABL.uniformProbability fun x =>
      k ≤ φ.selectedWidth x) ≤
    ↑φ.size * (2 ^ k)⁻¹

theorem FABL.uniformProbability_le_one.{u_1}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  (P : Ω → Prop) [DecidablePred P] :
  FABL.uniformProbability P ≤ 1

theorem FABL.expect_selectedWidth_eq_sum_tail
  {n : ℕ} (φ : FABL.DNFFormula n) :
  (Finset.univ.expect fun x =>
      ↑(φ.selectedWidth x)) =
    ∑ k ∈ Finset.range n,
      FABL.uniformProbability fun x =>
        k + 1 ≤ φ.selectedWidth x