theorem FABL.RandomizedDecisionTree.sum_queryProbabilityOnInput_eq_inputCost.{u_1,
    u_2}
  {Ω : Type u_1} {α : Type u_2} {n : ℕ}
  {f : (Fin n → Ω) → α}
  (T :
    FABL.RandomizedDecisionTree Ω α n f)
  (x : Fin n → Ω) :
  ∑ i, T.queryProbabilityOnInput i x =
    T.inputCost x

theorem FABL.RandomizedDecisionTree.sum_queryProbability_eq_averageCost.{u_1,
    u_2}
  {Ω : Type u_1} {α : Type u_2} {n : ℕ}
  {f : (Fin n → Ω) → α} [Fintype Ω]
  (T :
    FABL.RandomizedDecisionTree Ω α n f)
  (π : PMF Ω) :
  ∑ i, T.queryProbability π i =
    T.averageCost π

theorem FABL.RandomizedDecisionTree.averageCost_le_worstCaseCost.{u_1,
    u_2}
  {Ω : Type u_1} {α : Type u_2} {n : ℕ}
  {f : (Fin n → Ω) → α} [Fintype Ω]
  [Nonempty Ω]
  (T :
    FABL.RandomizedDecisionTree Ω α n f)
  (π : PMF Ω) :
  T.averageCost π ≤ T.worstCaseCost

theorem FABL.RandomizedDecisionTree.averageCost_eq_seedExpectation.{u_1,
    u_2}
  {Ω : Type u_1} {α : Type u_2} {n : ℕ}
  {f : (Fin n → Ω) → α} [Fintype Ω]
  (T :
    FABL.RandomizedDecisionTree Ω α n f)
  (π : PMF Ω) :
  T.averageCost π =
    FABL.pmfExpectation T.seedLaw
      fun seed =>
      FABL.RandomizedDecisionTree.deterministicAverageCost
        π (T.tree seed)

theorem FABL.RandomizedDecisionTree.exists_deterministic_averageCost_le.{u_1,
    u_2}
  {Ω : Type u_1} {α : Type u_2} {n : ℕ}
  {f : (Fin n → Ω) → α} [Fintype Ω]
  (T :
    FABL.RandomizedDecisionTree Ω α n f)
  (π : PMF Ω) :
  ∃ seed,
    FABL.RandomizedDecisionTree.deterministicAverageCost
        π (T.tree seed) ≤
      T.averageCost π

theorem FABL.majorityThreeRandomizedTree_inputCost
  (x : FABL.SignCube 3) :
  FABL.majorityThreeRandomizedTree.inputCost
      x =
    (((if x 0 = x 1 then 2 else 3) +
          if x 0 = x 2 then 2 else 3) +
        if x 1 = x 2 then 2 else 3) /
      3

theorem FABL.majorityThreeRandomizedTree_worstCaseCost :
  FABL.majorityThreeRandomizedTree.worstCaseCost =
    8 / 3

theorem FABL.majorityThreeTree01_uniform_averageCost :
  FABL.RandomizedDecisionTree.deterministicAverageCost
      (FABL.uniformPMF FABL.Sign)
      FABL.majorityThreeTree01 =
    5 / 2

theorem FABL.randomizedDecisionTreeComplexity_majority_three_le :
  FABL.RandomizedDecisionTree.complexity
      (FABL.majority 3) ≤
    8 / 3

theorem FABL.averageDecisionTreeComplexity_majority_three_le :
  FABL.RandomizedDecisionTree.averageComplexity
      (FABL.uniformPMF FABL.Sign)
      (FABL.majority 3) ≤
    5 / 2

theorem FABL.majority_majorityThreeFixedOneInput
  (i : Fin 3) (a s : FABL.Sign) :
  FABL.majority 3
      (FABL.majorityThreeFixedOneInput i a
        s) =
    s

theorem FABL.majority_majorityThreeFixedTwoInput
  (i j : Fin 3) (hij : i ≠ j)
  (a b s : FABL.Sign) (hab : a ≠ b) :
  FABL.majority 3
      (FABL.majorityThreeFixedTwoInput i j
        a b s) =
    s

theorem FABL.FiniteDecisionTree.exists_majorityThree_querySkeleton
  (T :
    FABL.FiniteAlphabetDecisionTree
      FABL.Sign FABL.Sign 3)
  (hT :
    FABL.FiniteDecisionTree.Computes T
      (FABL.majority 3)) :
  ∃ i,
    ∃ (hi : i ∈ Finset.univ),
      ∃ child,
        T =
            FABL.FiniteDecisionTree.query
              i hi child ∧
          ∀ (a : FABL.Sign),
            ∃ j,
              ∃ (hj :
                j ∈ Finset.univ.erase i),
                ∃ grandchild,
                  child a =
                      FABL.FiniteDecisionTree.query
                        j hj grandchild ∧
                    ∀ (b : FABL.Sign),
                      b ≠ a →
                        ∃ k,
                          ∃ (hk :
                            k ∈
                              (Finset.univ.erase
                                    i).erase
                                j),
                            ∃ next,
                              grandchild
                                  b =
                                FABL.FiniteDecisionTree.query
                                  k hk
                                  next

theorem FABL.FiniteDecisionTree.exists_majorityThree_first_second
  (T :
    FABL.FiniteAlphabetDecisionTree
      FABL.Sign FABL.Sign 3)
  (hT :
    FABL.FiniteDecisionTree.Computes T
      (FABL.majority 3)) :
  ∃ i j,
    (∀ (a : FABL.Sign), j a ≠ i) ∧
      ∀ (x : FABL.SignCube 3),
        (2 +
            if x i = x (j (x i)) then 0
            else 1) ≤
          FABL.FiniteDecisionTree.queryCount
            T x

theorem FABL.expect_majorityThree_skeleton_disagreement
  (i : Fin 3) (j : FABL.Sign → Fin 3)
  (hji : ∀ (a : FABL.Sign), j a ≠ i) :
  (Finset.univ.expect fun x =>
      if x i = x (j (x i)) then 0
      else 1) =
    1 / 2

theorem FABL.expect_majorityThreeHardInput_skeleton_disagreement
  (i : Fin 3) (j : FABL.Sign → Fin 3)
  (hji : ∀ (a : FABL.Sign), j a ≠ i) :
  (Finset.univ.expect fun seed =>
      if
          FABL.majorityThreeHardInput seed
              i =
            FABL.majorityThreeHardInput
              seed
              (j
                (FABL.majorityThreeHardInput
                  seed i)) then
        0
      else 1) =
    2 / 3

theorem FABL.RandomizedDecisionTree.averageCostUnder_eq_seedExpectation.{u_1,
    u_2}
  {Ω : Type u_1} {α : Type u_2} {n : ℕ}
  {f : (Fin n → Ω) → α}
  [Fintype (Fin n → Ω)]
  (T :
    FABL.RandomizedDecisionTree Ω α n f)
  (μ : PMF (Fin n → Ω)) :
  T.averageCostUnder μ =
    FABL.pmfExpectation T.seedLaw
      fun seed =>
      FABL.RandomizedDecisionTree.deterministicAverageCostUnder
        μ (T.tree seed)

theorem FABL.RandomizedDecisionTree.averageCostUnder_le_worstCaseCost.{u_1,
    u_2}
  {Ω : Type u_1} {α : Type u_2} {n : ℕ}
  {f : (Fin n → Ω) → α} [Fintype Ω]
  [Nonempty Ω]
  (T :
    FABL.RandomizedDecisionTree Ω α n f)
  (μ : PMF (Fin n → Ω)) :
  T.averageCostUnder μ ≤ T.worstCaseCost