Analysis of Boolean Functions in Lean

3.5. Highlight: the Goldreich–Levin Algorithm🔗

Theorem3.5.1
Statement uses 3
Statement dependency previews
Preview
Theorem 1.4.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-3-5fidelity-exact-with-explicit-rational-scheduler

Goldreich–Levin Theorem. Given query access to a target f:\{-1,1\}^n\to\{-1,1\} and an input 0<\tau\le1, there is a randomized algorithm running in time \operatorname{poly}(n,1/\tau) which, with probability at least 9/10, outputs a duplicate-free finite list L=\{U_1,\ldots,U_\ell\} of subsets of [n] such that |\widehat f(U)|\ge\tau implies U\in L, while U\in L implies |\widehat f(U)|\ge\tau/2. Consequently, Parseval's Theorem gives |L|\le\frac4{\tau^2}. The formal witness uses K=\left\lceil\frac4{\tau^2}\right\rceil and \delta_{\mathrm{call}}=\frac1{40(n+1)(K+1)}. It explicitly aborts before expanding an active family larger than K; the verified invariant proves that this branch is unreachable whenever all queried estimates are accurate. If Proposition 3.40 schedules m samples per bucket, every execution uses at most n(2K)(2m) membership queries and at most n\left(16(n+1)^2(K+1)^2+(2K)\,8(m+1)(n+1)\right) charged local work. In this explicit oracle/charged-work cost model these are bounded respectively by \frac{2^{21}n(n+1)}{\tau^8} and \frac{2^{25}n(n+1)^2}{\tau^8}, so the advertised polynomial bound is a proved consequence rather than an informal complexity annotation. The adaptive union bound is at most 1/20, which is stronger than the theorem's required failure probability 1/10. The formal soundness conclusion is the stronger strict inequality |\widehat f(U)|>\tau/2.

Lean code for Theorem3.5.1●13 declarations
  • defdefined in FABL/Chapter03/GoldreichLevinAlgorithm/Resources.lean
    complete
    def FABL.GoldreichLevinQueryState.IsCorrectOutput {n : ℕ}
  (state : FABL.GoldreichLevinQueryState n)
  (target : FABL.BooleanFunction n)
  (τ : ↑FABL.GoldreichLevinThreshold) : Prop
    def FABL.GoldreichLevinQueryState.IsCorrectOutput
  {n : ℕ}
  (state :
    FABL.GoldreichLevinQueryState n)
  (target : FABL.BooleanFunction n)
  (τ : ↑FABL.GoldreichLevinThreshold) :
  Prop
  • defdefined in FABL/Chapter03/GoldreichLevinAlgorithm/Adaptive.lean
    complete
    def FABL.goldreichLevinControllerStepWork (n : ℕ)
  (τ : ↑FABL.GoldreichLevinThreshold) : ℕ
    def FABL.goldreichLevinControllerStepWork
  (n : ℕ)
  (τ : ↑FABL.GoldreichLevinThreshold) : ℕ
    Conservative local-work charge for forming the next candidate family, searching the accumulated
trace, filtering candidates, and checking the active-family cap at one Goldreich--Levin stage.
  • defdefined in FABL/Chapter03/GoldreichLevinAlgorithm/Adaptive.lean
    complete
    def FABL.goldreichLevinStageStepProgram {n : ℕ}
  (τ : ↑FABL.GoldreichLevinThreshold) (k : ℕ) (hk : k < n)
  (state : FABL.GoldreichLevinQueryState n)
  (active : Finset (Finset (Fin n))) :
  FABL.LearningProgram n FABL.LearningAccess.queries
    (FABL.GoldreichLevinQueryState n)
    def FABL.goldreichLevinStageStepProgram
  {n : ℕ}
  (τ : ↑FABL.GoldreichLevinThreshold)
  (k : ℕ) (hk : k < n)
  (state :
    FABL.GoldreichLevinQueryState n)
  (active : Finset (Finset (Fin n))) :
  FABL.LearningProgram n
    FABL.LearningAccess.queries
    (FABL.GoldreichLevinQueryState n)
    One charged Goldreich--Levin controller transition after the stage estimators have run.
  • defdefined in FABL/Chapter03/GoldreichLevinAlgorithm/Resources.lean
    complete
    def FABL.goldreichLevinQueryBudget (n : ℕ)
  (τ : ↑FABL.GoldreichLevinThreshold) : ℕ
    def FABL.goldreichLevinQueryBudget (n : ℕ)
  (τ : ↑FABL.GoldreichLevinThreshold) : ℕ
    Target-independent membership-query budget of the finite Goldreich--Levin oracle program.
  • defdefined in FABL/Chapter03/GoldreichLevinAlgorithm/Resources.lean
    complete
    def FABL.goldreichLevinWorkBudget (n : ℕ)
  (τ : ↑FABL.GoldreichLevinThreshold) : ℕ
    def FABL.goldreichLevinWorkBudget (n : ℕ)
  (τ : ↑FABL.GoldreichLevinThreshold) : ℕ
    Target-independent charged-work budget of the finite Goldreich--Levin oracle program.
  • defdefined in FABL/Chapter03/GoldreichLevinAlgorithm/Resources.lean
    complete
    def FABL.goldreichLevinQueryProgram {n : ℕ}
  (τ : ↑FABL.GoldreichLevinThreshold) :
  FABL.LearningProgram n FABL.LearningAccess.queries
    (FABL.GoldreichLevinQueryState n)
    def FABL.goldreichLevinQueryProgram {n : ℕ}
  (τ : ↑FABL.GoldreichLevinThreshold) :
  FABL.LearningProgram n
    FABL.LearningAccess.queries
    (FABL.GoldreichLevinQueryState n)
  • theoremdefined in FABL/Chapter03/GoldreichLevinAlgorithm/Resources.lean
    complete
    theorem FABL.goldreichLevinQueryProgram_queries_le {n : ℕ}
  (target : FABL.BooleanFunction n) (τ : ↑FABL.GoldreichLevinThreshold)
  (outcome : FABL.GoldreichLevinQueryState n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.goldreichLevinQueryProgram τ)).support) :
  outcome.2.queries ≤ FABL.goldreichLevinQueryBudget n τ
    theorem FABL.goldreichLevinQueryProgram_queries_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (τ : ↑FABL.GoldreichLevinThreshold)
  (outcome :
    FABL.GoldreichLevinQueryState n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.goldreichLevinQueryProgram
            τ)).support) :
  outcome.2.queries ≤
    FABL.goldreichLevinQueryBudget n τ
  • theoremdefined in FABL/Chapter03/GoldreichLevinAlgorithm/Resources.lean
    complete
    theorem FABL.goldreichLevinQueryProgram_work_le {n : ℕ}
  (target : FABL.BooleanFunction n) (τ : ↑FABL.GoldreichLevinThreshold)
  (outcome : FABL.GoldreichLevinQueryState n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.goldreichLevinQueryProgram τ)).support) :
  outcome.2.work ≤ FABL.goldreichLevinWorkBudget n τ
    theorem FABL.goldreichLevinQueryProgram_work_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (τ : ↑FABL.GoldreichLevinThreshold)
  (outcome :
    FABL.GoldreichLevinQueryState n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.goldreichLevinQueryProgram
            τ)).support) :
  outcome.2.work ≤
    FABL.goldreichLevinWorkBudget n τ
  • theoremdefined in FABL/Chapter03/GoldreichLevinAlgorithm/Resources.lean
    complete
    theorem FABL.goldreichLevinQueryBudget_cast_le (n : ℕ)
  (τ : ↑FABL.GoldreichLevinThreshold) :
  ↑(FABL.goldreichLevinQueryBudget n τ) ≤
    2 ^ 21 * ↑n * (↑n + 1) / ↑τ ^ 8
    theorem FABL.goldreichLevinQueryBudget_cast_le
  (n : ℕ)
  (τ : ↑FABL.GoldreichLevinThreshold) :
  ↑(FABL.goldreichLevinQueryBudget n τ) ≤
    2 ^ 21 * ↑n * (↑n + 1) / ↑τ ^ 8
    The complete Goldreich--Levin query budget is polynomial in `n` and `1 / τ`.
  • theoremdefined in FABL/Chapter03/GoldreichLevinAlgorithm/Resources.lean
    complete
    theorem FABL.goldreichLevinWorkBudget_cast_le (n : ℕ)
  (τ : ↑FABL.GoldreichLevinThreshold) :
  ↑(FABL.goldreichLevinWorkBudget n τ) ≤
    2 ^ 25 * ↑n * (↑n + 1) ^ 2 / ↑τ ^ 8
    theorem FABL.goldreichLevinWorkBudget_cast_le
  (n : ℕ)
  (τ : ↑FABL.GoldreichLevinThreshold) :
  ↑(FABL.goldreichLevinWorkBudget n τ) ≤
    2 ^ 25 * ↑n * (↑n + 1) ^ 2 / ↑τ ^ 8
    The complete charged-work budget is polynomial in `n` and `1 / τ`.
  • theoremdefined in FABL/Chapter03/GoldreichLevinAlgorithm/Resources.lean
    complete
    theorem FABL.goldreichLevinQueryProgram_correct_of_mem_support_of_not_hasFailure
  {n : ℕ} (target : FABL.BooleanFunction n)
  (τ : ↑FABL.GoldreichLevinThreshold)
  (outcome : FABL.GoldreichLevinQueryState n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.goldreichLevinQueryProgram τ)).support)
  (hgood : ¬outcome.1.HasFailure target τ) :
  outcome.1.IsCorrectOutput target τ
    theorem FABL.goldreichLevinQueryProgram_correct_of_mem_support_of_not_hasFailure
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (τ : ↑FABL.GoldreichLevinThreshold)
  (outcome :
    FABL.GoldreichLevinQueryState n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.goldreichLevinQueryProgram
            τ)).support)
  (hgood :
    ¬outcome.1.HasFailure target τ) :
  outcome.1.IsCorrectOutput target τ
  • theoremdefined in FABL/Chapter03/GoldreichLevinAlgorithm/Resources.lean
    complete
    theorem FABL.goldreichLevinQueryProgram_incorrectProbability_le_one_twentieth
  {n : ℕ} (target : FABL.BooleanFunction n)
  (τ : ↑FABL.GoldreichLevinThreshold) :
  ((FABL.goldreichLevinQueryProgram τ).eventProbability target
      fun outcome => ¬outcome.1.IsCorrectOutput target τ) ≤
    1 / 20
    theorem FABL.goldreichLevinQueryProgram_incorrectProbability_le_one_twentieth
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (τ : ↑FABL.GoldreichLevinThreshold) :
  ((FABL.goldreichLevinQueryProgram
          τ).eventProbability
      target fun outcome =>
      ¬outcome.1.IsCorrectOutput target
          τ) ≤
    1 / 20
  • theoremdefined in FABL/Chapter03/GoldreichLevinAlgorithm/Resources.lean
    complete
    theorem FABL.goldreichLevinQueryProgram_incorrectProbability_le_one_tenth
  {n : ℕ} (target : FABL.BooleanFunction n)
  (τ : ↑FABL.GoldreichLevinThreshold) :
  ((FABL.goldreichLevinQueryProgram τ).eventProbability target
      fun outcome => ¬outcome.1.IsCorrectOutput target τ) ≤
    1 / 10
    theorem FABL.goldreichLevinQueryProgram_incorrectProbability_le_one_tenth
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (τ : ↑FABL.GoldreichLevinThreshold) :
  ((FABL.goldreichLevinQueryProgram
          τ).eventProbability
      target fun outcome =>
      ¬outcome.1.IsCorrectOutput target
          τ) ≤
    1 / 10
    The probability of violating any output guarantee is at most `1/10`.
