theorem FABL.repeatAndFunctionTester_acceptanceProbability.{u,
    v}
  {Domain : Type u} {Codomain : Type v}
  {r k : ℕ}
  (T :
    FABL.NonadaptiveFunctionTester Domain
      Codomain r)
  (f : Domain → Codomain) :
  (FABL.repeatAndFunctionTester T
          k).acceptanceProbability
      f =
    T.acceptanceProbability f ^ k

theorem FABL.amplificationRepetitions_queryBound
  {rate ε δ : ℝ} (hrate : 0 < rate)
  (hε : 0 < ε)
  (hδ : δ ∈ Set.Ioc 0 (1 / 2)) (r : ℕ) :
  ↑(FABL.amplificationRepetitions rate ε
          δ *
        r) ≤
    (Real.log (1 / δ) / (rate * ε) + 1) *
      ↑r

theorem FABL.repeatAndFunctionTester_amplifies.{u,
    v}
  {Domain : Type u} {Codomain : Type v}
  [Fintype Domain] [Nonempty Domain]
  [DecidableEq Codomain] {r : ℕ}
  (T :
    FABL.NonadaptiveFunctionTester Domain
      Codomain r)
  (P : (Domain → Codomain) → Prop)
  {rate ε δ : ℝ}
  (hT : FABL.IsLocalTester T P rate)
  (hε : ε ∈ Set.Ioc 0 (1 / 2))
  (hδ : δ ∈ Set.Ioc 0 (1 / 2)) :
  (∀ (f : Domain → Codomain),
      P f →
        (FABL.repeatAndFunctionTester T
                (FABL.amplificationRepetitions
                  rate ε
                  δ)).acceptanceProbability
            f =
          1) ∧
    ∀ (f : Domain → Codomain),
      (∀ (g : Domain → Codomain),
          P g → FABL.IsFar ε f g) →
        (FABL.repeatAndFunctionTester T
                (FABL.amplificationRepetitions
                  rate ε
                  δ)).acceptanceProbability
            f ≤
          δ

theorem FABL.equalityPairStringTester_rejectionProbability
  {n : ℕ} [NeZero n]
  (w : Fin (n * 2) → Bool) :
  FABL.NonadaptiveFunctionTester.rejectionProbability
      (FABL.equalityPairStringTester n)
      w =
    FABL.uniformProbability fun i =>
      w (FABL.equalityPairIndex i 0) ≠
        w (FABL.equalityPairIndex i 1)

theorem FABL.two_mul_relativeHammingDist_equalityPairRepair
  {n : ℕ} [NeZero n]
  (w : Fin (n * 2) → Bool) :
  2 *
      FABL.relativeHammingDist w
        (FABL.equalityPairRepair w) =
    FABL.uniformProbability fun i =>
      w (FABL.equalityPairIndex i 0) ≠
        w (FABL.equalityPairIndex i 1)

theorem FABL.equalityPairStringTester_isLocalTester
  {n : ℕ} [NeZero n] :
  FABL.IsLocalStringTester
    (FABL.equalityPairStringTester n)
    FABL.IsEqualPairString 1

theorem FABL.oddWeightShortProofPCPPSystem_acceptanceProbability
  {m : ℕ} (w : Fin (m + 2) → Bool)
  (proof : Fin m → Bool) :
  (FABL.oddWeightShortProofPCPPSystem
          m).acceptanceProbability
      w proof =
    (FABL.oddWeightPartialSumPCPPSystem
          m).acceptanceProbability
      w
      (FABL.extendProofWithFinalTrue
        proof)

theorem FABL.oddWeightShortProofPCPPSystem_rejectionProbability
  {m : ℕ} (w : Fin (m + 2) → Bool)
  (proof : Fin m → Bool) :
  (FABL.oddWeightShortProofPCPPSystem
          m).rejectionProbability
      w proof =
    (FABL.oddWeightPartialSumPCPPSystem
          m).rejectionProbability
      w
      (FABL.extendProofWithFinalTrue
        proof)

