theorem FABL.IsLocalTester.close_of_acceptanceProbability_ge.{u_1,
    u_2}
  {Ω : Type u_1} {β : Type u_2}
  [Fintype Ω] [Nonempty Ω] [DecidableEq β]
  {r : ℕ}
  {T :
    FABL.NonadaptiveFunctionTester Ω β r}
  {P : (Ω → β) → Prop} {rate ε : ℝ}
  (hT : FABL.IsLocalTester T P rate)
  (hε : ε ∈ Set.Icc 0 1) (f : Ω → β)
  (haccept :
    1 - rate * ε ≤
      T.acceptanceProbability f) :
  FABL.IsCloseToProperty ε f P

theorem FABL.isLocalTester_of_close_of_acceptanceProbability_ge.{u_1,
    u_2}
  {Ω : Type u_1} {β : Type u_2}
  [Fintype Ω] [Nonempty Ω] [DecidableEq β]
  {r : ℕ}
  (T :
    FABL.NonadaptiveFunctionTester Ω β r)
  (P : (Ω → β) → Prop) (rate : ℝ)
  (hrate : 0 < rate)
  (hcomplete :
    ∀ (f : Ω → β),
      P f → T.acceptanceProbability f = 1)
  (hclose :
    ∀ ε ∈ Set.Icc 0 1,
      ∀ (f : Ω → β),
        1 - rate * ε ≤
            T.acceptanceProbability f →
          FABL.IsCloseToProperty ε f P) :
  FABL.IsLocalTester T P rate

theorem FABL.blrFunctionTester_acceptanceProbability
  {n : ℕ} (f : FABL.F₂Cube n → FABL.𝔽₂) :
  (FABL.blrFunctionTester
          n).acceptanceProbability
      f =
    FABL.blrAcceptanceProbability f

theorem FABL.blrFunctionTester_complete {n : ℕ}
  (f : FABL.F₂Cube n → FABL.𝔽₂)
  (hf : FABL.IsF₂Linear f) :
  (FABL.blrFunctionTester
          n).acceptanceProbability
      f =
    1

theorem FABL.blrFunctionTester_isLocalTester
  {n : ℕ} :
  FABL.IsLocalTester
    (FABL.blrFunctionTester n)
    FABL.IsF₂Linear 1

theorem FABL.andFunctionTester_acceptanceProbability.{u,
    v}
  {Domain : Type u} {Codomain : Type v}
  {r s : ℕ}
  (T :
    FABL.NonadaptiveFunctionTester Domain
      Codomain r)
  (U :
    FABL.NonadaptiveFunctionTester Domain
      Codomain s)
  (f : Domain → Codomain) :
  (FABL.andFunctionTester T
          U).acceptanceProbability
      f =
    T.acceptanceProbability f *
      U.acceptanceProbability f

theorem FABL.naeFunctionTester_acceptanceProbability
  {n : ℕ} (f : FABL.BooleanFunction n) :
  (FABL.naeFunctionTester
          n).acceptanceProbability
      f =
    FABL.condorcetWinnerProbability f

theorem FABL.naeFunctionTester_complete_signedDictator
  {n : ℕ} (i : Fin n) (negated : Bool) :
  (FABL.naeFunctionTester
          n).acceptanceProbability
      (FABL.signedDictator i negated) =
    1

theorem FABL.naeTest_levelOneWeight_ge {n : ℕ}
  (f : FABL.BooleanFunction n) (ε : ℝ)
  (haccept :
    (FABL.naeFunctionTester
            n).acceptanceProbability
        f =
      1 - ε) :
  1 - 9 / 2 * ε ≤
    FABL.fourierWeightAtLevel 1 f.toReal

theorem FABL.naeTest_close_to_signedDictator
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hn : 0 < n) (ε : ℝ) (hε₀ : 0 ≤ ε)
  (haccept :
    (FABL.naeFunctionTester
            n).acceptanceProbability
        f =
      1 - ε) :
  ∃ i negated,
    FABL.relativeHammingDist f
        (FABL.signedDictator i negated) ≤
      7205 * ε

theorem FABL.fourierWeightAtLevel_one_add_coeff_sq_le_one_of_card_ne_one
  {n : ℕ} (f : FABL.BooleanFunction n)
  (S : Finset (Fin n))
  (hcard : S.card ≠ 1) :
  FABL.fourierWeightAtLevel 1 f.toReal +
      FABL.fourierCoeff f.toReal S ^ 2 ≤
    1

