theorem FABL.allZeroStringTester_acceptanceProbability
  {n : ℕ} [NeZero n] (w : Fin n → Bool) :
  FABL.NonadaptiveFunctionTester.acceptanceProbability
      (FABL.allZeroStringTester n) w =
    FABL.uniformProbability fun i =>
      w i = false

theorem FABL.allZeroStringTester_rejectionProbability
  {n : ℕ} [NeZero n] (w : Fin n → Bool) :
  FABL.NonadaptiveFunctionTester.rejectionProbability
      (FABL.allZeroStringTester n) w =
    FABL.uniformProbability fun i =>
      w i = true

theorem FABL.allZeroStringTester_isLocalTester
  {n : ℕ} [NeZero n] :
  FABL.IsLocalStringTester
    (FABL.allZeroStringTester n)
    FABL.IsAllZeroString 1

theorem FABL.allEqualStringTester_rejectionProbability
  {n : ℕ} [NeZero n] (w : Fin n → Bool) :
  FABL.NonadaptiveFunctionTester.rejectionProbability
      (FABL.allEqualStringTester n) w =
    Finset.univ.expect fun i =>
      Finset.univ.expect fun j =>
        if w i ≠ w j then 1 else 0

theorem FABL.allEqualStringTester_rejectionProbability_eq
  {n : ℕ} [NeZero n] (w : Fin n → Bool) :
  FABL.NonadaptiveFunctionTester.rejectionProbability
      (FABL.allEqualStringTester n) w =
    (2 *
        FABL.uniformProbability fun i =>
          w i = false) *
      FABL.uniformProbability fun i =>
        w i = true

theorem FABL.uniformProbability_bool_false_add_true
  {n : ℕ} [NeZero n] (w : Fin n → Bool) :
  ((FABL.uniformProbability fun i =>
        w i = false) +
      FABL.uniformProbability fun i =>
        w i = true) =
    1

theorem FABL.allEqualStringTester_isLocalTester
  {n : ℕ} [NeZero n] :
  FABL.IsLocalStringTester
    (FABL.allEqualStringTester n)
    FABL.IsAllEqualString 1

theorem FABL.IsPCPP.exists_close_of_acceptanceProbability_ge.{u}
  {Alphabet : Type u} [Fintype Alphabet]
  [DecidableEq Alphabet] {n ℓ r : ℕ}
  [NeZero n]
  {V : FABL.PCPPSystem Alphabet n ℓ r}
  {P : (Fin n → Alphabet) → Prop}
  {rate ε : ℝ} (hV : FABL.IsPCPP V P rate)
  (hε : ε ∈ Set.Icc 0 1)
  (w : Fin n → Alphabet)
  (proof : Fin ℓ → Alphabet)
  (haccept :
    1 - rate * ε ≤
      V.acceptanceProbability w proof) :
  FABL.IsCloseToProperty ε w P

theorem FABL.isPCPP_of_exists_close_of_acceptanceProbability_ge.{u}
  {Alphabet : Type u} [Fintype Alphabet]
  [DecidableEq Alphabet] {n ℓ r : ℕ}
  [NeZero n]
  (V : FABL.PCPPSystem Alphabet n ℓ r)
  (P : (Fin n → Alphabet) → Prop)
  (rate : ℝ) (hrate : 0 < rate)
  (hcomplete :
    ∀ (w : Fin n → Alphabet),
      P w →
        ∃ proof,
          V.acceptanceProbability w
              proof =
            1)
  (hclose :
    ∀ ε ∈ Set.Icc 0 1,
      ∀ (w : Fin n → Alphabet)
        (proof : Fin ℓ → Alphabet),
        1 - rate * ε ≤
            V.acceptanceProbability w
              proof →
          FABL.IsCloseToProperty ε w P) :
  FABL.IsPCPP V P rate

theorem FABL.oddWeightPartialSumPCPPSystem_rejectionProbability
  {m : ℕ} (w : Fin (m + 2) → Bool)
  (proof : Fin (m + 1) → Bool) :
  (FABL.oddWeightPartialSumPCPPSystem
          m).rejectionProbability
      w proof =
    FABL.uniformProbability fun seed =>
      ¬FABL.OddWeightPartialSumCheckHolds
          seed w proof

theorem FABL.oddWeightPartialSumProof_checks
  {m : ℕ} (w : Fin (m + 2) → Bool)
  (hw : FABL.IsOddWeightString w)
  (seed :
    FABL.OddWeightPartialSumCheckSeed m) :
  FABL.OddWeightPartialSumCheckHolds seed
    w (FABL.oddWeightPartialSumProof w)