Theorem3.5.2
uses 1used by 1✓L∃∀N
Tagssection-3-5fidelity-exact-with-rational-threshold-refinement

Theorem 3.37. Let \mathcal C be a concept class such that every f:\{-1,1\}^n\to\{-1,1\} in \mathcal C has its Fourier spectrum \epsilon/4-concentrated on a collection of at most M subsets of [n]. Then \mathcal C can be learned using queries with error \epsilon, success probability at least 9/10, and running time \operatorname{poly}(M,n,1/\epsilon). The output is a finite sparse Fourier circuit representing the hypothesis. This learning procedure is called the Kushilevitz–Mansour Algorithm.

Lean code for Theorem3.5.2●4 declarations
  • defdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    def FABL.kushilevitzMansourProgramForBound {n : ℕ}
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ) :
  FABL.LearningProgram n FABL.LearningAccess.queries
    (FABL.SparseFourierHypothesis n)
    def FABL.kushilevitzMansourProgramForBound
  {n : ℕ}
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ) :
  FABL.LearningProgram n
    FABL.LearningAccess.queries
    (FABL.SparseFourierHypothesis n)
    Target-independent KM program for a stated family-size bound; the zero-bound branch is a
zero-cost fallback and is vacuous under the theorem's concentration premise.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.kushilevitzMansourProgramForBound_failureProbability_le_one_tenth
  {n : ℕ} (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ)
  (initialFamily : Finset (Finset (Fin n)))
  (hcard : initialFamily.card ≤ M)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn target.toReal (↑↑ε / 4)
      ↑initialFamily) :
  ((FABL.kushilevitzMansourProgramForBound ε M).eventProbability target
      fun outcome =>
      ↑↑ε < FABL.relativeHammingDist target outcome.1.evaluate) ≤
    1 / 10
    theorem FABL.kushilevitzMansourProgramForBound_failureProbability_le_one_tenth
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ)
  (initialFamily :
    Finset (Finset (Fin n)))
  (hcard : initialFamily.card ≤ M)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn
      target.toReal (↑↑ε / 4)
      ↑initialFamily) :
  ((FABL.kushilevitzMansourProgramForBound
          ε M).eventProbability
      target fun outcome =>
      ↑↑ε <
        FABL.relativeHammingDist target
          outcome.1.evaluate) ≤
    1 / 10
    Theorem 3.37 without an extra positivity assumption on the advertised family-size bound.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.kushilevitzMansourProgramForBound_queries_polynomial_cast_le
  {n : ℕ} (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.kushilevitzMansourProgramForBound ε M)).support) :
  ↑outcome.2.queries ≤ 2 ^ 40 * (↑n + 1) ^ 2 * (↑M + 1) ^ 8 / ↑ε ^ 10
    theorem FABL.kushilevitzMansourProgramForBound_queries_polynomial_cast_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.kushilevitzMansourProgramForBound
            ε M)).support) :
  ↑outcome.2.queries ≤
    2 ^ 40 * (↑n + 1) ^ 2 * (↑M + 1) ^ 8 /
      ↑ε ^ 10
    Target-independent polynomial query bound for the zero-safe Theorem 3.37 wrapper.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.kushilevitzMansourProgramForBound_work_polynomial_cast_le {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.kushilevitzMansourProgramForBound ε M)).support) :
  ↑outcome.2.work ≤ 2 ^ 42 * (↑n + 1) ^ 3 * (↑M + 1) ^ 8 / ↑ε ^ 10
    theorem FABL.kushilevitzMansourProgramForBound_work_polynomial_cast_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.kushilevitzMansourProgramForBound
            ε M)).support) :
  ↑outcome.2.work ≤
    2 ^ 42 * (↑n + 1) ^ 3 * (↑M + 1) ^ 8 /
      ↑ε ^ 10
    Target-independent polynomial charged-work bound for the zero-safe Theorem 3.37 wrapper.
Theorem3.5.3
Statement uses 2
Statement dependency previews
Preview
Proposition 3.2.15
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-3-5fidelity-exact

Theorem 3.38. Let \mathcal C= \left\{f:\{-1,1\}^n\to\{-1,1\}: \|\widehat f\|_1\le s\right\}. Then \mathcal C is learnable using queries with error \epsilon, success probability at least 9/10, and running time \operatorname{poly}(n,s,1/\epsilon). In particular, Proposition 3.16 implies that this concept class contains every Boolean function computable by a decision tree of size at most s.

Lean code for Theorem3.5.3●8 theorems
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.fourierOneNormClass_queryLearnable {n : ℕ}
  (target : FABL.BooleanFunction n) (s : ℝ)
  (ε : ↑FABL.PositiveLearningParameter)
  (hnorm : FABL.fourierOneNorm target.toReal ≤ s) :
  ((FABL.kushilevitzMansourProgramForBound ε
          (FABL.fourierOneNormFamilySizeBound s ε)).eventProbability
      target fun outcome =>
      ↑↑ε < FABL.relativeHammingDist target outcome.1.evaluate) ≤
    1 / 10
    theorem FABL.fourierOneNormClass_queryLearnable
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (s : ℝ)
  (ε : ↑FABL.PositiveLearningParameter)
  (hnorm :
    FABL.fourierOneNorm target.toReal ≤
      s) :
  ((FABL.kushilevitzMansourProgramForBound
          ε
          (FABL.fourierOneNormFamilySizeBound
            s ε)).eventProbability
      target fun outcome =>
      ↑↑ε <
        FABL.relativeHammingDist target
          outcome.1.evaluate) ≤
    1 / 10
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.fourierOneNormFamilySizeBound_add_one_cast_le (s : ℝ)
  (ε : ↑FABL.PositiveLearningParameter) (hs : 0 ≤ s) :
  ↑(FABL.fourierOneNormFamilySizeBound s ε + 1) ≤ 6 * (s + 1) ^ 2 / ↑↑ε
    theorem FABL.fourierOneNormFamilySizeBound_add_one_cast_le
  (s : ℝ)
  (ε : ↑FABL.PositiveLearningParameter)
  (hs : 0 ≤ s) :
  ↑(FABL.fourierOneNormFamilySizeBound s
          ε +
        1) ≤
    6 * (s + 1) ^ 2 / ↑↑ε
    The Fourier-one-norm family-size bound is polynomial in `s` and `1 / ε`.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.fourierOneNormClass_queries_polynomial_le {n : ℕ}
  (target : FABL.BooleanFunction n) (s : ℝ)
  (ε : ↑FABL.PositiveLearningParameter) (hs : 0 ≤ s)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.kushilevitzMansourProgramForBound ε
            (FABL.fourierOneNormFamilySizeBound s ε))).support) :
  ↑outcome.2.queries ≤ 2 ^ 64 * (↑n + 1) ^ 2 * (s + 1) ^ 16 / ↑↑ε ^ 18
    theorem FABL.fourierOneNormClass_queries_polynomial_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (s : ℝ)
  (ε : ↑FABL.PositiveLearningParameter)
  (hs : 0 ≤ s)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.kushilevitzMansourProgramForBound
            ε
            (FABL.fourierOneNormFamilySizeBound
              s ε))).support) :
  ↑outcome.2.queries ≤
    2 ^ 64 * (↑n + 1) ^ 2 * (s + 1) ^ 16 /
      ↑↑ε ^ 18
    Theorem 3.38's Fourier-one-norm learner has an explicit polynomial membership-query bound.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.fourierOneNormClass_work_polynomial_le {n : ℕ}
  (target : FABL.BooleanFunction n) (s : ℝ)
  (ε : ↑FABL.PositiveLearningParameter) (hs : 0 ≤ s)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.kushilevitzMansourProgramForBound ε
            (FABL.fourierOneNormFamilySizeBound s ε))).support) :
  ↑outcome.2.work ≤ 2 ^ 66 * (↑n + 1) ^ 3 * (s + 1) ^ 16 / ↑↑ε ^ 18
    theorem FABL.fourierOneNormClass_work_polynomial_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (s : ℝ)
  (ε : ↑FABL.PositiveLearningParameter)
  (hs : 0 ≤ s)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.kushilevitzMansourProgramForBound
            ε
            (FABL.fourierOneNormFamilySizeBound
              s ε))).support) :
  ↑outcome.2.work ≤
    2 ^ 66 * (↑n + 1) ^ 3 * (s + 1) ^ 16 /
      ↑↑ε ^ 18
    Theorem 3.38's Fourier-one-norm learner has an explicit polynomial charged-work bound.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.fourierOneNorm_le_leafCount_of_decisionTree {n : ℕ}
  {available : Finset (Fin n)} (target : FABL.BooleanFunction n)
  (T : FABL.F₂DecisionTree n ℝ available)
  (hT :
    T.Computes fun x =>
      target.toReal ((FABL.binaryCubeSignEquiv n) x)) :
  FABL.fourierOneNorm target.toReal ≤ ↑T.leafCount
    theorem FABL.fourierOneNorm_le_leafCount_of_decisionTree
  {n : ℕ} {available : Finset (Fin n)}
  (target : FABL.BooleanFunction n)
  (T : FABL.F₂DecisionTree n ℝ available)
  (hT :
    T.Computes fun x =>
      target.toReal
        ((FABL.binaryCubeSignEquiv n)
          x)) :
  FABL.fourierOneNorm target.toReal ≤
    ↑T.leafCount
    A sign-cube Boolean function represented by a binary decision tree has Fourier one-norm at