theorem FABL.exists_dictator_close_of_signBlr_and_nae_acceptance_ge
  {n : ℕ} (f : FABL.BooleanFunction n)
  (ε : ℝ) (hε : ε ∈ Set.Icc 0 1)
  (hblr :
    1 - 1 / 10 * ε ≤
      (FABL.signBlrFunctionTester
            n).acceptanceProbability
        f)
  (hnae :
    1 - 1 / 10 * ε ≤
      (FABL.naeFunctionTester
            n).acceptanceProbability
        f) :
  ∃ i,
    FABL.relativeHammingDist f
        (FABL.dictator i) ≤
      ε

theorem FABL.blrAndNae_isLocalTester {n : ℕ} :
  FABL.IsLocalTester
    (FABL.andFunctionTester
      (FABL.signBlrFunctionTester n)
      (FABL.naeFunctionTester n))
    FABL.IsDictator (1 / 10)

theorem FABL.blrNae_isLocalTester {n : ℕ} :
  FABL.IsLocalTester
    (FABL.blrNaeFunctionTester n)
    FABL.IsDictator (1 / 20)

theorem FABL.uniformMixtureFunctionTester_acceptanceProbability.{u,
    v}
  {Domain : Type u} {Codomain : Type v}
  {r t : ℕ} (ht : 0 < t)
  (T :
    Fin t →
      FABL.NonadaptiveFunctionTester
        Domain Codomain r)
  (f : Domain → Codomain) :
  (FABL.uniformMixtureFunctionTester ht
          T).acceptanceProbability
      f =
    Finset.univ.expect fun i =>
      (T i).acceptanceProbability f

theorem FABL.component_acceptanceProbability_ge_of_uniformMixture_ge.{u,
    v}
  {Domain : Type u} {Codomain : Type v}
  {r t : ℕ} (ht : 0 < t)
  (T :
    Fin t →
      FABL.NonadaptiveFunctionTester
        Domain Codomain r)
  (f : Domain → Codomain) (rate ε : ℝ)
  (haccept :
    1 - rate / ↑t * ε ≤
      (FABL.uniformMixtureFunctionTester
            ht T).acceptanceProbability
        f)
  (i : Fin t) :
  1 - rate * ε ≤
    (T i).acceptanceProbability f

theorem FABL.subsetLocalCorrectionFunctionTester_dictator
  {n : ℕ} (S : Finset (Fin n))
  (i : Fin n) :
  (FABL.subsetLocalCorrectionFunctionTester
          S).acceptanceProbability
      (FABL.dictator i) =
    if i ∈ S then 1 else 0

theorem FABL.subsetLocalCorrection_correctProbability_ge
  {n : ℕ} (S A : Finset (Fin n))
  (f : FABL.BooleanFunction n) (δ : ℝ)
  (hclose :
    FABL.relativeHammingDist f
        (FABL.parityFunction A) ≤
      δ) :
  1 - 2 * δ ≤
    FABL.uniformProbability fun y =>
      FABL.localCorrection
          (fun z =>
            f
              ((FABL.binaryCubeSignEquiv
                  n)
                z))
          ((FABL.binaryCubeSignEquiv
                n).symm
            (FABL.subsetIndicatorSign S))
          y =
        FABL.parityFunction A
          (FABL.subsetIndicatorSign S)

theorem FABL.subsetLocalCorrectionFunctionTester_acceptanceProbability
  {n : ℕ} (S : Finset (Fin n))
  (f : FABL.BooleanFunction n) :
  (FABL.subsetLocalCorrectionFunctionTester
          S).acceptanceProbability
      f =
    FABL.uniformProbability fun y =>
      FABL.localCorrection
          (fun z =>
            f
              ((FABL.binaryCubeSignEquiv
                  n)
                z))
          ((FABL.binaryCubeSignEquiv
                n).symm
            (FABL.subsetIndicatorSign S))
          y =
        -1

theorem FABL.dictatorSubclass_isLocalTester
  {n : ℕ} (S : Finset (Fin n)) :
  FABL.IsLocalTester
    (FABL.dictatorSubclassFunctionTester
      S)
    (FABL.IsDictatorIn S) (1 / 100)