theorem FABL.inv_two_pow_card_le_abs_fourierCoeff_of_dependsOn
  {n : ℕ} (f : FABL.BooleanFunction n)
  (J S : Finset (Fin n))
  (hdepends : DependsOn f ↑J)
  (hcoeff :
    FABL.fourierCoeff f.toReal S ≠ 0) :
  1 / 2 ^ J.card ≤
    |FABL.fourierCoeff f.toReal S|

theorem FABL.isRelevant_toReal_of_fourierCoeff_ne_zero
  {n : ℕ} (f : FABL.BooleanFunction n)
  {S : Finset (Fin n)} {i : Fin n}
  (hcoeff :
    FABL.fourierCoeff f.toReal S ≠ 0)
  (hiS : i ∈ S) :
  FABL.IsRelevant f.toReal i

theorem FABL.fourierCoeff_eq_zero_or_inv_two_pow_le_abs_of_isKJunta
  {n k : ℕ} (f : FABL.BooleanFunction n)
  (hjunta : FABL.IsKJunta f k)
  (S : Finset (Fin n)) :
  FABL.fourierCoeff f.toReal S = 0 ∨
    1 / 2 ^ k ≤
      |FABL.fourierCoeff f.toReal S|

theorem FABL.fourierCoeff_eq_zero_or_two_zpow_neg_le_abs_of_isKJunta
  {n k : ℕ} (f : FABL.BooleanFunction n)
  (hjunta : FABL.IsKJunta f k)
  (S : Finset (Fin n)) :
  FABL.fourierCoeff f.toReal S = 0 ∨
    2 ^ (-↑k) ≤
      |FABL.fourierCoeff f.toReal S|

theorem FABL.lowDegreeJuntaLearningAlgorithm_successProbability_ge
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ)
  (hjunta : FABL.IsKJunta target k)
  (accuracy : ↑FABL.LearningAccuracy) :
  9 / 10 ≤
    (FABL.lowDegreeJuntaLearningAlgorithm
          n k).successProbability
      target accuracy

theorem FABL.lowDegreeJuntaLearningAlgorithm_learns
  (n k : ℕ)
  (accuracy : ↑FABL.LearningAccuracy) :
  FABL.LearnsConceptClassWithError
    (FABL.lowDegreeJuntaLearningAlgorithm
      n k)
    (FABL.kJuntaConceptClass n k) accuracy

theorem FABL.lowDegreeJuntaLearnerProgram_failureProbability_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ)
  (hjunta : FABL.IsKJunta target k)
  (failure :
    ↑FABL.PositiveLearningParameter) :
  ((FABL.lowDegreeJuntaLearnerProgram n k
          failure).eventProbability
      target fun outcome =>
      FABL.JuntaLearnerOutputBad target
        outcome.1) ≤
    ↑↑failure

theorem FABL.lowDegreeJuntaLearnerProgram_depth_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ)
  (failure :
    ↑FABL.PositiveLearningParameter)
  (outcome :
    Option
        (FABL.DecisionTree n FABL.Sign) ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.lowDegreeJuntaLearnerProgram
            n k failure)).support)
  (tree : FABL.DecisionTree n FABL.Sign)
  (htree : outcome.1 = some tree) :
  FABL.F₂DecisionTree.depth tree ≤ k

theorem FABL.lowDegreeJuntaLearnerProgram_cost_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ)
  (failure :
    ↑FABL.PositiveLearningParameter)
  (outcome :
    Option
        (FABL.DecisionTree n FABL.Sign) ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.lowDegreeJuntaLearnerProgram
            n k failure)).support) :
  outcome.2.randomExamples ≤
      FABL.juntaTreeCallCount k *
        FABL.lowDegreeJuntaNodeRandomExampleBound
          n k
          (FABL.juntaTreePerCallFailure k
            failure) ∧
    outcome.2.queries = 0 ∧
      outcome.2.work ≤
        FABL.juntaTreeCallCount k *
          FABL.lowDegreeJuntaNodeUniformWorkBound
            n k
            (FABL.juntaTreePerCallFailure
              k failure)

theorem FABL.lowDegreeJuntaLearnerProgram_cost_le_totalBudget
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ)
  (failure :
    ↑FABL.PositiveLearningParameter)
  (outcome :
    Option
        (FABL.DecisionTree n FABL.Sign) ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.lowDegreeJuntaLearnerProgram
            n k failure)).support) :
  outcome.2.randomExamples ≤
      FABL.lowDegreeJuntaTotalRandomExampleBudget
        n k failure ∧
    outcome.2.queries = 0 ∧
      outcome.2.work ≤
        FABL.lowDegreeJuntaTotalWorkBudget
          n k failure

theorem FABL.lowDegreeJuntaRuntimeExponentLedger
  (k : ℕ) :
  FABL.lowDegreeJuntaCutoff k ≤
      FABL.lowDegreeJuntaCutoff k + 3 ∧
    3 *
        FABL.lowDegreeJuntaPolynomialDegree
          k ≤
      FABL.lowDegreeJuntaCutoff k + 3