most the tree's number of leaves.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.decisionTreeSizeClass_queryLearnable {n : ℕ}
  {available : Finset (Fin n)} (target : FABL.BooleanFunction n)
  (T : FABL.F₂DecisionTree n ℝ available)
  (hT :
    T.Computes fun x => target.toReal ((FABL.binaryCubeSignEquiv n) x))
  (s : ℕ) (hsize : T.leafCount ≤ s)
  (ε : ↑FABL.PositiveLearningParameter) :
  ((FABL.kushilevitzMansourProgramForBound ε
          (FABL.fourierOneNormFamilySizeBound (↑s) ε)).eventProbability
      target fun outcome =>
      ↑↑ε < FABL.relativeHammingDist target outcome.1.evaluate) ≤
    1 / 10
    theorem FABL.decisionTreeSizeClass_queryLearnable
  {n : ℕ} {available : Finset (Fin n)}
  (target : FABL.BooleanFunction n)
  (T : FABL.F₂DecisionTree n ℝ available)
  (hT :
    T.Computes fun x =>
      target.toReal
        ((FABL.binaryCubeSignEquiv n) x))
  (s : ℕ) (hsize : T.leafCount ≤ s)
  (ε : ↑FABL.PositiveLearningParameter) :
  ((FABL.kushilevitzMansourProgramForBound
          ε
          (FABL.fourierOneNormFamilySizeBound
            (↑s) ε)).eventProbability
      target fun outcome =>
      ↑↑ε <
        FABL.relativeHammingDist target
          outcome.1.evaluate) ≤
    1 / 10
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.decisionTreeSizeClass_queries_polynomial_le {n : ℕ}
  {available : Finset (Fin n)} (target : FABL.BooleanFunction n)
  (T : FABL.F₂DecisionTree n ℝ available)
  (hT :
    T.Computes fun x => target.toReal ((FABL.binaryCubeSignEquiv n) x))
  (s : ℕ) (hsize : T.leafCount ≤ s)
  (ε : ↑FABL.PositiveLearningParameter)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.kushilevitzMansourProgramForBound ε
            (FABL.fourierOneNormFamilySizeBound (↑s) ε))).support) :
  ↑outcome.2.queries ≤ 2 ^ 64 * (↑n + 1) ^ 2 * (↑s + 1) ^ 16 / ↑↑ε ^ 18
    theorem FABL.decisionTreeSizeClass_queries_polynomial_le
  {n : ℕ} {available : Finset (Fin n)}
  (target : FABL.BooleanFunction n)
  (T : FABL.F₂DecisionTree n ℝ available)
  (hT :
    T.Computes fun x =>
      target.toReal
        ((FABL.binaryCubeSignEquiv n) x))
  (s : ℕ) (hsize : T.leafCount ≤ s)
  (ε : ↑FABL.PositiveLearningParameter)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.kushilevitzMansourProgramForBound
            ε
            (FABL.fourierOneNormFamilySizeBound
              (↑s) ε))).support) :
  ↑outcome.2.queries ≤
    2 ^ 64 * (↑n + 1) ^ 2 *
        (↑s + 1) ^ 16 /
      ↑↑ε ^ 18
    Exercise 3.39's decision-tree learner inherits the Fourier-one-norm polynomial query bound.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.decisionTreeSizeClass_work_polynomial_le {n : ℕ}
  {available : Finset (Fin n)} (target : FABL.BooleanFunction n)
  (T : FABL.F₂DecisionTree n ℝ available)
  (hT :
    T.Computes fun x => target.toReal ((FABL.binaryCubeSignEquiv n) x))
  (s : ℕ) (hsize : T.leafCount ≤ s)
  (ε : ↑FABL.PositiveLearningParameter)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.kushilevitzMansourProgramForBound ε
            (FABL.fourierOneNormFamilySizeBound (↑s) ε))).support) :
  ↑outcome.2.work ≤ 2 ^ 66 * (↑n + 1) ^ 3 * (↑s + 1) ^ 16 / ↑↑ε ^ 18
    theorem FABL.decisionTreeSizeClass_work_polynomial_le
  {n : ℕ} {available : Finset (Fin n)}
  (target : FABL.BooleanFunction n)
  (T : FABL.F₂DecisionTree n ℝ available)
  (hT :
    T.Computes fun x =>
      target.toReal
        ((FABL.binaryCubeSignEquiv n) x))
  (s : ℕ) (hsize : T.leafCount ≤ s)
  (ε : ↑FABL.PositiveLearningParameter)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.kushilevitzMansourProgramForBound
            ε
            (FABL.fourierOneNormFamilySizeBound
              (↑s) ε))).support) :
  ↑outcome.2.work ≤
    2 ^ 66 * (↑n + 1) ^ 3 *
        (↑s + 1) ^ 16 /
      ↑↑ε ^ 18
    Exercise 3.39's decision-tree learner inherits the Fourier-one-norm polynomial work bound.
Definition3.5.4
Statement uses 2
Statement dependency previews
Preview
Proposition 1.4.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 3.5.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-3-5fidelity-exact

Definition 3.39. Let f:\{-1,1\}^n\to\mathbb R and S\subseteq J\subseteq[n]. Write \mathbf W^{S\mid\overline J}[f] =\sum_{T\subseteq\overline J}\widehat f(S\cup T)^2 for the Fourier weight of f on sets whose restriction to J is S. Here \overline J=[n]\setminus J.