theorem FABL.isOddWeightString_of_partialSumChecks
  {m : ℕ} (w : Fin (m + 2) → Bool)
  (proof : Fin (m + 1) → Bool)
  (hchecks :
    ∀
      (seed :
        FABL.OddWeightPartialSumCheckSeed
          m),
      FABL.OddWeightPartialSumCheckHolds
        seed w proof) :
  FABL.IsOddWeightString w

theorem FABL.oddWeightPartialSumPCPPSystem_isPCPP
  (m : ℕ) :
  FABL.IsPCPP
    (FABL.oddWeightPartialSumPCPPSystem m)
    FABL.IsOddWeightString 1

theorem FABL.boolTruthTableLiftTester_acceptanceProbability
  {r N : ℕ}
  (T :
    FABL.NonadaptiveFunctionTester
      (FABL.SignCube N) FABL.Sign r)
  (n : ℕ) (w : Fin n → Bool)
  (proof : Fin (2 ^ N) → Bool) :
  (FABL.boolTruthTableLiftTester T
          n).acceptanceProbability
      (FABL.inputProofWord w proof) =
    T.acceptanceProbability
      (FABL.pcppProofFunction proof)

theorem FABL.subsetIndicatorSign_coordinateTrueIndexSet
  (n : ℕ) (j : Fin n) :
  FABL.subsetIndicatorSign
      (FABL.coordinateTrueIndexSet n j) =
    FABL.coordinateTruthTable n j

theorem FABL.coordinateLocalCorrection_correctProbability_ge
  {n : ℕ}
  (f : FABL.BooleanFunction (2 ^ n))
  (j : Fin n) (i : Fin (2 ^ n)) (δ : ℝ)
  (hclose :
    FABL.relativeHammingDist f
        (FABL.dictator i) ≤
      δ) :
  1 - 2 * δ ≤
    FABL.uniformProbability fun y =>
      FABL.localCorrection
          (fun z =>
            f
              ((FABL.binaryCubeSignEquiv
                  (2 ^ n))
                z))
          ((FABL.binaryCubeSignEquiv
                (2 ^ n)).symm
            (FABL.coordinateTruthTable n
              j))
          y =
        FABL.pcppBoolSignEquiv
          ((FABL.booleanStringIndexEquiv
                n).symm
            i j)

theorem FABL.coordinateConsistencyFunctionTester_acceptanceProbability
  {n : ℕ} [NeZero n] (w : Fin n → Bool)
  (proof : Fin (2 ^ 2 ^ n) → Bool) :
  (FABL.coordinateConsistencyFunctionTester
          n).acceptanceProbability
      (FABL.inputProofWord w proof) =
    Finset.univ.expect fun j =>
      FABL.coordinateCorrectionProbability
        (FABL.pcppProofFunction proof) j
        (w j)

theorem FABL.coordinateLocalCorrection_dictator
  {n : ℕ} (w : Fin n → Bool) (j : Fin n)
  (y : FABL.F₂Cube (2 ^ n)) :
  FABL.localCorrection
      (fun z =>
        FABL.dictator
          ((FABL.booleanStringIndexEquiv
              n)
            w)
          ((FABL.binaryCubeSignEquiv
              (2 ^ n))
            z))
      ((FABL.binaryCubeSignEquiv
            (2 ^ n)).symm
        (FABL.coordinateTruthTable n j))
      y =
    FABL.pcppBoolSignEquiv (w j)

theorem FABL.arbitraryPropertyPCPPSystem_acceptanceProbability
  {n : ℕ} (P : (Fin n → Bool) → Prop)
  [NeZero n] (w : Fin n → Bool)
  (proof : Fin (2 ^ 2 ^ n) → Bool) :
  (FABL.arbitraryPropertyPCPPSystem
          P).acceptanceProbability
      w proof =
    ((FABL.propertyTruthTableFunctionTester
              P).acceptanceProbability
          (FABL.inputProofWord w proof) +
        (FABL.coordinateConsistencyFunctionTester
              n).acceptanceProbability
          (FABL.inputProofWord w proof)) /
      2

theorem FABL.arbitraryPropertyPCPPSystem_complete
  {n : ℕ} (P : (Fin n → Bool) → Prop)
  [NeZero n] (w : Fin n → Bool)
  (hw : P w) :
  (FABL.arbitraryPropertyPCPPSystem
          P).acceptanceProbability
      w
      (FABL.encodeBooleanFunctionProof
        (FABL.dictator
          ((FABL.booleanStringIndexEquiv
              n)
            w))) =
    1