theorem FABL.oddWeightShortProofPCPPSystem_isPCPP
  (m : ℕ) :
  FABL.IsPCPP
    (FABL.oddWeightShortProofPCPPSystem m)
    FABL.IsOddWeightString 1

theorem FABL.allEqualStringTester_rejectionProbability_eq_distanceFormula
  {n : ℕ} [NeZero n] (w : Fin n → Bool) :
  FABL.NonadaptiveFunctionTester.rejectionProbability
      (FABL.allEqualStringTester n) w =
    1 / 2 -
      1 / 2 *
        (1 -
            2 *
              FABL.allEqualStringDistance
                w) ^
          2

theorem FABL.allEqualStringDistance_le_rejectionProbability
  {n : ℕ} [NeZero n] (w : Fin n → Bool) :
  FABL.allEqualStringDistance w ≤
    FABL.NonadaptiveFunctionTester.rejectionProbability
      (FABL.allEqualStringTester n) w

theorem FABL.oddWeightString_no_localTester_of_queries_lt
  {n r : ℕ} [NeZero n]
  (T :
    FABL.NonadaptiveStringTester Bool n r)
  (hr : r < n) (rate : ℝ) :
  ¬FABL.IsLocalStringTester T
      FABL.IsOddWeightString rate

theorem FABL.twoQueryTester_accepts_embeddedOddMajority
  {n : ℕ}
  (T :
    FABL.NonadaptiveFunctionTester
      (FABL.SignCube n) FABL.Sign 2)
  (hcomplete :
    ∀ (i : Fin n),
      T.acceptanceProbability
          (FABL.dictator i) =
        1)
  {d : ℕ} (hd : Odd d) (h : d ≤ n) :
  T.acceptanceProbability
      (FABL.embeddedMajority d n h) =
    1

theorem FABL.no_maxE3Lin_dictatorVsNoNotables_of_perfectCompleteness
  (alpha : ℝ) (halpha : alpha < 1) :
  ¬∃ error T,
      FABL.IsDictatorVsNoNotablesTest
        FABL.maxE3LinPredicates alpha 1
        error T

theorem FABL.signAndFunctionTester_acceptanceProbability
  {n : ℕ} (f : FABL.BooleanFunction n) :
  (FABL.signAndFunctionTester
          n).acceptanceProbability
      f =
    Finset.univ.expect fun x =>
      Finset.univ.expect fun y =>
        if
            FABL.signAnd (f x) (f y) =
              f
                (FABL.signCubeAnd x
                  y) then
          1
        else 0

theorem FABL.signAndFunctionTester_parity_acceptanceProbability
  {n : ℕ} (S : Finset (Fin n)) :
  (FABL.signAndFunctionTester
          n).acceptanceProbability
      (FABL.parityFunction S) =
    FABL.parityAndAcceptanceProbability
      S.card

theorem FABL.pcppBoolSignEquiv_boolAnd
  (a b : Bool) :
  FABL.pcppBoolSignEquiv (a && b) =
    FABL.signAnd
      (FABL.pcppBoolSignEquiv a)
      (FABL.pcppBoolSignEquiv b)

theorem FABL.pcppBoolCubeSignEquiv_boolCubeAnd
  {n : ℕ} (x y : Fin n → Bool) :
  (FABL.pcppBoolCubeSignEquiv n)
      (FABL.boolCubeAnd x y) =
    FABL.signCubeAnd
      ((FABL.pcppBoolCubeSignEquiv n) x)
      ((FABL.pcppBoolCubeSignEquiv n) y)

theorem FABL.boolAndFunctionTester_acceptanceProbability
  {n : ℕ} (f : (Fin n → Bool) → Bool) :
  (FABL.boolAndFunctionTester
          n).acceptanceProbability
      f =
    Finset.univ.expect fun x =>
      Finset.univ.expect fun y =>
        if
            (f x && f y) =
              f
                (FABL.boolCubeAnd x
                  y) then
          1
        else 0