Lean code for Definition3.5.4●1 definition
  • defdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    def FABL.restrictedFourierWeight {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (S : Finset ↥J) : ℝ
    def FABL.restrictedFourierWeight {n : ℕ}
  (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (S : Finset ↥J) : ℝ
    O'Donnell, Definition 3.39: Fourier weight on the frequencies whose intersection with the
free-coordinate set `J` is the subtype-indexed set `S`.
Lemma3.5.5
Statement uses 3
Statement dependency previews
Preview
Definition 3.3.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-3-5supportfidelity-exact

Equation (3.5). For f:\{-1,1\}^n\to\mathbb R and S\subseteq J\subseteq[n], restriction to J gives \mathbf W^{S\mid\overline J}[f] =\mathbb E_{z\sim\{-1,1\}^{\overline J}} \left[\widehat{f_{J\mid z}}(S)^2\right]. This is the specialization of Corollary 3.22 used by the Goldreich–Levin Algorithm.

Lean code for Lemma3.5.5●1 theorem
  • theoremdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    theorem FABL.restrictedFourierWeight_eq_expect_sq_restrictionFourierCoeff
  {n : ℕ} (f : FABL.SignCube n → ℝ) (J : Finset (Fin n))
  (S : Finset ↥J) :
  FABL.restrictedFourierWeight f J S =
    Finset.univ.expect fun z => FABL.restrictionFourierCoeff f J S z ^ 2
    theorem FABL.restrictedFourierWeight_eq_expect_sq_restrictionFourierCoeff
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (S : Finset ↥J) :
  FABL.restrictedFourierWeight f J S =
    Finset.univ.expect fun z =>
      FABL.restrictionFourierCoeff f J S
          z ^
        2
    O'Donnell, equation (3.5): restricted Fourier weight is the second moment of the corresponding
Fourier coefficient after a uniformly random restriction.
Proposition3.5.6
Statement uses 2
Statement dependency previews
Preview
Proposition 3.4.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-3-5fidelity-exact-with-controlled-rational-scheduler

Proposition 3.40. Let S\subseteq J\subseteq[n], and let \epsilon>0 and 0<\delta\le1. An algorithm with query access to f:\{-1,1\}^n\to\{-1,1\} can output an estimate \widetilde{\mathbf W}^{S\mid\overline J}[f] satisfying \Pr\!\left[ \left|\widetilde{\mathbf W}^{S\mid\overline J}[f] -\mathbf W^{S\mid\overline J}[f]\right|>\epsilon \right]\le\delta. Its running time is \operatorname{poly}(n,1/\epsilon)\log(1/\delta).

Concretely, one sample draws independently z\sim\{-1,1\}^{\overline J} and y,y'\sim\{-1,1\}^{J}, and evaluates the \{-1,1\}-valued random variable f(y,z)\chi_S(y)\,f(y',z)\chi_S(y'). The empirical estimator uses m=O\!\left(\frac{\log(1/\delta)}{\epsilon^2}\right) independent samples, makes exactly 2m membership queries, and estimates the expectation in Equation (3.5) to the claimed accuracy and confidence. For arbitrary positive real \epsilon,\delta, the formal theorem chooses positive rational scheduler inputs \epsilon',\delta' satisfying \frac{\min(\epsilon,1/2)}2<\epsilon'<\min(\epsilon,1/2), \qquad \frac{\min(\delta,1/2)}2<\delta'<\min(\delta,1/2). Event monotonicity transfers the rational concentration theorem to the book's full positive-real parameter range. More explicitly, put E=\min(\epsilon,1/2), \qquad B=\left\lceil\log_2\left\lceil\frac{4}{\min(\delta,1/2)}\right\rceil\right\rceil. The formal scheduler uses at most 16B/E^2 samples. Every execution path makes at most 32B/E^2 membership queries and incurs at most 256B(n+1)/E^2 charged local work, which proves the stated polynomial and logarithmic resource dependence.

Lean code for Proposition3.5.6●25 declarations
  • defdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    def FABL.restrictionCoefficientObservation {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (S : Finset ↥J) (z : FABL.FixedSignCube J)
  (y : FABL.FreeSignCube J) : ℝ
    def FABL.restrictionCoefficientObservation
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (S : Finset ↥J)
  (z : FABL.FixedSignCube J)
  (y : FABL.FreeSignCube J) : ℝ
    One query-answer contribution to the restricted coefficient indexed by `S`.
  • defdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    def FABL.restrictedFourierWeightObservation {n : ℕ}
  (f : FABL.SignCube n → ℝ) (J : Finset (Fin n)) (S : Finset ↥J)
  (z : FABL.FixedSignCube J) (y y' : FABL.FreeSignCube J) : ℝ
    def FABL.restrictedFourierWeightObservation
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (S : Finset ↥J)
  (z : FABL.FixedSignCube J)
  (y y' : FABL.FreeSignCube J) : ℝ
    The product of two conditionally independent query observations used in Proposition 3.40.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    theorem FABL.expect_restrictedFourierWeightObservation_eq_restrictedFourierWeight
  {n : ℕ} (f : FABL.SignCube n → ℝ) (J : Finset (Fin n))
  (S : Finset ↥J) :
  (Finset.univ.expect fun z =>
      Finset.univ.expect fun y =>
        Finset.univ.expect fun y' =>
          FABL.restrictedFourierWeightObservation f J S z y y') =
    FABL.restrictedFourierWeight f J S
    theorem FABL.expect_restrictedFourierWeightObservation_eq_restrictedFourierWeight
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (S : Finset ↥J) :
  (Finset.univ.expect fun z =>
      Finset.univ.expect fun y =>
        Finset.univ.expect fun y' =>
          FABL.restrictedFourierWeightObservation
            f J S z y y') =
    FABL.restrictedFourierWeight f J S
    The unconditional observation used by Proposition 3.40 is unbiased for the restricted Fourier
weight.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    theorem FABL.restrictedFourierWeightObservation_mem_Icc {n : ℕ}
  (target : FABL.BooleanFunction n) (J : Finset (Fin n)) (S : Finset ↥J)
  (z : FABL.FixedSignCube J) (y y' : FABL.FreeSignCube J) :
  FABL.restrictedFourierWeightObservation target.toReal J S z y y' ∈
    Set.Icc (-1) 1
    theorem FABL.restrictedFourierWeightObservation_mem_Icc
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (S : Finset ↥J)
  (z : FABL.FixedSignCube J)
  (y y' : FABL.FreeSignCube J) :
  FABL.restrictedFourierWeightObservation
      target.toReal J S z y y' ∈
    Set.Icc (-1) 1
    For a Boolean target, every restricted-weight observation lies in `[-1,1]`.
  • defdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    def FABL.rationalRestrictedFourierWeightObservation {n : ℕ}
  (J : Finset (Fin n)) (S : Finset ↥J) (z : FABL.FixedSignCube J)
  (y y' : FABL.FreeSignCube J) (answer answer' : FABL.Sign) : ℚ
    def FABL.rationalRestrictedFourierWeightObservation
  {n : ℕ} (J : Finset (Fin n))
  (S : Finset ↥J)
  (z : FABL.FixedSignCube J)
  (y y' : FABL.FreeSignCube J)
  (answer answer' : FABL.Sign) : ℚ
    Executable rational form of one restricted-weight query-pair observation.
  • defdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    def FABL.restrictedFourierWeightObservationFromInputs {n : ℕ}
  (target : FABL.BooleanFunction n) (J : Finset (Fin n)) (S : Finset ↥J)
  (zInput yInput y'Input : FABL.SignCube n) : ℝ
    def FABL.restrictedFourierWeightObservationFromInputs
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (S : Finset ↥J)
  (zInput yInput y'Input :
    FABL.SignCube n) :
  ℝ
    Real observation obtained from the three full-cube inputs sampled by the executable
estimator. Only the fixed projection of the first input and free projections of the other two
inputs are used.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    theorem FABL.expect_restrictedFourierWeightObservationFromInputs_eq_restrictedFourierWeight
  {n : ℕ} (target : FABL.BooleanFunction n) (J : Finset (Fin n))
  (S : Finset ↥J) :
  (Finset.univ.expect fun zInput =>
      Finset.univ.expect fun yInput =>
        Finset.univ.expect fun y'Input =>
          FABL.restrictedFourierWeightObservationFromInputs target J S
            zInput yInput y'Input) =
    FABL.restrictedFourierWeight target.toReal J S
    theorem FABL.expect_restrictedFourierWeightObservationFromInputs_eq_restrictedFourierWeight
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (S : Finset ↥J) :
  (Finset.univ.expect fun zInput =>
      Finset.univ.expect fun yInput =>
        Finset.univ.expect fun y'Input =>
          FABL.restrictedFourierWeightObservationFromInputs
            target J S zInput yInput
            y'Input) =
    FABL.restrictedFourierWeight
      target.toReal J S
    One triple of independent full-cube inputs used by the executable estimator is unbiased for
the restricted Fourier weight.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    theorem FABL.restrictedFourierWeightObservationFromInputs_mem_Icc {n : ℕ}
  (target : FABL.BooleanFunction n) (J : Finset (Fin n)) (S : Finset ↥J)
  (zInput yInput y'Input : FABL.SignCube n) :
  FABL.restrictedFourierWeightObservationFromInputs target J S zInput
      yInput y'Input ∈
    Set.Icc (-1) 1
    theorem FABL.restrictedFourierWeightObservationFromInputs_mem_Icc
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (S : Finset ↥J)
  (zInput yInput y'Input :
    FABL.SignCube n) :
  FABL.restrictedFourierWeightObservationFromInputs
      target J S zInput yInput y'Input ∈
    Set.Icc (-1) 1
    Every full-cube observation used by the executable estimator lies in `[-1,1]`.
  • defdefined in FABL/Chapter03/GoldreichLevin/Estimator.lean
    complete
    def FABL.restrictedFourierWeightObservationProgram {n : ℕ}
  (J : Finset (Fin n)) (S : Finset ↥J) (z : FABL.FixedSignCube J)
  (y y' : FABL.FreeSignCube J) :
  FABL.LearningProgram n FABL.LearningAccess.queries ℚ
    def FABL.restrictedFourierWeightObservationProgram
  {n : ℕ} (J : Finset (Fin n))
  (S : Finset ↥J)
  (z : FABL.FixedSignCube J)
  (y y' : FABL.FreeSignCube J) :
  FABL.LearningProgram n
    FABL.LearningAccess.queries ℚ
    One executable observation, using exactly two membership queries.
  • defdefined in FABL/Chapter03/GoldreichLevin/Estimator.lean
    complete
    def FABL.restrictedFourierWeightEstimatorProgram {n : ℕ}
  (J : Finset (Fin n)) (S : Finset ↥J) (m : ℕ) :
  FABL.LearningProgram n FABL.LearningAccess.queries ℚ
    def FABL.restrictedFourierWeightEstimatorProgram
  {n : ℕ} (J : Finset (Fin n))
  (S : Finset ↥J) (m : ℕ) :
  FABL.LearningProgram n
    FABL.LearningAccess.queries ℚ
    Proposition 3.40's finite query program. Three independent uniform full-cube batches are
projected to `z`, `y`, and `y'`; only the two combined inputs per observation are queried.
  • defdefined in FABL/Chapter03/GoldreichLevin/Estimator.lean
    complete
    def FABL.scheduledRestrictedFourierWeightEstimatorProgram {n : ℕ}
  (J : Finset (Fin n)) (S : Finset ↥J)
  (ε δ : ↑FABL.PositiveLearningParameter) :
  FABL.LearningProgram n FABL.LearningAccess.queries ℚ
    def FABL.scheduledRestrictedFourierWeightEstimatorProgram
  {n : ℕ} (J : Finset (Fin n))
  (S : Finset ↥J)
  (ε δ :
    ↑FABL.PositiveLearningParameter) :
  FABL.LearningProgram n
    FABL.LearningAccess.queries ℚ
    Scheduled Proposition 3.40 estimator, reusing the computable positive rational scheduler
from Proposition 3.30.
  • defdefined in FABL/Chapter03/GoldreichLevin/Estimator.lean
    complete
    def FABL.restrictedFourierWeightEstimatorOutput {n : ℕ}
  (target : FABL.BooleanFunction n) (J : Finset (Fin n)) (S : Finset ↥J)
  (m : ℕ) (zInputs yInputs y'Inputs : Fin m → FABL.SignCube n) : ℚ
    def FABL.restrictedFourierWeightEstimatorOutput
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (S : Finset ↥J)
  (m : ℕ)
  (zInputs yInputs y'Inputs :
    Fin m → FABL.SignCube n) :
  ℚ
    Deterministic estimator output associated with three sampled full-cube batches.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/Estimator.lean
    complete
    theorem FABL.restrictedFourierWeightEstimatorOutput_cast {n : ℕ}
  (target : FABL.BooleanFunction n) (J : Finset (Fin n)) (S : Finset ↥J)
  (m : ℕ) (zInputs yInputs y'Inputs : Fin m → FABL.SignCube n) :
  ↑(FABL.restrictedFourierWeightEstimatorOutput target J S m zInputs
        yInputs y'Inputs) =
    FABL.realRestrictedFourierWeightEstimatorOutput target J S m zInputs
      yInputs y'Inputs
    theorem FABL.restrictedFourierWeightEstimatorOutput_cast
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (S : Finset ↥J)
  (m : ℕ)
  (zInputs yInputs y'Inputs :
    Fin m → FABL.SignCube n) :
  ↑(FABL.restrictedFourierWeightEstimatorOutput
        target J S m zInputs yInputs
        y'Inputs) =
    FABL.realRestrictedFourierWeightEstimatorOutput
      target J S m zInputs yInputs
      y'Inputs
    Casting the executable estimator output gives the corresponding real empirical mean.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    theorem FABL.measure_restrictedFourierWeightTripleEmpiricalMean_failure_le
  {n : ℕ} (target : FABL.BooleanFunction n) (J : Finset (Fin n))
  (S : Finset ↥J) {m : ℕ} (hm : 0 < m) (ε : ℝ) (hε : 0 ≤ ε) :
  (FABL.uniformPMF
            (Fin m →
              FABL.SignCube n ×
                FABL.SignCube n × FABL.SignCube n)).toMeasure.real
      {samples |
        ε ≤
          |FABL.finiteUniformEmpiricalMean
                (FABL.restrictedFourierWeightTripleObservation target J
                  S)
                samples -
              FABL.restrictedFourierWeight target.toReal J S|} ≤
    2 * Real.exp (-↑m * ε ^ 2 / 2)
    theorem FABL.measure_restrictedFourierWeightTripleEmpiricalMean_failure_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (S : Finset ↥J)
  {m : ℕ} (hm : 0 < m) (ε : ℝ)
  (hε : 0 ≤ ε) :
  (FABL.uniformPMF
            (Fin m →
              FABL.SignCube n ×
                FABL.SignCube n ×
                  FABL.SignCube
                    n)).toMeasure.real
      {samples |
        ε ≤
          |FABL.finiteUniformEmpiricalMean
                (FABL.restrictedFourierWeightTripleObservation
                  target J S)
                samples -
              FABL.restrictedFourierWeight
                target.toReal J S|} ≤
    2 * Real.exp (-↑m * ε ^ 2 / 2)
    Hoeffding concentration for a batch of independent restricted-weight observations.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/Estimator.lean
    complete
    theorem FABL.measure_restrictedFourierWeightEstimatorOutput_failure_le {n : ℕ}
  (target : FABL.BooleanFunction n) (J : Finset (Fin n)) (S : Finset ↥J)
  {m : ℕ} (hm : 0 < m) (ε : ℝ) (hε : 0 ≤ ε) :
  (FABL.uniformPMF
            ((Fin m → FABL.SignCube n) ×
              (Fin m → FABL.SignCube n) ×
                (Fin m → FABL.SignCube n))).toMeasure.real
      {inputs |
        ε ≤
          |FABL.realRestrictedFourierWeightEstimatorOutput target J S m
                inputs.1 inputs.2.1 inputs.2.2 -
              FABL.restrictedFourierWeight target.toReal J S|} ≤
    2 * Real.exp (-↑m * ε ^ 2 / 2)
    theorem FABL.measure_restrictedFourierWeightEstimatorOutput_failure_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (S : Finset ↥J)
  {m : ℕ} (hm : 0 < m) (ε : ℝ)
  (hε : 0 ≤ ε) :
  (FABL.uniformPMF
            ((Fin m → FABL.SignCube n) ×
              (Fin m → FABL.SignCube n) ×
                (Fin m →
                  FABL.SignCube
                    n))).toMeasure.real
      {inputs |
        ε ≤
          |FABL.realRestrictedFourierWeightEstimatorOutput
                target J S m inputs.1
                inputs.2.1 inputs.2.2 -
              FABL.restrictedFourierWeight
                target.toReal J S|} ≤
    2 * Real.exp (-↑m * ε ^ 2 / 2)
    The three separately generated input batches inherit the same concentration bound.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/Estimator.lean
    complete
    theorem FABL.runWithCost_restrictedFourierWeightEstimatorProgram {n : ℕ}
  (target : FABL.BooleanFunction n) (J : Finset (Fin n)) (S : Finset ↥J)
  (m : ℕ) :
  FABL.LearningProgram.runWithCost target
      (FABL.restrictedFourierWeightEstimatorProgram J S m) =
    (FABL.uniformPMF (Fin m → FABL.SignCube n)).bind fun zInputs =>
      (FABL.uniformPMF (Fin m → FABL.SignCube n)).bind fun yInputs =>
        (FABL.uniformPMF (Fin m → FABL.SignCube n)).bind fun y'Inputs =>
          PMF.pure
            (FABL.restrictedFourierWeightEstimatorOutput target J S m
                zInputs yInputs y'Inputs,
              FABL.restrictedFourierWeightEstimatorCost J S m)
    theorem FABL.runWithCost_restrictedFourierWeightEstimatorProgram
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (S : Finset ↥J)
  (m : ℕ) :
  FABL.LearningProgram.runWithCost target
      (FABL.restrictedFourierWeightEstimatorProgram
        J S m) =
    (FABL.uniformPMF
          (Fin m → FABL.SignCube n)).bind
      fun zInputs =>
      (FABL.uniformPMF
            (Fin m →
              FABL.SignCube n)).bind
        fun yInputs =>
        (FABL.uniformPMF
              (Fin m →
                FABL.SignCube n)).bind
          fun y'Inputs =>
          PMF.pure
            (FABL.restrictedFourierWeightEstimatorOutput
                target J S m zInputs
                yInputs y'Inputs,
              FABL.restrictedFourierWeightEstimatorCost
                J S m)
    Proposition 3.40 estimator's exact output law. The three nested binds are three independent
uniform full-cube batches; every leaf records the same constructor-derived cost.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/Estimator.lean
    complete
    theorem FABL.runWithCost_restrictedFourierWeightEstimatorProgram_uniformProduct
  {n : ℕ} (target : FABL.BooleanFunction n) (J : Finset (Fin n))
  (S : Finset ↥J) (m : ℕ) :
  FABL.LearningProgram.runWithCost target
      (FABL.restrictedFourierWeightEstimatorProgram J S m) =
    PMF.map
      (fun inputs =>
        (FABL.restrictedFourierWeightEstimatorOutput target J S m
            inputs.1 inputs.2.1 inputs.2.2,
          FABL.restrictedFourierWeightEstimatorCost J S m))
      (FABL.uniformPMF
        ((Fin m → FABL.SignCube n) ×
          (Fin m → FABL.SignCube n) × (Fin m → FABL.SignCube n)))
    theorem FABL.runWithCost_restrictedFourierWeightEstimatorProgram_uniformProduct
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (S : Finset ↥J)
  (m : ℕ) :
  FABL.LearningProgram.runWithCost target
      (FABL.restrictedFourierWeightEstimatorProgram
        J S m) =
    PMF.map
      (fun inputs =>
        (FABL.restrictedFourierWeightEstimatorOutput
            target J S m inputs.1
            inputs.2.1 inputs.2.2,
          FABL.restrictedFourierWeightEstimatorCost
            J S m))
      (FABL.uniformPMF
        ((Fin m → FABL.SignCube n) ×
          (Fin m → FABL.SignCube n) ×
            (Fin m → FABL.SignCube n)))
    The estimator law is a pushforward of the uniform law on three input batches.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/Estimator.lean
    complete
    theorem FABL.restrictedFourierWeightEstimatorProgram_cost_eq {n : ℕ}
  (target : FABL.BooleanFunction n) (J : Finset (Fin n)) (S : Finset ↥J)
  (m : ℕ) (outcome : ℚ × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.restrictedFourierWeightEstimatorProgram J S
            m)).support) :
  outcome.2 = FABL.restrictedFourierWeightEstimatorCost J S m
    theorem FABL.restrictedFourierWeightEstimatorProgram_cost_eq
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (S : Finset ↥J)
  (m : ℕ)
  (outcome : ℚ × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.restrictedFourierWeightEstimatorProgram
            J S m)).support) :
  outcome.2 =
    FABL.restrictedFourierWeightEstimatorCost
      J S m
    Every execution path of the finite restricted-weight estimator has the same exact cost.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/Estimator.lean
    complete
    theorem FABL.scheduledRestrictedFourierWeightEstimatorProgram_queries_eq {n : ℕ}
  (target : FABL.BooleanFunction n) (J : Finset (Fin n)) (S : Finset ↥J)
  (ε δ : ↑FABL.PositiveLearningParameter)
  (outcome : ℚ × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.scheduledRestrictedFourierWeightEstimatorProgram J S ε
            δ)).support) :
  outcome.2.queries = 2 * FABL.fourierEstimatorSampleCount ε δ
    theorem FABL.scheduledRestrictedFourierWeightEstimatorProgram_queries_eq
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (S : Finset ↥J)
  (ε δ : ↑FABL.PositiveLearningParameter)
  (outcome : ℚ × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.scheduledRestrictedFourierWeightEstimatorProgram
            J S ε δ)).support) :
  outcome.2.queries =
    2 *
      FABL.fourierEstimatorSampleCount ε δ
    The scheduled Proposition 3.40 program uses exactly twice the scheduler's sample count in
membership queries, independently of all random choices.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/Estimator.lean
    complete
    theorem FABL.restrictedFourierWeightEstimatorCost_work_le {n : ℕ}
  (J : Finset (Fin n)) (S : Finset ↥J) (m : ℕ) :
  (FABL.restrictedFourierWeightEstimatorCost J S m).work ≤
    8 * (m + 1) * (n + 1)
    theorem FABL.restrictedFourierWeightEstimatorCost_work_le
  {n : ℕ} (J : Finset (Fin n))
  (S : Finset ↥J) (m : ℕ) :
  (FABL.restrictedFourierWeightEstimatorCost
        J S m).work ≤
    8 * (m + 1) * (n + 1)
    A dimension-only polynomial upper bound for the constructor-derived work charge.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/Estimator.lean
    complete
    theorem FABL.scheduledRestrictedFourierWeightEstimatorProgram_failureProbability_le
  {n : ℕ} (target : FABL.BooleanFunction n) (J : Finset (Fin n))
  (S : Finset ↥J) (ε δ : ↑FABL.PositiveLearningParameter) :
  ((FABL.scheduledRestrictedFourierWeightEstimatorProgram J S ε
          δ).eventProbability
      target fun outcome =>
      ↑↑ε ≤
        |↑outcome.1 - FABL.restrictedFourierWeight target.toReal J S|) ≤
    ↑↑δ
    theorem FABL.scheduledRestrictedFourierWeightEstimatorProgram_failureProbability_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (S : Finset ↥J)
  (ε δ :
    ↑FABL.PositiveLearningParameter) :
  ((FABL.scheduledRestrictedFourierWeightEstimatorProgram
          J S ε δ).eventProbability
      target fun outcome =>
      ↑↑ε ≤
        |↑outcome.1 -
            FABL.restrictedFourierWeight
              target.toReal J S|) ≤
    ↑↑δ
    O'Donnell, Proposition 3.40: the scheduled two-query-pair estimator approximates the
restricted Fourier weight within `ε`, except with probability at most `δ`.
  • defdefined in FABL/Chapter03/GoldreichLevin/Estimator.lean
    complete
    def FABL.realRestrictedFourierWeightFailureBits (δ : ℝ) : ℕ
    def FABL.realRestrictedFourierWeightFailureBits
  (δ : ℝ) : ℕ
    A binary-confidence envelope expressed only in Proposition 3.40's arbitrary positive real
failure parameter. The clipping at `1 / 2` matches the finite rational scheduler's domain.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/Estimator.lean
    complete
    theorem FABL.fourierEstimatorFailureBits_le_realRestrictedFourierWeightFailureBits
  (δ' : ↑FABL.PositiveLearningParameter) (δ : ℝ) (hδ : 0 < δ)
  (hδ'Lower : min δ (1 / 2) / 2 < ↑↑δ') :
  FABL.fourierEstimatorFailureBits δ' ≤
    FABL.realRestrictedFourierWeightFailureBits δ
    theorem FABL.fourierEstimatorFailureBits_le_realRestrictedFourierWeightFailureBits
  (δ' : ↑FABL.PositiveLearningParameter)
  (δ : ℝ) (hδ : 0 < δ)
  (hδ'Lower : min δ (1 / 2) / 2 < ↑↑δ') :
  FABL.fourierEstimatorFailureBits δ' ≤
    FABL.realRestrictedFourierWeightFailureBits
      δ
    A rational confidence parameter above half of the clipped real parameter uses no more than the
real-parameter binary-confidence envelope.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/Estimator.lean
    complete
    theorem FABL.exists_scheduledRestrictedFourierWeightEstimatorProgram_failureProbability_le
  {n : ℕ} (target : FABL.BooleanFunction n) (J : Finset (Fin n))
  (S : Finset ↥J) (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
  ∃ ε' δ',
    min ε (1 / 2) / 2 < ↑↑ε' ∧
      ↑↑ε' < min ε (1 / 2) ∧
        min δ (1 / 2) / 2 < ↑↑δ' ∧
          ↑↑δ' < min δ (1 / 2) ∧
            ((FABL.scheduledRestrictedFourierWeightEstimatorProgram J S
                    ε' δ').eventProbability
                target fun outcome =>
                ε ≤
                  |↑outcome.1 -
                      FABL.restrictedFourierWeight target.toReal J S|) ≤
              δ
    theorem FABL.exists_scheduledRestrictedFourierWeightEstimatorProgram_failureProbability_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (S : Finset ↥J)
  (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
  ∃ ε' δ',
    min ε (1 / 2) / 2 < ↑↑ε' ∧
      ↑↑ε' < min ε (1 / 2) ∧
        min δ (1 / 2) / 2 < ↑↑δ' ∧
          ↑↑δ' < min δ (1 / 2) ∧
            ((FABL.scheduledRestrictedFourierWeightEstimatorProgram
                    J S ε'
                    δ').eventProbability
                target fun outcome =>
                ε ≤
                  |↑outcome.1 -
                      FABL.restrictedFourierWeight
                        target.toReal J
                        S|) ≤
              δ
    O'Donnell, Proposition 3.40 for arbitrary positive real accuracy and failure parameters.
The witnesses are finitely encoded positive rational scheduler parameters within a factor of two
of the clipped real inputs.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/Estimator.lean
    complete
    theorem FABL.exists_scheduledRestrictedFourierWeightEstimatorProgram_with_resource_bounds
  {n : ℕ} (target : FABL.BooleanFunction n) (J : Finset (Fin n))
  (S : Finset ↥J) (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
  ∃ ε' δ',
    min ε (1 / 2) / 2 < ↑↑ε' ∧
      ↑↑ε' < min ε (1 / 2) ∧
        min δ (1 / 2) / 2 < ↑↑δ' ∧
          ↑↑δ' < min δ (1 / 2) ∧
            ((FABL.scheduledRestrictedFourierWeightEstimatorProgram J S
                      ε' δ').eventProbability
                  target fun outcome =>
                  ε ≤
                    |↑outcome.1 -
                        FABL.restrictedFourierWeight target.toReal J
                          S|) ≤
                δ ∧
              FABL.fourierEstimatorFailureBits δ' ≤
                  FABL.realRestrictedFourierWeightFailureBits δ ∧
                ↑(FABL.fourierEstimatorSampleCount ε' δ') ≤
                    16 *
                        ↑(FABL.realRestrictedFourierWeightFailureBits
                            δ) /
                      min ε (1 / 2) ^ 2 ∧
                  ∀
                    outcome ∈
                      (FABL.LearningProgram.runWithCost target
                          (FABL.scheduledRestrictedFourierWeightEstimatorProgram
                            J S ε' δ')).support,
                    ↑outcome.2.queries ≤
                        32 *
                            ↑(FABL.realRestrictedFourierWeightFailureBits
                                δ) /
                          min ε (1 / 2) ^ 2 ∧
                      ↑outcome.2.work ≤
                        256 *
                              ↑(FABL.realRestrictedFourierWeightFailureBits
                                  δ) *
                            (↑n + 1) /
                          min ε (1 / 2) ^ 2
    theorem FABL.exists_scheduledRestrictedFourierWeightEstimatorProgram_with_resource_bounds
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (J : Finset (Fin n)) (S : Finset ↥J)
  (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
  ∃ ε' δ',
    min ε (1 / 2) / 2 < ↑↑ε' ∧
      ↑↑ε' < min ε (1 / 2) ∧
        min δ (1 / 2) / 2 < ↑↑δ' ∧
          ↑↑δ' < min δ (1 / 2) ∧
            ((FABL.scheduledRestrictedFourierWeightEstimatorProgram
                      J S ε'
                      δ').eventProbability
                  target fun outcome =>
                  ε ≤
                    |↑outcome.1 -
                        FABL.restrictedFourierWeight
                          target.toReal J
                          S|) ≤
                δ ∧
              FABL.fourierEstimatorFailureBits
                    δ' ≤
                  FABL.realRestrictedFourierWeightFailureBits
                    δ ∧
                ↑(FABL.fourierEstimatorSampleCount
                        ε' δ') ≤
                    16 *
                        ↑(FABL.realRestrictedFourierWeightFailureBits
                            δ) /
                      min ε (1 / 2) ^ 2 ∧
                  ∀
                    outcome ∈
                      (FABL.LearningProgram.runWithCost
                          target
                          (FABL.scheduledRestrictedFourierWeightEstimatorProgram
                            J S ε'
                            δ')).support,
                    ↑outcome.2.queries ≤
                        32 *
                            ↑(FABL.realRestrictedFourierWeightFailureBits
                                δ) /
                          min ε (1 / 2) ^
                            2 ∧
                      ↑outcome.2.work ≤
                        256 *
                              ↑(FABL.realRestrictedFourierWeightFailureBits
                                  δ) *
                            (↑n + 1) /
                          min ε (1 / 2) ^
                            2
    Proposition 3.40's arbitrary-real scheduler with probability and pathwise resource bounds in
the original real parameters. With `E = min ε (1 / 2)` and
`B = realRestrictedFourierWeightFailureBits δ`, the selected rational scheduler uses at most
`16 * B / E²` samples; every path makes at most `32 * B / E²` membership queries and incurs at most
`256 * B * (n + 1) / E²` charged local work.
Lemma3.5.7
Statement uses 2
Statement dependency previews
Preview
Definition 3.2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-3-5supportfidelity-exact-with-cube-bridge-explicit

Exercise 3.16. Let f:\{-1,1\}^n\to\mathbb R and let \eta>0. Prove that the Fourier spectrum of f is \eta-concentrated on a collection \mathcal F\subseteq2^{[n]} satisfying |\mathcal F|\le\frac{\|\widehat f\|_1^2}{\eta}.

Lean code for Lemma3.5.7●7 declarations
  • defdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    def FABL.fourierOneNorm {n : ℕ} (f : FABL.SignCube n → ℝ) : ℝ
    def FABL.fourierOneNorm {n : ℕ}
  (f : FABL.SignCube n → ℝ) : ℝ
    The Fourier `1`-norm of a real-valued function on the sign cube.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    theorem FABL.fourierOneNorm_nonneg {n : ℕ} (f : FABL.SignCube n → ℝ) :
  0 ≤ FABL.fourierOneNorm f
    theorem FABL.fourierOneNorm_nonneg {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  0 ≤ FABL.fourierOneNorm f
    The Fourier `1`-norm is nonnegative.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    theorem FABL.fourierOneNorm_eq_spectralPNorm_one {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  FABL.fourierOneNorm f =
    FABL.spectralPNorm 1 fun x => f ((FABL.binaryCubeSignEquiv n) x)
    theorem FABL.fourierOneNorm_eq_spectralPNorm_one
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.fourierOneNorm f =
    FABL.spectralPNorm 1 fun x =>
      f ((FABL.binaryCubeSignEquiv n) x)
    The sign-cube Fourier `1`-norm agrees with Definition 3.8 after the canonical cube
reindexing.
  • defdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    def FABL.l1ConcentratingFourierFamily {n : ℕ} (f : FABL.SignCube n → ℝ)
  (ε : ℝ) : Finset (Finset (Fin n))
    def FABL.l1ConcentratingFourierFamily {n : ℕ}
  (f : FABL.SignCube n → ℝ) (ε : ℝ) :
  Finset (Finset (Fin n))
    Frequencies whose coefficient is at least `ε / ‖f̂‖₁`, written without division so the
zero-norm case is handled uniformly.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    theorem FABL.mem_l1ConcentratingFourierFamily {n : ℕ} (f : FABL.SignCube n → ℝ)
  (ε : ℝ) (S : Finset (Fin n)) :
  S ∈ FABL.l1ConcentratingFourierFamily f ε ↔
    ε ≤ FABL.fourierOneNorm f * |FABL.fourierCoeff f S|
    theorem FABL.mem_l1ConcentratingFourierFamily
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (ε : ℝ) (S : Finset (Fin n)) :
  S ∈
      FABL.l1ConcentratingFourierFamily f
        ε ↔
    ε ≤
      FABL.fourierOneNorm f *
        |FABL.fourierCoeff f S|
    Membership in the explicit Fourier `1`-norm concentrating family.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    theorem FABL.card_l1ConcentratingFourierFamily_le {n : ℕ}
  (f : FABL.SignCube n → ℝ) {ε : ℝ} (hε : 0 < ε) :
  ↑(FABL.l1ConcentratingFourierFamily f ε).card ≤
    FABL.fourierOneNorm f ^ 2 / ε
    theorem FABL.card_l1ConcentratingFourierFamily_le
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  {ε : ℝ} (hε : 0 < ε) :
  ↑(FABL.l1ConcentratingFourierFamily f
          ε).card ≤
    FABL.fourierOneNorm f ^ 2 / ε
    The explicit concentrating family has cardinality at most `‖f̂‖₁² / ε`.
  • theoremdefined in FABL/Chapter03/GoldreichLevin/RestrictedWeights.lean
    complete
    theorem FABL.isFourierSpectrumConcentratedOn_l1ConcentratingFourierFamily
  {n : ℕ} (f : FABL.SignCube n → ℝ) {ε : ℝ} (hε : 0 < ε) :
  FABL.IsFourierSpectrumConcentratedOn f ε
    ↑(FABL.l1ConcentratingFourierFamily f ε)
    theorem FABL.isFourierSpectrumConcentratedOn_l1ConcentratingFourierFamily
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  {ε : ℝ} (hε : 0 < ε) :
  FABL.IsFourierSpectrumConcentratedOn f ε
    ↑(FABL.l1ConcentratingFourierFamily f
        ε)
    Exercise 3.16: every function is `ε`-concentrated on the explicit family of coefficients
whose size is controlled by its Fourier `1`-norm.
Lemma3.5.8
Statement uses 3
Statement dependency previews
Preview
Definition 3.4.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-3-5supportfidelity-exact

Exercise 3.38. Prove Theorem 3.38 in full: if every Boolean target in \mathcal C satisfies \|\widehat f\|_1\le s, then \mathcal C is learnable using queries with error \epsilon, success probability at least 9/10, and running time \operatorname{poly}(n,s,1/\epsilon). (Hint: use Exercise 3.16.)

Lean code for Lemma3.5.8●3 declarations
  • defdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    def FABL.fourierOneNormFamilySizeBound (s : ℝ)
  (ε : ↑FABL.PositiveLearningParameter) : ℕ
    def FABL.fourierOneNormFamilySizeBound (s : ℝ)
  (ε : ↑FABL.PositiveLearningParameter) :
  ℕ
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.fourierOneNormFamilySizeBound_pos (s : ℝ)
  (ε : ↑FABL.PositiveLearningParameter) :
  0 < FABL.fourierOneNormFamilySizeBound s ε
    theorem FABL.fourierOneNormFamilySizeBound_pos
  (s : ℝ)
  (ε : ↑FABL.PositiveLearningParameter) :
  0 <
    FABL.fourierOneNormFamilySizeBound s ε
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.card_l1ConcentratingFourierFamily_le_familySizeBound {n : ℕ}
  (target : FABL.BooleanFunction n) (s : ℝ)
  (ε : ↑FABL.PositiveLearningParameter)
  (hnorm : FABL.fourierOneNorm target.toReal ≤ s) :
  (FABL.l1ConcentratingFourierFamily target.toReal (↑↑ε / 4)).card ≤
    FABL.fourierOneNormFamilySizeBound s ε
    theorem FABL.card_l1ConcentratingFourierFamily_le_familySizeBound
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (s : ℝ)
  (ε : ↑FABL.PositiveLearningParameter)
  (hnorm :
    FABL.fourierOneNorm target.toReal ≤
      s) :
  (FABL.l1ConcentratingFourierFamily
        target.toReal (↑↑ε / 4)).card ≤
    FABL.fourierOneNormFamilySizeBound s ε
Lemma3.5.9
Statement uses 4
Statement dependency previews
Preview
Theorem 1.4.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-3-5supportfidelity-exact-with-rational-threshold-refinement

Exercise 3.39. Deduce Theorem 3.37 from the Goldreich–Levin Algorithm. Precisely, suppose the Fourier spectrum of each Boolean target f is \epsilon/4-concentrated on some collection \mathcal F_0 with |\mathcal F_0|\le M. For M\ge1, run Goldreich–Levin with \tau=\sqrt{\frac{\epsilon}{4M}}. Prove that the resulting list L carries all but at most \epsilon/2 Fourier weight, and then implement Theorem 3.29 using only membership queries to produce a finite sparse Fourier circuit h satisfying \operatorname{dist}(f,h)\le\epsilon. The complete construction must run in \operatorname{poly}(M,n,1/\epsilon) time and succeed with probability at least 9/10. The finite Lean oracle-program witness uses the smaller rational threshold \tau=\epsilon/(4M) so that all scheduler inputs remain finite rational data; this preserves the stated conclusion and polynomial resource bound. The two randomized stages each receive failure budget 1/20. The formal wrapper also proves that the concentration premise rules out M=0 in the nontrivial accuracy range.

Lean code for Lemma3.5.9●25 declarations
  • defdefined in FABL/Chapter03/QueryLearning.lean
    complete
    def FABL.queryInputBatchProgram {n : ℕ} (m : ℕ) :
  (Fin m → FABL.SignCube n) →
    FABL.LearningProgram n FABL.LearningAccess.queries
      (Fin m → FABL.SignCube n × FABL.Sign)
    def FABL.queryInputBatchProgram {n : ℕ}
  (m : ℕ) :
  (Fin m → FABL.SignCube n) →
    FABL.LearningProgram n
      FABL.LearningAccess.queries
      (Fin m →
        FABL.SignCube n × FABL.Sign)
    Query the target at every input in a fixed finite batch.
  • theoremdefined in FABL/Chapter03/QueryLearning.lean
    complete
    theorem FABL.runWithCost_queryInputBatchProgram {n : ℕ}
  (target : FABL.BooleanFunction n) (m : ℕ)
  (inputs : Fin m → FABL.SignCube n) :
  FABL.LearningProgram.runWithCost target
      (FABL.queryInputBatchProgram m inputs) =
    PMF.pure
      (fun i => (inputs i, target (inputs i)),
        { randomExamples := 0, queries := m, work := m })
    theorem FABL.runWithCost_queryInputBatchProgram
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (m : ℕ)
  (inputs : Fin m → FABL.SignCube n) :
  FABL.LearningProgram.runWithCost target
      (FABL.queryInputBatchProgram m
        inputs) =
    PMF.pure
      (fun i =>
        (inputs i, target (inputs i)),
        { randomExamples := 0,
          queries := m, work := m })
    Querying a fixed batch returns exactly the target-labeled batch, at one query per input.
  • theoremdefined in FABL/Chapter03/QueryLearning.lean
    complete
    theorem FABL.runWithCost_queriedFiniteFamilyFourierEstimatorProgramWithSamples_uniformMatrix
  {n : ℕ} (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n))) (m : ℕ) :
  FABL.LearningProgram.runWithCost target
      (FABL.queriedFiniteFamilyFourierEstimatorProgramWithSamples 𝓕 m) =
    PMF.map
      (fun sampleInputs =>
        (FABL.finiteFamilyFourierEstimatorOutput target 𝓕 m
            sampleInputs,
          FABL.queriedFiniteFamilyFourierEstimatorCost 𝓕 m))
      (FABL.uniformPMF (↥𝓕 → Fin m → FABL.SignCube n))
    theorem FABL.runWithCost_queriedFiniteFamilyFourierEstimatorProgramWithSamples_uniformMatrix
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n))) (m : ℕ) :
  FABL.LearningProgram.runWithCost target
      (FABL.queriedFiniteFamilyFourierEstimatorProgramWithSamples
        𝓕 m) =
    PMF.map
      (fun sampleInputs =>
        (FABL.finiteFamilyFourierEstimatorOutput
            target 𝓕 m sampleInputs,
          FABL.queriedFiniteFamilyFourierEstimatorCost
            𝓕 m))
      (FABL.uniformPMF
        (↥𝓕 → Fin m → FABL.SignCube n))
    Reshaping exposes exactly the uniform matrix law and the existing deterministic estimator
output, so all downstream concentration lemmas can be reused without a new analytic proof.
  • defdefined in FABL/Chapter03/QueryLearning.lean
    complete
    def FABL.finiteFamilyCoefficientConfidenceForTotal {n : ℕ}
  (𝓕 : Finset (Finset (Fin n))) (h𝓕 : 𝓕.Nonempty)
  (δ : ↑FABL.PositiveLearningParameter) :
  ↑FABL.PositiveLearningParameter
    def FABL.finiteFamilyCoefficientConfidenceForTotal
  {n : ℕ} (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty)
  (δ : ↑FABL.PositiveLearningParameter) :
  ↑FABL.PositiveLearningParameter
    Divide a total failure budget equally among a nonempty finite coefficient family.
  • defdefined in FABL/Chapter03/QueryLearning.lean
    complete
    def FABL.queriedFiniteFamilySamplesPerCoefficient {n : ℕ}
  (𝓕 : Finset (Finset (Fin n))) (h𝓕 : 𝓕.Nonempty)
  (ε δ : ↑FABL.PositiveLearningParameter) : ℕ
    def FABL.queriedFiniteFamilySamplesPerCoefficient
  {n : ℕ} (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty)
  (ε δ :
    ↑FABL.PositiveLearningParameter) :
  ℕ
    Samples per coefficient for a prescribed total finite-family failure budget.
  • defdefined in FABL/Chapter03/QueryLearning.lean
    complete
    def FABL.queriedFiniteFamilyFourierEstimatorProgramWithConfidence {n : ℕ}
  (𝓕 : Finset (Finset (Fin n))) (h𝓕 : 𝓕.Nonempty)
  (ε δ : ↑FABL.PositiveLearningParameter) :
  FABL.LearningProgram n FABL.LearningAccess.queries
    (FABL.SparseFourierHypothesis n)
    def FABL.queriedFiniteFamilyFourierEstimatorProgramWithConfidence
  {n : ℕ} (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty)
  (ε δ :
    ↑FABL.PositiveLearningParameter) :
  FABL.LearningProgram n
    FABL.LearningAccess.queries
    (FABL.SparseFourierHypothesis n)
    The query-access finite-family learner with an explicit total failure budget.
  • theoremdefined in FABL/Chapter03/QueryLearning.lean
    complete
    theorem FABL.queriedFiniteFamilyFourierEstimatorProgramWithConfidence_failureProbability_le
  {n : ℕ} (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n))) (h𝓕 : 𝓕.Nonempty)
  (ε δ : ↑FABL.PositiveLearningParameter)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn target.toReal (↑↑ε / 2) ↑𝓕) :
  ((FABL.queriedFiniteFamilyFourierEstimatorProgramWithConfidence 𝓕 h𝓕 ε
          δ).eventProbability
      target fun outcome =>
      ↑↑ε < FABL.relativeHammingDist target outcome.1.evaluate) ≤
    ↑↑δ
    theorem FABL.queriedFiniteFamilyFourierEstimatorProgramWithConfidence_failureProbability_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty)
  (ε δ : ↑FABL.PositiveLearningParameter)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn
      target.toReal (↑↑ε / 2) ↑𝓕) :
  ((FABL.queriedFiniteFamilyFourierEstimatorProgramWithConfidence
          𝓕 h𝓕 ε δ).eventProbability
      target fun outcome =>
      ↑↑ε <
        FABL.relativeHammingDist target
          outcome.1.evaluate) ≤
    ↑↑δ
    The configurable query learner exceeds relative Hamming error `ε` with probability at most
its requested total failure budget.
  • theoremdefined in FABL/Chapter03/QueryLearning.lean
    complete
    theorem FABL.queriedFiniteFamilyFourierEstimatorProgramWithConfidence_queries_cast_le
  {n : ℕ} (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n))) (h𝓕 : 𝓕.Nonempty)
  (ε δ : ↑FABL.PositiveLearningParameter)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.queriedFiniteFamilyFourierEstimatorProgramWithConfidence
            𝓕 h𝓕 ε δ)).support) :
  ↑outcome.2.queries ≤
    16 * ↑𝓕.card ^ 3 *
        ↑(FABL.fourierEstimatorFailureBits
            (FABL.finiteFamilyCoefficientConfidenceForTotal 𝓕 h𝓕 δ)) /
      ↑ε ^ 2
    theorem FABL.queriedFiniteFamilyFourierEstimatorProgramWithConfidence_queries_cast_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty)
  (ε δ : ↑FABL.PositiveLearningParameter)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.queriedFiniteFamilyFourierEstimatorProgramWithConfidence
            𝓕 h𝓕 ε δ)).support) :
  ↑outcome.2.queries ≤
    16 * ↑𝓕.card ^ 3 *
        ↑(FABL.fourierEstimatorFailureBits
            (FABL.finiteFamilyCoefficientConfidenceForTotal
              𝓕 h𝓕 δ)) /
      ↑ε ^ 2
    Explicit polynomial/logarithmic query bound for the configurable learner.
  • theoremdefined in FABL/Chapter03/QueryLearning.lean
    complete
    theorem FABL.queriedFiniteFamilyFourierEstimatorProgramWithConfidence_work_cast_le
  {n : ℕ} (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n))) (h𝓕 : 𝓕.Nonempty)
  (ε δ : ↑FABL.PositiveLearningParameter)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.queriedFiniteFamilyFourierEstimatorProgramWithConfidence
            𝓕 h𝓕 ε δ)).support) :
  ↑outcome.2.work ≤
    32 * ↑𝓕.card ^ 3 * (↑n + 1) *
        ↑(FABL.fourierEstimatorFailureBits
            (FABL.finiteFamilyCoefficientConfidenceForTotal 𝓕 h𝓕 δ)) /
      ↑ε ^ 2
    theorem FABL.queriedFiniteFamilyFourierEstimatorProgramWithConfidence_work_cast_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty)
  (ε δ : ↑FABL.PositiveLearningParameter)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.queriedFiniteFamilyFourierEstimatorProgramWithConfidence
            𝓕 h𝓕 ε δ)).support) :
  ↑outcome.2.work ≤
    32 * ↑𝓕.card ^ 3 * (↑n + 1) *
        ↑(FABL.fourierEstimatorFailureBits
            (FABL.finiteFamilyCoefficientConfidenceForTotal
              𝓕 h𝓕 δ)) /
      ↑ε ^ 2
    Explicit polynomial/logarithmic work bound for the configurable learner.
  • defdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    def FABL.oneTwentiethLearningParameter : ↑FABL.PositiveLearningParameter
    def FABL.oneTwentiethLearningParameter :
  ↑FABL.PositiveLearningParameter
  • defdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    def FABL.kushilevitzMansourThreshold (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ) (hM : 0 < M) : ↑FABL.GoldreichLevinThreshold
    def FABL.kushilevitzMansourThreshold
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ) (hM : 0 < M) :
  ↑FABL.GoldreichLevinThreshold
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.isFourierSpectrumConcentratedOn_of_goldreichLevin_complete {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ) (hM : 0 < M)
  (initialFamily outputFamily : Finset (Finset (Fin n)))
  (hcard : initialFamily.card ≤ M)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn target.toReal (↑↑ε / 4)
      ↑initialFamily)
  (hcomplete :
    ∀ (U : Finset (Fin n)),
      ↑↑(FABL.kushilevitzMansourThreshold ε M hM) ≤
          |FABL.fourierCoeff target.toReal U| →
        U ∈ outputFamily) :
  FABL.IsFourierSpectrumConcentratedOn target.toReal (↑↑ε / 2)
    ↑outputFamily
    theorem FABL.isFourierSpectrumConcentratedOn_of_goldreichLevin_complete
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ) (hM : 0 < M)
  (initialFamily outputFamily :
    Finset (Finset (Fin n)))
  (hcard : initialFamily.card ≤ M)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn
      target.toReal (↑↑ε / 4)
      ↑initialFamily)
  (hcomplete :
    ∀ (U : Finset (Fin n)),
      ↑↑(FABL.kushilevitzMansourThreshold
                ε M hM) ≤
          |FABL.fourierCoeff target.toReal
              U| →
        U ∈ outputFamily) :
  FABL.IsFourierSpectrumConcentratedOn
    target.toReal (↑↑ε / 2) ↑outputFamily
  • defdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    def FABL.kushilevitzMansourSecondStage {n : ℕ}
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ) (hM : 0 < M)
  (state : FABL.GoldreichLevinQueryState n) :
  FABL.LearningProgram n FABL.LearningAccess.queries
    (FABL.SparseFourierHypothesis n)
    def FABL.kushilevitzMansourSecondStage {n : ℕ}
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ) (hM : 0 < M)
  (state :
    FABL.GoldreichLevinQueryState n) :
  FABL.LearningProgram n
    FABL.LearningAccess.queries
    (FABL.SparseFourierHypothesis n)
  • defdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    def FABL.kushilevitzMansourProgram {n : ℕ}
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ) (hM : 0 < M) :
  FABL.LearningProgram n FABL.LearningAccess.queries
    (FABL.SparseFourierHypothesis n)
    def FABL.kushilevitzMansourProgram {n : ℕ}
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ) (hM : 0 < M) :
  FABL.LearningProgram n
    FABL.LearningAccess.queries
    (FABL.SparseFourierHypothesis n)
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.kushilevitzMansourProgram_failureProbability_le_one_tenth {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ) (hM : 0 < M)
  (initialFamily : Finset (Finset (Fin n)))
  (hcard : initialFamily.card ≤ M)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn target.toReal (↑↑ε / 4)
      ↑initialFamily) :
  ((FABL.kushilevitzMansourProgram ε M hM).eventProbability target
      fun outcome =>
      ↑↑ε < FABL.relativeHammingDist target outcome.1.evaluate) ≤
    1 / 10
    theorem FABL.kushilevitzMansourProgram_failureProbability_le_one_tenth
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ) (hM : 0 < M)
  (initialFamily :
    Finset (Finset (Fin n)))
  (hcard : initialFamily.card ≤ M)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn
      target.toReal (↑↑ε / 4)
      ↑initialFamily) :
  ((FABL.kushilevitzMansourProgram ε M
          hM).eventProbability
      target fun outcome =>
      ↑↑ε <
        FABL.relativeHammingDist target
          outcome.1.evaluate) ≤
    1 / 10
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.positive_familyBound_of_spectrum_concentrated {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ)
  (family : Finset (Finset (Fin n))) (hcard : family.card ≤ M)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn target.toReal (↑↑ε / 4)
      ↑family) :
  0 < M
    theorem FABL.positive_familyBound_of_spectrum_concentrated
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ)
  (family : Finset (Finset (Fin n)))
  (hcard : family.card ≤ M)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn
      target.toReal (↑↑ε / 4) ↑family) :
  0 < M
    In the nontrivial accuracy range, a family carrying all but `ε/4` Fourier weight cannot have