theorem FABL.lowDegreeJuntaTotalRandomExampleBudget_le_linearConfidence
  (n k confidenceBits : ℕ) :
  FABL.lowDegreeJuntaTotalRandomExampleBudget
      n k
      (FABL.lowDegreeJuntaDyadicFailure
        confidenceBits) ≤
    FABL.juntaTreeCallCount k *
          FABL.lowDegreeJuntaNodeRandomExampleLinearCoefficient
            k *
        (n + 1) ^
          FABL.lowDegreeJuntaNodeBaseResourceExponent
            k *
      (confidenceBits + 1)

theorem FABL.lowDegreeJuntaTotalWorkBudget_le_linearConfidence
  (n k confidenceBits : ℕ) :
  FABL.lowDegreeJuntaTotalWorkBudget n k
      (FABL.lowDegreeJuntaDyadicFailure
        confidenceBits) ≤
    FABL.juntaTreeCallCount k *
          FABL.lowDegreeJuntaNodeWorkLinearCoefficient
            k *
        (n + 1) ^
          FABL.lowDegreeJuntaNodeWorkResourceExponent
            k *
      (confidenceBits + 1)

theorem FABL.lowDegreeJuntaTotalRandomExampleBudget_isBigO_linearConfidence
  (k : ℕ) :
  (fun input =>
      ↑(FABL.lowDegreeJuntaTotalRandomExampleBudget
          input.1 k
          (FABL.lowDegreeJuntaDyadicFailure
            input.2))) =O[Filter.atTop]
    fun input =>
    ↑((input.1 + 1) ^
          FABL.lowDegreeJuntaNodeBaseResourceExponent
            k *
        (input.2 + 1))

theorem FABL.lowDegreeJuntaTotalWorkBudget_isBigO_linearConfidence
  (k : ℕ) :
  (fun input =>
      ↑(FABL.lowDegreeJuntaTotalWorkBudget
          input.1 k
          (FABL.lowDegreeJuntaDyadicFailure
            input.2))) =O[Filter.atTop]
    fun input =>
    ↑((input.1 + 1) ^
          FABL.lowDegreeJuntaNodeWorkResourceExponent
            k *
        (input.2 + 1))

theorem FABL.lowDegreeJuntaLearningFailure_eq_dyadicFailure :
  FABL.lowDegreeJuntaLearningFailure =
    FABL.lowDegreeJuntaDyadicFailure 3

theorem FABL.lowDegreeJuntaLearningAlgorithm_randomExampleCost_le
  (n k : ℕ)
  (accuracy : ↑FABL.LearningAccuracy) :
  (FABL.lowDegreeJuntaLearningAlgorithm n
          k).randomExampleCost
      accuracy ≤
    4 * FABL.juntaTreeCallCount k *
        FABL.lowDegreeJuntaNodeRandomExampleLinearCoefficient
          k *
      (n + 1) ^
        FABL.lowDegreeJuntaNodeBaseResourceExponent
          k

theorem FABL.lowDegreeJuntaLearningAlgorithm_workCost_le
  (n k : ℕ)
  (accuracy : ↑FABL.LearningAccuracy) :
  (FABL.lowDegreeJuntaLearningAlgorithm n
          k).workCost
      accuracy ≤
    4 * FABL.juntaTreeCallCount k *
        FABL.lowDegreeJuntaNodeWorkLinearCoefficient
          k *
      (n + 1) ^
        FABL.lowDegreeJuntaNodeWorkResourceExponent
          k

theorem FABL.lowDegreeJuntaLearningAlgorithm_randomExampleCost_isBigO
  (k : ℕ)
  (accuracy : ↑FABL.LearningAccuracy) :
  (fun n =>
      ↑((FABL.lowDegreeJuntaLearningAlgorithm
              n k).randomExampleCost
          accuracy)) =O[Filter.atTop]
    fun n =>
    ↑((n + 1) ^
        FABL.lowDegreeJuntaNodeBaseResourceExponent
          k)

theorem FABL.lowDegreeJuntaLearningAlgorithm_workCost_isBigO
  (k : ℕ)
  (accuracy : ↑FABL.LearningAccuracy) :
  (fun n =>
      ↑((FABL.lowDegreeJuntaLearningAlgorithm
              n k).workCost
          accuracy)) =O[Filter.atTop]
    fun n =>
    ↑((n + 1) ^
        FABL.lowDegreeJuntaNodeWorkResourceExponent
          k)