theorem FABL.boolAndFunctionTester_parity_acceptanceProbability
  {n : ℕ} (S : Finset (Fin n)) :
  (FABL.boolAndFunctionTester
          n).acceptanceProbability
      (FABL.boolParityFunction S) =
    FABL.parityAndAcceptanceProbability
      S.card

theorem FABL.parityAndAcceptanceProbability_zero :
  FABL.parityAndAcceptanceProbability 0 =
    1

theorem FABL.parityAndAcceptanceProbability_one :
  FABL.parityAndAcceptanceProbability 1 =
    1

theorem FABL.parityAndAcceptanceProbability_le_twoPowInv
  {k : ℕ} (_hk : 2 ≤ k) :
  FABL.parityAndAcceptanceProbability k ≤
    1 / 2 + (2 ^ k)⁻¹

theorem FABL.oddBLREquationFunctionTester_acceptanceProbability
  {n : ℕ} (f : FABL.BooleanFunction n) :
  (FABL.oddBLREquationFunctionTester
          n).acceptanceProbability
      f =
    Finset.univ.expect fun x =>
      Finset.univ.expect fun y =>
        Finset.univ.expect fun b =>
          if
              f x * f y *
                  f
                    (FABL.scaledPointwiseProduct
                      b x y) =
                b then
            1
          else 0

theorem FABL.oddBLREquationFunctionTester_eq_oddBLRAcceptanceProbability
  {n : ℕ} (f : FABL.BooleanFunction n) :
  (FABL.oddBLREquationFunctionTester
          n).acceptanceProbability
      f =
    FABL.oddBLRAcceptanceProbability
      (FABL.BoundedCubeFunction.ofBoolean
        f)

theorem FABL.oddBLRAcceptanceProbability_eq_one_iff_oddParity
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.oddBLRAcceptanceProbability
        (FABL.BoundedCubeFunction.ofBoolean
          f) =
      1 ↔
    ∃ S,
      Odd S.card ∧
        f = FABL.parityFunction S

theorem FABL.oddBLRAndAndFunctionTester_acceptanceProbability_eq_one_iff
  {n : ℕ} (f : FABL.BooleanFunction n) :
  (FABL.oddBLRAndAndFunctionTester
            n).acceptanceProbability
        f =
      1 ↔
    FABL.IsDictator f

theorem FABL.nonDictatorBooleanFunctions_nonempty
  (n : ℕ) :
  (FABL.nonDictatorBooleanFunctions
      n).Nonempty

theorem FABL.oddBLRAndAndRejectionValues_nonempty
  (n : ℕ) :
  (FABL.oddBLRAndAndRejectionValues
      n).Nonempty

theorem FABL.oddBLRAndAndRejectionGap_pos
  (n : ℕ) :
  0 < FABL.oddBLRAndAndRejectionGap n

theorem FABL.oddBLRAndAnd_isLocalTester {n : ℕ} :
  FABL.IsLocalTester
    (FABL.oddBLRAndAndFunctionTester n)
    FABL.IsDictator
    (FABL.oddBLRAndAndRejectionGap n / 2)

theorem FABL.PolytimeMap.IsThresholdApproximation.distinguishesGap
  {algorithm : FABL.PolytimeMap}
  {problem :
    FABL.EncodedMaximizationProblem}
  {outputThreshold optimumThreshold
    soundness completeness : ℚ}
  (happrox :
    algorithm.IsThresholdApproximation
      problem outputThreshold
      optimumThreshold)
  (thresholdTest :
    algorithm.ValueThresholdTest problem
      outputThreshold)
  (hgap : soundness < completeness)
  (hsoundness :
    soundness < outputThreshold)
  (hcompleteness :
    optimumThreshold ≤ completeness) :
  thresholdTest.decision.DistinguishesPromise
    (problem.gapPromise soundness
      completeness hgap)