cardinality bounded by zero.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.kushilevitzMansourSecondStage_cost_cases {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ) (hM : 0 < M)
  (state : FABL.GoldreichLevinQueryState n)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.kushilevitzMansourSecondStage ε M hM state)).support) :
  outcome.2 = 0 ∨
    ∃ family,
      ∃ (hnonempty : family.Nonempty),
        state.active = some family ∧
          family.card ≤
              FABL.goldreichLevinActiveCap
                (FABL.kushilevitzMansourThreshold ε M hM) ∧
            outcome.2 =
              FABL.queriedFiniteFamilyFourierEstimatorCost family
                (FABL.queriedFiniteFamilySamplesPerCoefficient family
                  hnonempty ε FABL.oneTwentiethLearningParameter)
    theorem FABL.kushilevitzMansourSecondStage_cost_cases
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ) (hM : 0 < M)
  (state :
    FABL.GoldreichLevinQueryState n)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.kushilevitzMansourSecondStage
            ε M hM state)).support) :
  outcome.2 = 0 ∨
    ∃ family,
      ∃ (hnonempty : family.Nonempty),
        state.active = some family ∧
          family.card ≤
              FABL.goldreichLevinActiveCap
                (FABL.kushilevitzMansourThreshold
                  ε M hM) ∧
            outcome.2 =
              FABL.queriedFiniteFamilyFourierEstimatorCost
                family
                (FABL.queriedFiniteFamilySamplesPerCoefficient
                  family hnonempty ε
                  FABL.oneTwentiethLearningParameter)
    A second-stage execution either takes a zero-cost fallback or runs the guarded finite-family