theorem FABL.recursiveJuntaLearner_failureProbability_le
  {n k : ℕ}
  (finder :
    FABL.JuntaRelevantCoordinateFinder n
      k)
  (target : FABL.BooleanFunction n)
  (hjunta : FABL.IsKJunta target k)
  (failure :
    ↑FABL.PositiveLearningParameter) :
  ((FABL.recursiveJuntaLearner finder
          failure).eventProbability
      target fun outcome =>
      FABL.JuntaLearnerOutputBad target
        outcome.1) ≤
    ↑↑failure

theorem FABL.recursiveJuntaLearner_depth_le
  {n k : ℕ}
  (finder :
    FABL.JuntaRelevantCoordinateFinder n
      k)
  (target : FABL.BooleanFunction n)
  (failure :
    ↑FABL.PositiveLearningParameter)
  (outcome :
    Option
        (FABL.DecisionTree n FABL.Sign) ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.recursiveJuntaLearner
            finder failure)).support)
  (tree : FABL.DecisionTree n FABL.Sign)
  (htree : outcome.1 = some tree) :
  FABL.F₂DecisionTree.depth tree ≤ k

theorem FABL.recursiveJuntaLearner_cost_le
  {n k : ℕ}
  (finder :
    FABL.JuntaRelevantCoordinateFinder n
      k)
  (target : FABL.BooleanFunction n)
  (failure :
    ↑FABL.PositiveLearningParameter)
  (outcome :
    Option
        (FABL.DecisionTree n FABL.Sign) ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.recursiveJuntaLearner
            finder failure)).support) :
  outcome.2.randomExamples ≤
      FABL.juntaTreeCallCount k *
        finder.randomExampleBound
          (FABL.juntaTreePerCallFailure k
            failure) ∧
    outcome.2.queries = 0 ∧
      outcome.2.work ≤
        FABL.juntaTreeCallCount k *
          finder.workBound
            (FABL.juntaTreePerCallFailure
              k failure)

theorem FABL.lowDegreeJuntaRelevantCoordinateProgram_root_failureProbability_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ)
  (hjunta : FABL.IsKJunta target k)
  (hnonconstant :
    ¬∀ (x y : FABL.SignCube n),
        target x = target y)
  (failure :
    ↑FABL.PositiveLearningParameter) :
  ((FABL.lowDegreeJuntaRelevantCoordinateProgram
          k ∅ (fun x => 1)
          failure).eventProbability
      target fun outcome =>
      FABL.LowDegreeJuntaRootFinderBad
        target outcome.1) ≤
    ↑↑failure

theorem FABL.lowDegreeJuntaRelevantCoordinateProgram_cost_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (P : Finset (Fin n))
  (z : FABL.JuntaFixedAssignment P)
  (k : ℕ)
  (failure :
    ↑FABL.PositiveLearningParameter)
  (outcome :
    Option (FABL.JuntaNodeDecision P) ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.lowDegreeJuntaRelevantCoordinateProgram
            k P z failure)).support) :
  outcome.2.randomExamples ≤
      FABL.lowDegreeJuntaNodeRandomExampleBound
        n k failure ∧
    outcome.2.queries = 0 ∧
      outcome.2.work ≤
        FABL.lowDegreeJuntaNodeUniformWorkBound
          n k failure

theorem FABL.lowDegreeJuntaNodeRandomExampleBound_le_linearConfidence
  (n k confidenceBits : ℕ) :
  FABL.lowDegreeJuntaNodeRandomExampleBound
      n k
      (FABL.lowDegreeJuntaDyadicNodeFailure
        k confidenceBits) ≤
    FABL.lowDegreeJuntaNodeRandomExampleLinearCoefficient
          k *
        (n + 1) ^
          FABL.lowDegreeJuntaNodeBaseResourceExponent
            k *
      (confidenceBits + 1)

theorem FABL.lowDegreeJuntaNodeUniformWorkBound_le_linearConfidence
  (n k confidenceBits : ℕ) :
  FABL.lowDegreeJuntaNodeUniformWorkBound
      n k
      (FABL.lowDegreeJuntaDyadicNodeFailure
        k confidenceBits) ≤
    FABL.lowDegreeJuntaNodeWorkLinearCoefficient
          k *
        (n + 1) ^
          FABL.lowDegreeJuntaNodeWorkResourceExponent
            k *
      (confidenceBits + 1)

theorem FABL.matrixExponentJuntaRuntimeExponentLedger
  (ω : ↑FABL.PositiveMatrixExponent)
  (k : ℕ) :
  FABL.matrixExponentJuntaBalancedExponent
        ω k =
      ↑ω / (↑ω + 1) * ↑k ∧
    0 ≤
        FABL.matrixExponentJuntaSolverExponent
          ω k ∧
      FABL.matrixExponentJuntaSolverExponent
            ω k ≤
          ↑(FABL.matrixExponentJuntaCutoff
              ω k) ∧
        max
            (FABL.matrixExponentJuntaSolverExponent
              ω k)
            ↑(FABL.matrixExponentJuntaCutoff
                ω k) <
          ↑ω / (↑ω + 1) * ↑k + 1