query learner on a nonempty family below the Goldreich--Levin cap.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.kushilevitzMansourProgram_cost_decomposition {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ) (hM : 0 < M)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.kushilevitzMansourProgram ε M hM)).support) :
  ∃ firstOutcome secondOutcome,
    firstOutcome ∈
        (FABL.LearningProgram.runWithCost target
            (FABL.goldreichLevinQueryProgram
              (FABL.kushilevitzMansourThreshold ε M hM))).support ∧
      secondOutcome ∈
          (FABL.LearningProgram.runWithCost target
              (FABL.kushilevitzMansourSecondStage ε M hM
                firstOutcome.1)).support ∧
        outcome.1 = secondOutcome.1 ∧
          outcome.2 = firstOutcome.2 + secondOutcome.2
    theorem FABL.kushilevitzMansourProgram_cost_decomposition
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ) (hM : 0 < M)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.kushilevitzMansourProgram
            ε M hM)).support) :
  ∃ firstOutcome secondOutcome,
    firstOutcome ∈
        (FABL.LearningProgram.runWithCost
            target
            (FABL.goldreichLevinQueryProgram
              (FABL.kushilevitzMansourThreshold
                ε M hM))).support ∧
      secondOutcome ∈
          (FABL.LearningProgram.runWithCost
              target
              (FABL.kushilevitzMansourSecondStage
                ε M hM
                firstOutcome.1)).support ∧
        outcome.1 = secondOutcome.1 ∧
          outcome.2 =
            firstOutcome.2 +
              secondOutcome.2
    Exact cost decomposition of the two sequential KM stages.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.fourierEstimatorFailureBits_oneTwentieth_per_family_le {n : ℕ}
  (𝓕 : Finset (Finset (Fin n))) (h𝓕 : 𝓕.Nonempty) :
  FABL.fourierEstimatorFailureBits
      (FABL.finiteFamilyCoefficientConfidenceForTotal 𝓕 h𝓕
        FABL.oneTwentiethLearningParameter) ≤
    40 * 𝓕.card
    theorem FABL.fourierEstimatorFailureBits_oneTwentieth_per_family_le
  {n : ℕ} (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty) :
  FABL.fourierEstimatorFailureBits
      (FABL.finiteFamilyCoefficientConfidenceForTotal
        𝓕 h𝓕
        FABL.oneTwentiethLearningParameter) ≤
    40 * 𝓕.card
    At total failure budget `1/20`, the binary confidence scheduler uses at most forty bits per
member of the nonempty family.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.kushilevitzMansourSecondStage_queries_cast_le {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ) (hM : 0 < M)
  (state : FABL.GoldreichLevinQueryState n)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.kushilevitzMansourSecondStage ε M hM state)).support) :
  ↑outcome.2.queries ≤
    640 *
        ↑(FABL.goldreichLevinActiveCap
              (FABL.kushilevitzMansourThreshold ε M hM)) ^
          4 /
      ↑ε ^ 2
    theorem FABL.kushilevitzMansourSecondStage_queries_cast_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ) (hM : 0 < M)
  (state :
    FABL.GoldreichLevinQueryState n)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.kushilevitzMansourSecondStage
            ε M hM state)).support) :
  ↑outcome.2.queries ≤
    640 *
        ↑(FABL.goldreichLevinActiveCap
              (FABL.kushilevitzMansourThreshold
                ε M hM)) ^
          4 /
      ↑ε ^ 2
    Uniform rational membership-query bound for every guarded KM second-stage execution.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.kushilevitzMansourSecondStage_work_cast_le {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ) (hM : 0 < M)
  (state : FABL.GoldreichLevinQueryState n)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.kushilevitzMansourSecondStage ε M hM state)).support) :
  ↑outcome.2.work ≤
    1280 *
          ↑(FABL.goldreichLevinActiveCap
                (FABL.kushilevitzMansourThreshold ε M hM)) ^
            4 *
        (↑n + 1) /
      ↑ε ^ 2
    theorem FABL.kushilevitzMansourSecondStage_work_cast_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ) (hM : 0 < M)
  (state :
    FABL.GoldreichLevinQueryState n)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.kushilevitzMansourSecondStage
            ε M hM state)).support) :
  ↑outcome.2.work ≤
    1280 *
          ↑(FABL.goldreichLevinActiveCap
                (FABL.kushilevitzMansourThreshold
                  ε M hM)) ^
            4 *
        (↑n + 1) /
      ↑ε ^ 2
    Uniform rational charged-work bound for every guarded KM second-stage execution.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.kushilevitzMansourProgram_queries_cast_le {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ) (hM : 0 < M)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.kushilevitzMansourProgram ε M hM)).support) :
  ↑outcome.2.queries ≤
    ↑(FABL.goldreichLevinQueryBudget n
          (FABL.kushilevitzMansourThreshold ε M hM)) +
      640 *
          ↑(FABL.goldreichLevinActiveCap
                (FABL.kushilevitzMansourThreshold ε M hM)) ^
            4 /
        ↑ε ^ 2
    theorem FABL.kushilevitzMansourProgram_queries_cast_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ) (hM : 0 < M)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.kushilevitzMansourProgram
            ε M hM)).support) :
  ↑outcome.2.queries ≤
    ↑(FABL.goldreichLevinQueryBudget n
          (FABL.kushilevitzMansourThreshold
            ε M hM)) +
      640 *
          ↑(FABL.goldreichLevinActiveCap
                (FABL.kushilevitzMansourThreshold
                  ε M hM)) ^
            4 /
        ↑ε ^ 2
    Target-independent query bound for the complete two-stage KM program before eliminating its
Goldreich--Levin threshold.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.kushilevitzMansourProgram_work_cast_le {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ) (hM : 0 < M)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.kushilevitzMansourProgram ε M hM)).support) :
  ↑outcome.2.work ≤
    ↑(FABL.goldreichLevinWorkBudget n
          (FABL.kushilevitzMansourThreshold ε M hM)) +
      1280 *
            ↑(FABL.goldreichLevinActiveCap
                  (FABL.kushilevitzMansourThreshold ε M hM)) ^
              4 *
          (↑n + 1) /
        ↑ε ^ 2
    theorem FABL.kushilevitzMansourProgram_work_cast_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ) (hM : 0 < M)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.kushilevitzMansourProgram
            ε M hM)).support) :
  ↑outcome.2.work ≤
    ↑(FABL.goldreichLevinWorkBudget n
          (FABL.kushilevitzMansourThreshold
            ε M hM)) +
      1280 *
            ↑(FABL.goldreichLevinActiveCap
                  (FABL.kushilevitzMansourThreshold
                    ε M hM)) ^
              4 *
          (↑n + 1) /
        ↑ε ^ 2
    Target-independent charged-work bound for the complete two-stage KM program before eliminating
its Goldreich--Levin threshold.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.kushilevitzMansourProgram_queries_polynomial_cast_le {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ) (hM : 0 < M)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.kushilevitzMansourProgram ε M hM)).support) :
  ↑outcome.2.queries ≤ 2 ^ 40 * (↑n + 1) ^ 2 * (↑M + 1) ^ 8 / ↑ε ^ 10
    theorem FABL.kushilevitzMansourProgram_queries_polynomial_cast_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ) (hM : 0 < M)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.kushilevitzMansourProgram
            ε M hM)).support) :
  ↑outcome.2.queries ≤
    2 ^ 40 * (↑n + 1) ^ 2 * (↑M + 1) ^ 8 /
      ↑ε ^ 10
    The complete KM membership-query count is polynomial in `n`, `M`, and `1 / ε`.
  • theoremdefined in FABL/Chapter03/KushilevitzMansour.lean
    complete
    theorem FABL.kushilevitzMansourProgram_work_polynomial_cast_le {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter) (M : ℕ) (hM : 0 < M)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.kushilevitzMansourProgram ε M hM)).support) :
  ↑outcome.2.work ≤ 2 ^ 42 * (↑n + 1) ^ 3 * (↑M + 1) ^ 8 / ↑ε ^ 10
    theorem FABL.kushilevitzMansourProgram_work_polynomial_cast_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter)
  (M : ℕ) (hM : 0 < M)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.kushilevitzMansourProgram
            ε M hM)).support) :
  ↑outcome.2.work ≤
    2 ^ 42 * (↑n + 1) ^ 3 * (↑M + 1) ^ 8 /
      ↑ε ^ 10
    The complete KM charged-work count is polynomial in `n`, `M`, and `1 / ε`.