3.4. Learning theory🔗

Definition3.4.1

Statement uses 3

Statement dependency previews

Preview

Definition 1.3.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Theorem 3.4.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagssection-3-4fidelity-exact-finite-rational-accuracy-encoding

Definition 3.27. In the model of PAC (Probably Approximately Correct) learning under the uniform distribution on \{-1,1\}^n, a learning problem is specified by a concept class \mathcal C\subseteq \{f:\{-1,1\}^n\to\{-1,1\}\}. A learning algorithm A for \mathcal C is randomized and has limited access to an unknown target f\in\mathcal C. The two access models, in increasing order of strength, are:

random examples: A may draw independent pairs (x,f(x)), where x is uniform on \{-1,1\}^n;
queries: A may request f(x) for any x\in\{-1,1\}^n of its choice.

The algorithm also receives an accuracy parameter \epsilon\in[0,1/2] and must output a finite circuit representation of a hypothesis h:\{-1,1\}^n\to\{-1,1\}. It learns \mathcal C with error \epsilon if, for every target f\in\mathcal C, with high probability its output satisfies \operatorname{dist}(f,h) =\Pr_{x\sim\{-1,1\}^n}[f(x)\ne h(x)] \le\epsilon. Here and throughout this chapter, “with high probability” may be fixed to mean success probability at least 9/10.

Lean code for Definition3.4.1●10 declarations

abbrevdefined in FABL/Chapter03/LearningTheory/Program.lean

complete

abbrev FABL.LearningAccuracy : Set ℚ

abbrev FABL.LearningAccuracy : Set ℚ

A finitely encoded accuracy input in the range used by O'Donnell, Definition 3.27. Rational
inputs give the scheduler finite parameters; mathematical error bounds use their real coercions.

theoremdefined in FABL/Chapter03/LearningTheory/Program.lean

complete

theorem FABL.learningAccuracy_toReal_mem_Icc (ε : ↑FABL.LearningAccuracy) :
  ↑↑ε ∈ Set.Icc 0 (1 / 2)

theorem FABL.learningAccuracy_toReal_mem_Icc
  (ε : ↑FABL.LearningAccuracy) :
  ↑↑ε ∈ Set.Icc 0 (1 / 2)

The real value of a finitely encoded learning-accuracy input lies in `[0, 1/2]`.

inductive(2 constructors)defined in FABL/Chapter03/LearningTheory/Program.lean

complete

inductive FABL.LearningAccess : Type

inductive FABL.LearningAccess : Type

The two access models in O'Donnell, Definition 3.27.

Constructors

FABL.LearningAccess.randomExamples : FABL.LearningAccess

The learner receives independent uniform pairs.

FABL.LearningAccess.queries : FABL.LearningAccess

The learner requests the target value at an input of its choice.

structure(3 fields)defined in FABL/Chapter03/LearningTheory/Program.lean

complete

structure FABL.LearningCost : Type

structure FABL.LearningCost : Type

Resource usage of a finite learning computation.

Fields

randomExamples : ℕ

Number of calls to the random-example oracle.

queries : ℕ

Number of membership queries.

work : ℕ

Number of explicitly charged local computation steps.

inductive(9 constructors, 3 parameters)defined in FABL/Chapter03/LearningTheory/Program.lean

complete

inductive FABL.LearningProgram.{u} (n : ℕ) :
  FABL.LearningAccess → Type u → Type (u + 1)

inductive FABL.LearningProgram.{u} (n : ℕ) :
  FABL.LearningAccess →
    Type u → Type (u + 1)

A finite pure randomized computation whose only target-function effects are exposed by its
access-indexed constructors. Branches are finite syntax trees, not opaque functions with claimed
oracle costs.

Constructors

FABL.LearningProgram.pure.{u} {n : ℕ}
  {access : FABL.LearningAccess} {α : Type u} (output : α) :
  FABL.LearningProgram n access α

Return a value.

FABL.LearningProgram.coin.{u} {n : ℕ}
  {access : FABL.LearningAccess} {α : Type u}
  (next : Bool → FABL.LearningProgram n access α) :
  FABL.LearningProgram n access α

Draw one unbiased random bit.

FABL.LearningProgram.randomExample.{u} {n : ℕ} {α : Type u}
  (next :
    FABL.SignCube n × FABL.Sign →
      FABL.LearningProgram n
        FABL.LearningAccess.randomExamples α) :
  FABL.LearningProgram n FABL.LearningAccess.randomExamples
    α

Draw one independent uniform labeled example.

FABL.LearningProgram.randomExampleBatch.{u} {n : ℕ}
  {α : Type u} (m : ℕ)
  (next :
    (Fin m → FABL.SignCube n × FABL.Sign) →
      FABL.LearningProgram n
        FABL.LearningAccess.randomExamples α) :
  FABL.LearningProgram n FABL.LearningAccess.randomExamples
    α

Draw exactly `m` independent uniform labeled examples.

FABL.LearningProgram.uniformInputBatch.{u} {n : ℕ}
  {access : FABL.LearningAccess} {α : Type u} (m : ℕ)
  (next :
    (Fin m → FABL.SignCube n) →
      FABL.LearningProgram n access α) :
  FABL.LearningProgram n access α

Draw `m` independent uniform cube inputs without calling the target oracle.

FABL.LearningProgram.randomExampleMatrix.{u} {n : ℕ}
  {κ : Type} {α : Type u} (indices : Finset κ) (m : ℕ)
  (next :
    (↥indices → Fin m → FABL.SignCube n × FABL.Sign) →
      FABL.LearningProgram n
        FABL.LearningAccess.randomExamples α) :
  FABL.LearningProgram n FABL.LearningAccess.randomExamples
    α

Draw an `m`-sample batch independently for every element of a finite index type.

FABL.LearningProgram.randomExampleMatrixOutput.{u} {n : ℕ}
  {κ : Type} {α : Type u} (indices : Finset κ) (m work : ℕ)
  (output :
    (↥indices → Fin m → FABL.SignCube n × FABL.Sign) → α) :
  FABL.LearningProgram n FABL.LearningAccess.randomExamples
    α

Draw a finite matrix of labeled examples and return a pure function of it with an explicit
local-work charge.

FABL.LearningProgram.query.{u} {n : ℕ} {α : Type u}
  (x : FABL.SignCube n)
  (next :
    FABL.Sign →
      FABL.LearningProgram n FABL.LearningAccess.queries
        α) :
  FABL.LearningProgram n FABL.LearningAccess.queries α

Query the target at a chosen input.

FABL.LearningProgram.tick.{u} {n : ℕ}
  {access : FABL.LearningAccess} {α : Type u} (steps : ℕ)
  (next : FABL.LearningProgram n access α) :
  FABL.LearningProgram n access α

Charge a specified number of local computation steps.

defdefined in FABL/Chapter03/LearningTheory/Program.lean

complete

def FABL.LearningProgram.runWithCost.{u} {n : ℕ}
  {access : FABL.LearningAccess} {α : Type u}
  (target : FABL.BooleanFunction n) :
  FABL.LearningProgram n access α → PMF (α × FABL.LearningCost)

def FABL.LearningProgram.runWithCost.{u}
  {n : ℕ} {access : FABL.LearningAccess}
  {α : Type u}
  (target : FABL.BooleanFunction n) :
  FABL.LearningProgram n access α →
    PMF (α × FABL.LearningCost)

Distributional semantics of a finite learning program, including the cost of each execution
path. The target function is observable only at random-example or query nodes.

defdefined in FABL/Chapter03/LearningTheory/Program.lean

complete

def FABL.LearningProgram.eventProbability.{u} {n : ℕ}
  {access : FABL.LearningAccess} {α : Type u}
  (program : FABL.LearningProgram n access α)
  (target : FABL.BooleanFunction n)
  (event : α × FABL.LearningCost → Prop) : ℝ

def FABL.LearningProgram.eventProbability.{u}
  {n : ℕ} {access : FABL.LearningAccess}
  {α : Type u}
  (program :
    FABL.LearningProgram n access α)
  (target : FABL.BooleanFunction n)
  (event : α × FABL.LearningCost → Prop) :
  ℝ

Probability of an event on the result and cost of a finite learning computation.

structure(6 fields)defined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

structure FABL.FiniteHypothesisRepresentation.{u} (n : ℕ) : Type (u + 1)

structure FABL.FiniteHypothesisRepresentation.{u}
  (n : ℕ) : Type (u + 1)

An executable hypothesis language with finite binary encodings and explicit evaluation cost.
The decoding law makes every code produced by a learner an honest finite representation.

Fields

Code : Type u

Structured hypotheses represented by this language.

encode : self.Code → List Bool

Finite binary encoding.

decode : List Bool → Option self.Code

Decoder for finite binary strings.

decode_encode : ∀ (code : self.Code), self.decode (self.encode code) = some code

Encoding followed by decoding recovers the structured hypothesis.

evaluate : self.Code → FABL.BooleanFunction n

Total evaluator of a structured hypothesis.

evaluationWork : self.Code → FABL.SignCube n → ℕ

Explicit work used to evaluate a hypothesis at an input.

structure(7 fields)defined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

structure FABL.LearningAlgorithm.{u_1} (n : ℕ) (access : FABL.LearningAccess)
  (hypotheses : FABL.FiniteHypothesisRepresentation n) : Type (u_1 + 1)

structure FABL.LearningAlgorithm.{u_1} (n : ℕ)
  (access : FABL.LearningAccess)
  (hypotheses :
    FABL.FiniteHypothesisRepresentation
      n) :
  Type (u_1 + 1)

A Definition 3.27 learning algorithm consists of a real program, an exact success-probability
field tied to its semantics, and verified pathwise resource bounds.

Fields

program : ↑FABL.LearningAccuracy → FABL.LearningProgram n access hypotheses.Code

Program selected by the requested accuracy.

successProbability : FABL.BooleanFunction n → ↑FABL.LearningAccuracy → ℝ

Exact success probability on each target and accuracy.

randomExampleCost : ↑FABL.LearningAccuracy → ℕ

Uniform bound on random-example calls at each accuracy, independent of the target.

queryCost : ↑FABL.LearningAccuracy → ℕ

Uniform bound on membership queries at each accuracy, independent of the target.

workCost : ↑FABL.LearningAccuracy → ℕ

Uniform bound on local work at each accuracy, independent of the target.

successProbability_eq : ∀ (target : FABL.BooleanFunction n) (ε : ↑FABL.LearningAccuracy),
  self.successProbability target ε =
    (self.program ε).eventProbability target fun outcome =>
      FABL.relativeHammingDist target (hypotheses.evaluate outcome.1) ≤ ↑↑ε

The advertised probability is the actual probability of outputting an accurate hypothesis.

cost_le : ∀ (target : FABL.BooleanFunction n) (ε : ↑FABL.LearningAccuracy),
  ∀ outcome ∈ (FABL.LearningProgram.runWithCost target (self.program ε)).support,
    outcome.2.randomExamples ≤ self.randomExampleCost ε ∧
      outcome.2.queries ≤ self.queryCost ε ∧ outcome.2.work ≤ self.workCost ε

Every execution path obeys all advertised resource bounds.

defdefined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

def FABL.LearnsConceptClassWithError.{u_1} {n : ℕ}
  {access : FABL.LearningAccess}
  {hypotheses : FABL.FiniteHypothesisRepresentation n}
  (algorithm : FABL.LearningAlgorithm n access hypotheses)
  (conceptClass : Set (FABL.BooleanFunction n))
  (ε : ↑FABL.LearningAccuracy) : Prop

def FABL.LearnsConceptClassWithError.{u_1}
  {n : ℕ} {access : FABL.LearningAccess}
  {hypotheses :
    FABL.FiniteHypothesisRepresentation n}
  (algorithm :
    FABL.LearningAlgorithm n access
      hypotheses)
  (conceptClass :
    Set (FABL.BooleanFunction n))
  (ε : ↑FABL.LearningAccuracy) : Prop

O'Donnell, Definition 3.27: the algorithm PAC-learns the concept class with error ε under the
uniform distribution, with high probability fixed to at least 9/10.

Definition3.4.2

Statement uses 4

Statement dependency previews

Preview

Proposition 1.4.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 4

Reverse dependency previews

Preview

Theorem 3.4.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagssection-3-4fidelity-exact

Definition 3.28. Let \mathcal F be a collection of subsets of [n]. The Fourier spectrum of f:\{-1,1\}^n\to\mathbb R is \epsilon-concentrated on \mathcal F if \sum_{\substack{S\subseteq[n]\\S\notin\mathcal F}} \widehat f(S)^2\le\epsilon. For Boolean-valued f, this is equivalently \Pr_{\boldsymbol S\sim\mathcal S_f} [\boldsymbol S\notin\mathcal F]\le\epsilon, where \mathcal S_f is the spectral sample of f.

Lean code for Definition3.4.2●5 declarations

defdefined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

def FABL.fourierWeightOutside {n : ℕ} (f : FABL.SignCube n → ℝ)
  (𝓕 : Set (Finset (Fin n))) : ℝ

def FABL.fourierWeightOutside {n : ℕ}
  (f : FABL.SignCube n → ℝ)
  (𝓕 : Set (Finset (Fin n))) : ℝ

Fourier weight outside an arbitrary collection of characters.

defdefined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

def FABL.IsFourierSpectrumConcentratedOn {n : ℕ} (f : FABL.SignCube n → ℝ)
  (ε : ℝ) (𝓕 : Set (Finset (Fin n))) : Prop

def FABL.IsFourierSpectrumConcentratedOn
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (ε : ℝ) (𝓕 : Set (Finset (Fin n))) :
  Prop

O'Donnell, Definition 3.28: the Fourier spectrum is ε-concentrated on an arbitrary
collection.

defdefined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

def FABL.spectralSampleOutsideProbability {n : ℕ}
  (f : FABL.BooleanFunction n) (𝓕 : Set (Finset (Fin n))) : ℝ

def FABL.spectralSampleOutsideProbability
  {n : ℕ} (f : FABL.BooleanFunction n)
  (𝓕 : Set (Finset (Fin n))) : ℝ

Probability that the spectral sample lies outside an arbitrary collection.

theoremdefined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

theorem FABL.spectralSampleOutsideProbability_eq_fourierWeightOutside {n : ℕ}
  (f : FABL.BooleanFunction n) (𝓕 : Set (Finset (Fin n))) :
  FABL.spectralSampleOutsideProbability f 𝓕 =
    FABL.fourierWeightOutside f.toReal 𝓕

theorem FABL.spectralSampleOutsideProbability_eq_fourierWeightOutside
  {n : ℕ} (f : FABL.BooleanFunction n)
  (𝓕 : Set (Finset (Fin n))) :
  FABL.spectralSampleOutsideProbability f
      𝓕 =
    FABL.fourierWeightOutside f.toReal 𝓕

For Boolean functions, spectral-sample mass outside a collection is exactly its Fourier
weight outside that collection.

theoremdefined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

theorem FABL.isFourierSpectrumConcentratedOn_iff_spectralSampleOutsideProbability_le
  {n : ℕ} (f : FABL.BooleanFunction n) (ε : ℝ)
  (𝓕 : Set (Finset (Fin n))) :
  FABL.IsFourierSpectrumConcentratedOn f.toReal ε 𝓕 ↔
    FABL.spectralSampleOutsideProbability f 𝓕 ≤ ε

theorem FABL.isFourierSpectrumConcentratedOn_iff_spectralSampleOutsideProbability_le
  {n : ℕ} (f : FABL.BooleanFunction n)
  (ε : ℝ) (𝓕 : Set (Finset (Fin n))) :
  FABL.IsFourierSpectrumConcentratedOn
      f.toReal ε 𝓕 ↔
    FABL.spectralSampleOutsideProbability
        f 𝓕 ≤
      ε

The spectral-sample formulation in O'Donnell, Definition 3.28.

Theorem3.4.3

Statement uses 6

Statement dependency previews

Preview

Theorem 1.2.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 3

Reverse dependency previews

Preview

Theorem 3.4.6

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagssection-3-4fidelity-exact-stronger-rational-scheduler

Theorem 3.29. Assume that a learning algorithm A has at least random-example access to a target f:\{-1,1\}^n\to\{-1,1\}. Suppose that A can identify a finite collection \mathcal F\subseteq2^{[n]} on which the Fourier spectrum of f is \epsilon/2-concentrated. Then, using \operatorname{poly}(|\mathcal F|,n,1/\epsilon) additional time and random examples, A can output, with probability at least 9/10, a finite circuit representation of a hypothesis h satisfying \operatorname{dist}(f,h)\le\epsilon.

For nonempty \mathcal F, the associated procedure estimates every \widehat f(S), S\in\mathcal F, to accuracy |\widetilde f(S)-\widehat f(S)|\le \frac{\sqrt\epsilon}{2\sqrt{|\mathcal F|}} with per-coefficient failure probability at most 1/(10|\mathcal F|), and outputs the sparse Fourier hypothesis h(x)=\operatorname{sgn}\!\left( \sum_{S\in\mathcal F}\widetilde f(S)\chi_S(x) \right). The empty-family case is handled directly. The simultaneous-estimation guarantee and Parseval give \left\|f-\sum_{S\in\mathcal F}\widetilde f(S)\chi_S\right\|_2^2 =\sum_{S\in\mathcal F} (\widehat f(S)-\widetilde f(S))^2 +\sum_{S\notin\mathcal F}\widehat f(S)^2 \le\epsilon.

The finite Lean oracle-program learner avoids an irrational square-root scheduler input by using the stronger rational per-coefficient accuracy \epsilon/(2|\mathcal F|). For 0<\epsilon\le1/2 and nonempty \mathcal F, this is no larger than the book's displayed \sqrt\epsilon/(2\sqrt{|\mathcal F|}) budget, so it proves the same theorem with a conservative polynomial sample bound. The empty-family premise is impossible for a Boolean target in this parameter range because its total Fourier weight is 1.

Lean code for Theorem3.4.3●18 declarations

theoremdefined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

theorem FABL.not_isFourierSpectrumConcentratedOn_empty {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter) :
  ¬FABL.IsFourierSpectrumConcentratedOn target.toReal (↑↑ε / 2) ∅

theorem FABL.not_isFourierSpectrumConcentratedOn_empty
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (ε : ↑FABL.PositiveLearningParameter) :
  ¬FABL.IsFourierSpectrumConcentratedOn
      target.toReal (↑↑ε / 2) ∅

A Boolean function's spectrum cannot be `ε/2`-concentrated on the empty family for the
learning-accuracy range `0 < ε ≤ 1/2`.

theoremdefined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

theorem FABL.finiteFamily_nonempty_of_spectrum_concentrated {n : ℕ}
  (target : FABL.BooleanFunction n) (𝓕 : Finset (Finset (Fin n)))
  (ε : ↑FABL.PositiveLearningParameter)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn target.toReal (↑↑ε / 2) ↑𝓕) :
  𝓕.Nonempty

theorem FABL.finiteFamily_nonempty_of_spectrum_concentrated
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n)))
  (ε : ↑FABL.PositiveLearningParameter)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn
      target.toReal (↑↑ε / 2) ↑𝓕) :
  𝓕.Nonempty

Hence every finite family satisfying Theorem 3.29's concentration premise is automatically
nonempty; this discharges the theorem's empty-family branch without a fictitious estimator.

defdefined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

def FABL.SparseFourierHypothesis.finiteRepresentation {n : ℕ} :
  FABL.FiniteHypothesisRepresentation n

def FABL.SparseFourierHypothesis.finiteRepresentation
  {n : ℕ} :
  FABL.FiniteHypothesisRepresentation n

Sparse rational Fourier hypotheses form an honest finite binary hypothesis language with a
total executable evaluator.

theoremdefined in FABL/Chapter03/LearningTheory/FiniteFamily.lean

complete

theorem FABL.finiteFamilyFourierEstimatorOutput_decode_encode {n : ℕ}
  (target : FABL.BooleanFunction n) (𝓕 : Finset (Finset (Fin n)))
  (m : ℕ) (sampleInputs : ↥𝓕 → Fin m → FABL.SignCube n) :
  FABL.SparseFourierHypothesis.decode
      (FABL.finiteFamilyFourierEstimatorOutput target 𝓕 m
          sampleInputs).encode =
    some
      (FABL.finiteFamilyFourierEstimatorOutput target 𝓕 m sampleInputs)

theorem FABL.finiteFamilyFourierEstimatorOutput_decode_encode
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n))) (m : ℕ)
  (sampleInputs :
    ↥𝓕 → Fin m → FABL.SignCube n) :
  FABL.SparseFourierHypothesis.decode
      (FABL.finiteFamilyFourierEstimatorOutput
          target 𝓕 m
          sampleInputs).encode =
    some
      (FABL.finiteFamilyFourierEstimatorOutput
        target 𝓕 m sampleInputs)

Every concrete finite-family output round-trips through the sparse hypothesis's finite binary
encoding.

theoremdefined in FABL/Chapter03/LearningTheory/FiniteFamily.lean

complete

theorem FABL.finiteFamilyFourierEstimatorOutput_evaluationWork {n : ℕ}
  (target : FABL.BooleanFunction n) (𝓕 : Finset (Finset (Fin n)))
  (m : ℕ) (sampleInputs : ↥𝓕 → Fin m → FABL.SignCube n)
  (x : FABL.SignCube n) :
  (FABL.finiteFamilyFourierEstimatorOutput target 𝓕 m
          sampleInputs).evaluationWork
      x =
    𝓕.card * (n + 1)

theorem FABL.finiteFamilyFourierEstimatorOutput_evaluationWork
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n))) (m : ℕ)
  (sampleInputs :
    ↥𝓕 → Fin m → FABL.SignCube n)
  (x : FABL.SignCube n) :
  (FABL.finiteFamilyFourierEstimatorOutput
          target 𝓕 m
          sampleInputs).evaluationWork
      x =
    𝓕.card * (n + 1)

Evaluating the finite circuit output has the advertised support-linear structural work.

theoremdefined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

theorem FABL.uniformLpNorm_sub_sparseFourierApproximation_sq {n : ℕ}
  (f : FABL.SignCube n → ℝ) (𝓕 : Finset (Finset (Fin n)))
  (coefficient : Finset (Fin n) → ℝ) :
  (FABL.uniformLpNorm 2 fun x =>
        f x - FABL.sparseFourierApproximation 𝓕 coefficient x) ^
      2 =
    ∑ S ∈ 𝓕, (FABL.fourierCoeff f S - coefficient S) ^ 2 +
      ∑ S with S ∉ 𝓕, FABL.fourierCoeff f S ^ 2

theorem FABL.uniformLpNorm_sub_sparseFourierApproximation_sq
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (𝓕 : Finset (Finset (Fin n)))
  (coefficient : Finset (Fin n) → ℝ) :
  (FABL.uniformLpNorm 2 fun x =>
        f x -
          FABL.sparseFourierApproximation
            𝓕 coefficient x) ^
      2 =
    ∑ S ∈ 𝓕,
        (FABL.fourierCoeff f S -
            coefficient S) ^
          2 +
      ∑ S with S ∉ 𝓕,
        FABL.fourierCoeff f S ^ 2

The deterministic Parseval error decomposition used in the proof of O'Donnell,
Theorem 3.29.

defdefined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

def FABL.finiteFamilyCoefficientAccuracy {n : ℕ}
  (𝓕 : Finset (Finset (Fin n))) (h𝓕 : 𝓕.Nonempty)
  (ε : ↑FABL.PositiveLearningParameter) :
  ↑FABL.PositiveLearningParameter

def FABL.finiteFamilyCoefficientAccuracy
  {n : ℕ} (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty)
  (ε : ↑FABL.PositiveLearningParameter) :
  ↑FABL.PositiveLearningParameter

The per-coefficient accuracy budget used in Theorem 3.29.

defdefined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

def FABL.finiteFamilyCoefficientConfidence {n : ℕ}
  (𝓕 : Finset (Finset (Fin n))) (h𝓕 : 𝓕.Nonempty) :
  ↑FABL.PositiveLearningParameter

def FABL.finiteFamilyCoefficientConfidence
  {n : ℕ} (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty) :
  ↑FABL.PositiveLearningParameter

The per-coefficient confidence budget used for the `1/10` union bound.

defdefined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

def FABL.finiteFamilySamplesPerCoefficient {n : ℕ}
  (𝓕 : Finset (Finset (Fin n))) (h𝓕 : 𝓕.Nonempty)
  (ε : ↑FABL.PositiveLearningParameter) : ℕ

def FABL.finiteFamilySamplesPerCoefficient
  {n : ℕ} (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty)
  (ε : ↑FABL.PositiveLearningParameter) :
  ℕ

Samples per Fourier coefficient in the finite-family learner.

defdefined in FABL/Chapter03/LearningTheory/FiniteFamily.lean

complete

def FABL.finiteFamilyFourierEstimatorProgram {n : ℕ}
  (𝓕 : Finset (Finset (Fin n))) (h𝓕 : 𝓕.Nonempty)
  (ε : ↑FABL.PositiveLearningParameter) :
  FABL.LearningProgram n FABL.LearningAccess.randomExamples
    (FABL.SparseFourierHypothesis n)

def FABL.finiteFamilyFourierEstimatorProgram
  {n : ℕ} (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty)
  (ε : ↑FABL.PositiveLearningParameter) :
  FABL.LearningProgram n
    FABL.LearningAccess.randomExamples
    (FABL.SparseFourierHypothesis n)

The scheduled finite-family estimator used by Theorem 3.29.

theoremdefined in FABL/Chapter03/LearningTheory/FiniteFamily.lean

complete

theorem FABL.runWithCost_finiteFamilyFourierEstimatorProgram {n : ℕ}
  (target : FABL.BooleanFunction n) (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty) (ε : ↑FABL.PositiveLearningParameter) :
  FABL.LearningProgram.runWithCost target
      (FABL.finiteFamilyFourierEstimatorProgram 𝓕 h𝓕 ε) =
    FABL.LearningProgram.randomExampleMatrixOutputLaw target 𝓕
      (FABL.finiteFamilySamplesPerCoefficient 𝓕 h𝓕 ε)
      (𝓕.card * FABL.finiteFamilySamplesPerCoefficient 𝓕 h𝓕 ε * (n + 1))
      (FABL.finiteFamilyFourierEstimatorLabeledOutput 𝓕
        (FABL.finiteFamilySamplesPerCoefficient 𝓕 h𝓕 ε))

theorem FABL.runWithCost_finiteFamilyFourierEstimatorProgram
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty)
  (ε : ↑FABL.PositiveLearningParameter) :
  FABL.LearningProgram.runWithCost target
      (FABL.finiteFamilyFourierEstimatorProgram
        𝓕 h𝓕 ε) =
    FABL.LearningProgram.randomExampleMatrixOutputLaw
      target 𝓕
      (FABL.finiteFamilySamplesPerCoefficient
        𝓕 h𝓕 ε)
      (𝓕.card *
          FABL.finiteFamilySamplesPerCoefficient
            𝓕 h𝓕 ε *
        (n + 1))
      (FABL.finiteFamilyFourierEstimatorLabeledOutput
        𝓕
        (FABL.finiteFamilySamplesPerCoefficient
          𝓕 h𝓕 ε))

The scheduled family learner is interpreted by the direct finite matrix-output law.

theoremdefined in FABL/Chapter03/LearningTheory/FiniteFamily.lean

complete

theorem FABL.finiteFamilyFourierEstimatorProgram_cost_eq {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.finiteFamilyFourierEstimatorProgram 𝓕 h𝓕 ε)).support) :
  outcome.2 =
    {
      randomExamples :=
        𝓕.card * FABL.finiteFamilySamplesPerCoefficient 𝓕 h𝓕 ε,
      queries := 0,
      work :=
        𝓕.card * FABL.finiteFamilySamplesPerCoefficient 𝓕 h𝓕 ε +
          𝓕.card * FABL.finiteFamilySamplesPerCoefficient 𝓕 h𝓕 ε *
            (n + 1) }

theorem FABL.finiteFamilyFourierEstimatorProgram_cost_eq
  {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.finiteFamilyFourierEstimatorProgram
            𝓕 h𝓕 ε)).support) :
  outcome.2 =
    {
      randomExamples :=
        𝓕.card *
          FABL.finiteFamilySamplesPerCoefficient
            𝓕 h𝓕 ε,
      queries := 0,
      work :=
        𝓕.card *
            FABL.finiteFamilySamplesPerCoefficient
              𝓕 h𝓕 ε +
          𝓕.card *
              FABL.finiteFamilySamplesPerCoefficient
                𝓕 h𝓕 ε *
            (n + 1) }

Every finite-family estimator path has exact target-independent resource usage.

theoremdefined in FABL/Chapter03/LearningTheory/FiniteFamily.lean

complete

theorem FABL.finiteFamilyFourierEstimatorProgram_cost_polyBound {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.finiteFamilyFourierEstimatorProgram 𝓕 h𝓕 ε)).support) :
  ↑outcome.2.randomExamples ≤
      16 * ↑𝓕.card ^ 3 * ↑(Nat.clog 2 (20 * 𝓕.card)) / ↑ε ^ 2 ∧
    outcome.2.queries = 0 ∧
      ↑outcome.2.work ≤
        16 * ↑𝓕.card ^ 3 * (↑n + 2) * ↑(Nat.clog 2 (20 * 𝓕.card)) /
          ↑ε ^ 2

theorem FABL.finiteFamilyFourierEstimatorProgram_cost_polyBound
  {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.finiteFamilyFourierEstimatorProgram
            𝓕 h𝓕 ε)).support) :
  ↑outcome.2.randomExamples ≤
      16 * ↑𝓕.card ^ 3 *
          ↑(Nat.clog 2 (20 * 𝓕.card)) /
        ↑ε ^ 2 ∧
    outcome.2.queries = 0 ∧
      ↑outcome.2.work ≤
        16 * ↑𝓕.card ^ 3 * (↑n + 2) *
            ↑(Nat.clog 2 (20 * 𝓕.card)) /
          ↑ε ^ 2

Every actual estimator path has zero query cost and the explicit
`poly(|𝓕|, n, 1/ε) · clog₂(20|𝓕|)` random-example and work bounds.

theoremdefined in FABL/Chapter03/LearningTheory/FiniteFamily.lean

complete

theorem FABL.measure_finiteFamily_someCoefficient_bad_le_one_tenth {n : ℕ}
  (target : FABL.BooleanFunction n) (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty) (ε : ↑FABL.PositiveLearningParameter) :
  (FABL.LearningProgram.randomExampleMatrixInputLaw 𝓕
            (FABL.finiteFamilySamplesPerCoefficient 𝓕 h𝓕
              ε)).toMeasure.real
      (⋃ S, FABL.finiteFamilyCoefficientBadSet target 𝓕 h𝓕 ε S) ≤
    1 / 10

theorem FABL.measure_finiteFamily_someCoefficient_bad_le_one_tenth
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty)
  (ε : ↑FABL.PositiveLearningParameter) :
  (FABL.LearningProgram.randomExampleMatrixInputLaw
            𝓕
            (FABL.finiteFamilySamplesPerCoefficient
              𝓕 h𝓕 ε)).toMeasure.real
      (⋃ S,
        FABL.finiteFamilyCoefficientBadSet
          target 𝓕 h𝓕 ε S) ≤
    1 / 10

With the `1/(10|𝓕|)` confidence budget, the probability that any Theorem 3.29 row is
inaccurate is at most `1/10`.

theoremdefined in FABL/Chapter03/LearningTheory/FiniteFamily.lean

complete

theorem FABL.relativeHammingDist_sparseFourierHypothesis_of_coefficients_le
  {n : ℕ} (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n))) (h𝓕 : 𝓕.Nonempty)
  (ε : ↑FABL.PositiveLearningParameter) (coefficient : ↥𝓕 → ℚ)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn target.toReal (↑↑ε / 2) ↑𝓕)
  (hcoefficient :
    ∀ (S : ↥𝓕),
      |↑(coefficient S) - FABL.fourierCoeff target.toReal ↑S| ≤
        ↑↑(FABL.finiteFamilyCoefficientAccuracy 𝓕 h𝓕 ε)) :
  FABL.relativeHammingDist target
      (FABL.SparseFourierHypothesis.ofCoefficients 𝓕
          coefficient).evaluate ≤
    ↑↑ε

theorem FABL.relativeHammingDist_sparseFourierHypothesis_of_coefficients_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty)
  (ε : ↑FABL.PositiveLearningParameter)
  (coefficient : ↥𝓕 → ℚ)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn
      target.toReal (↑↑ε / 2) ↑𝓕)
  (hcoefficient :
    ∀ (S : ↥𝓕),
      |↑(coefficient S) -
            FABL.fourierCoeff
              target.toReal ↑S| ≤
        ↑↑(FABL.finiteFamilyCoefficientAccuracy
              𝓕 h𝓕 ε)) :
  FABL.relativeHammingDist target
      (FABL.SparseFourierHypothesis.ofCoefficients
          𝓕 coefficient).evaluate ≤
    ↑↑ε

Deterministic analytic core of Theorem 3.29: simultaneous coefficient accuracy and spectral
concentration imply that sign rounding of the sparse output has error at most `ε`.

theoremdefined in FABL/Chapter03/LearningTheory/FiniteFamily.lean

complete

theorem FABL.relativeHammingDist_finiteFamilyFourierEstimatorOutput_le_of_no_bad
  {n : ℕ} (target : FABL.BooleanFunction n)
  (𝒽 : Finset (Finset (Fin n))) (h𝒽 : 𝒽.Nonempty)
  (ε : ↑FABL.PositiveLearningParameter)
  (sampleInputs :
    ↥𝒽 →
      Fin (FABL.finiteFamilySamplesPerCoefficient 𝒽 h𝒽 ε) →
        FABL.SignCube n)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn target.toReal (↑↑ε / 2) ↑𝒽)
  (hgood :
    ∀ (S : ↥𝒽),
      sampleInputs ∉
        FABL.finiteFamilyCoefficientBadSet target 𝒽 h𝒽 ε S) :
  FABL.relativeHammingDist target
      (FABL.finiteFamilyFourierEstimatorOutput target 𝒽
          (FABL.finiteFamilySamplesPerCoefficient 𝒽 h𝒽 ε)
          sampleInputs).evaluate ≤
    ↑↑ε

theorem FABL.relativeHammingDist_finiteFamilyFourierEstimatorOutput_le_of_no_bad
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (𝒽 : Finset (Finset (Fin n)))
  (h𝒽 : 𝒽.Nonempty)
  (ε : ↑FABL.PositiveLearningParameter)
  (sampleInputs :
    ↥𝒽 →
      Fin
          (FABL.finiteFamilySamplesPerCoefficient
            𝒽 h𝒽 ε) →
        FABL.SignCube n)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn
      target.toReal (↑↑ε / 2) ↑𝒽)
  (hgood :
    ∀ (S : ↥𝒽),
      sampleInputs ∉
        FABL.finiteFamilyCoefficientBadSet
          target 𝒽 h𝒽 ε S) :
  FABL.relativeHammingDist target
      (FABL.finiteFamilyFourierEstimatorOutput
          target 𝒽
          (FABL.finiteFamilySamplesPerCoefficient
            𝒽 h𝒽 ε)
          sampleInputs).evaluate ≤
    ↑↑ε

Outside every scheduled coefficient failure event, the finite-family estimator outputs a
hypothesis of relative Hamming error at most `ε`.

theoremdefined in FABL/Chapter03/LearningTheory/FiniteFamily.lean

complete

theorem FABL.measure_finiteFamilyFourierEstimatorOutput_failure_le_one_tenth
  {n : ℕ} (target : FABL.BooleanFunction n)
  (𝒽 : Finset (Finset (Fin n))) (h𝒽 : 𝒽.Nonempty)
  (ε : ↑FABL.PositiveLearningParameter)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn target.toReal (↑↑ε / 2) ↑𝒽) :
  (FABL.LearningProgram.randomExampleMatrixInputLaw 𝒽
            (FABL.finiteFamilySamplesPerCoefficient 𝒽 h𝒽
              ε)).toMeasure.real
      {sampleInputs |
        ↑↑ε <
          FABL.relativeHammingDist target
            (FABL.finiteFamilyFourierEstimatorOutput target 𝒽
                (FABL.finiteFamilySamplesPerCoefficient 𝒽 h𝒽 ε)
                sampleInputs).evaluate} ≤
    1 / 10

theorem FABL.measure_finiteFamilyFourierEstimatorOutput_failure_le_one_tenth
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (𝒽 : Finset (Finset (Fin n)))
  (h𝒽 : 𝒽.Nonempty)
  (ε : ↑FABL.PositiveLearningParameter)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn
      target.toReal (↑↑ε / 2) ↑𝒽) :
  (FABL.LearningProgram.randomExampleMatrixInputLaw
            𝒽
            (FABL.finiteFamilySamplesPerCoefficient
              𝒽 h𝒽 ε)).toMeasure.real
      {sampleInputs |
        ↑↑ε <
          FABL.relativeHammingDist target
            (FABL.finiteFamilyFourierEstimatorOutput
                target 𝒽
                (FABL.finiteFamilySamplesPerCoefficient
                  𝒽 h𝒽 ε)
                sampleInputs).evaluate} ≤
    1 / 10

A uniform matrix of random examples makes the finite-family estimator inaccurate with
probability at most `1/10`.

theoremdefined in FABL/Chapter03/LearningTheory/FiniteFamily.lean

complete

theorem FABL.finiteFamilyFourierEstimatorProgram_failureProbability_le_one_tenth
  {n : ℕ} (target : FABL.BooleanFunction n)
  (𝒽 : Finset (Finset (Fin n))) (h𝒽 : 𝒽.Nonempty)
  (ε : ↑FABL.PositiveLearningParameter)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn target.toReal (↑↑ε / 2) ↑𝒽) :
  ((FABL.finiteFamilyFourierEstimatorProgram 𝒽 h𝒽 ε).eventProbability
      target fun outcome =>
      ↑↑ε < FABL.relativeHammingDist target outcome.1.evaluate) ≤
    1 / 10

theorem FABL.finiteFamilyFourierEstimatorProgram_failureProbability_le_one_tenth
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (𝒽 : Finset (Finset (Fin n)))
  (h𝒽 : 𝒽.Nonempty)
  (ε : ↑FABL.PositiveLearningParameter)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedOn
      target.toReal (↑↑ε / 2) ↑𝒽) :
  ((FABL.finiteFamilyFourierEstimatorProgram
          𝒽 h𝒽 ε).eventProbability
      target fun outcome =>
      ↑↑ε <
        FABL.relativeHammingDist target
          outcome.1.evaluate) ≤
    1 / 10

O'Donnell, Theorem 3.29, probabilistic conclusion for a nonempty concentrating family: the
scheduled random-example learner returns an `ε`-accurate sparse Fourier hypothesis with probability
at least `9/10`.  Equivalently, its failure probability is at most `1/10`.

Proposition3.4.4

Statement uses 2

Statement dependency previews

Preview

Definition 1.3.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 3

Reverse dependency previews

Preview

Theorem 3.4.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagssection-3-4fidelity-exact

Proposition 3.30. Given random-example access to f:\{-1,1\}^n\to\{-1,1\}, there is a randomized algorithm which takes as input S\subseteq[n] and 0<\delta,\epsilon\le1/2, and outputs an estimate \widetilde f(S) satisfying \Pr\!\left[ |\widetilde f(S)-\widehat f(S)|>\epsilon \right]\le\delta. Its running time is \operatorname{poly}(n,1/\epsilon)\log(1/\delta). Concretely, it takes m=O\!\left(\frac{\log(1/\delta)}{\epsilon^2}\right) independent random examples, makes exactly m random-example calls, and returns the empirical average of the \{-1,1\}-valued samples f(x)\chi_S(x).

Lean code for Proposition3.4.4●13 declarations

abbrevdefined in FABL/Chapter03/LearningTheory/Program.lean

complete

abbrev FABL.PositiveLearningParameter : Set ℚ

abbrev FABL.PositiveLearningParameter : Set ℚ

A strictly positive finite parameter in the range required by Proposition 3.30.

defdefined in FABL/Chapter03/LearningTheory/Program.lean

complete

def FABL.fourierEstimatorFailureBits (δ : ↑FABL.PositiveLearningParameter) :
  ℕ

def FABL.fourierEstimatorFailureBits
  (δ : ↑FABL.PositiveLearningParameter) :
  ℕ

Number of binary confidence bits sufficient to reduce the two-sided failure bound to `δ`.

defdefined in FABL/Chapter03/LearningTheory/Program.lean

complete

def FABL.fourierEstimatorSampleCount
  (ε δ : ↑FABL.PositiveLearningParameter) : ℕ

def FABL.fourierEstimatorSampleCount
  (ε δ :
    ↑FABL.PositiveLearningParameter) :
  ℕ

Computable rational sample scheduler for Proposition 3.30.

theoremdefined in FABL/Chapter03/LearningTheory/Program.lean

complete

theorem FABL.fourierEstimatorSampleCount_cast_le
  (ε δ : ↑FABL.PositiveLearningParameter) :
  ↑(FABL.fourierEstimatorSampleCount ε δ) ≤
    4 * ↑(FABL.fourierEstimatorFailureBits δ) / ↑ε ^ 2

theorem FABL.fourierEstimatorSampleCount_cast_le
  (ε δ :
    ↑FABL.PositiveLearningParameter) :
  ↑(FABL.fourierEstimatorSampleCount ε
        δ) ≤
    4 *
        ↑(FABL.fourierEstimatorFailureBits
            δ) /
      ↑ε ^ 2

Explicit polynomial/logarithmic sample bound: the scheduler is at most four times the binary
confidence-bit count divided by `ε²`. The bit count is definitionally
`clog₂ ⌈2 / δ⌉`.

defdefined in FABL/Chapter03/LearningTheory/FourierEstimation.lean

complete

def FABL.rationalFourierObservation {n : ℕ} (S : Finset (Fin n))
  (labeledSample : FABL.SignCube n × FABL.Sign) : ℚ

def FABL.rationalFourierObservation {n : ℕ}
  (S : Finset (Fin n))
  (labeledSample :
    FABL.SignCube n × FABL.Sign) :
  ℚ

The rational observation whose expectation is the Fourier coefficient indexed by `S`.

defdefined in FABL/Chapter03/LearningTheory/FourierEstimation.lean

complete

def FABL.empiricalFourierCoeff {n : ℕ} (S : Finset (Fin n)) {m : ℕ}
  (samples : Fin m → FABL.SignCube n × FABL.Sign) : ℚ

def FABL.empiricalFourierCoeff {n : ℕ}
  (S : Finset (Fin n)) {m : ℕ}
  (samples :
    Fin m → FABL.SignCube n × FABL.Sign) :
  ℚ

Empirical average of `m` rational Fourier observations. Division by zero has its field
convention; the concentration theorem below assumes `m > 0`.

defdefined in FABL/Chapter03/LearningTheory/FourierEstimation.lean

complete

def FABL.finiteUniformEmpiricalMean.{u_1} {Ω : Type u_1} [Fintype Ω]
  (observation : Ω → ℝ) {m : ℕ} (samples : Fin m → Ω) : ℝ

def FABL.finiteUniformEmpiricalMean.{u_1}
  {Ω : Type u_1} [Fintype Ω]
  (observation : Ω → ℝ) {m : ℕ}
  (samples : Fin m → Ω) : ℝ

Empirical mean of a real observation on a finite uniform sample.

theoremdefined in FABL/Chapter03/LearningTheory/FourierEstimation.lean

complete

theorem FABL.measure_finiteUniformEmpiricalMean_sub_expect_ge_le.{u_1}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] [MeasurableSpace Ω]
  [MeasurableSingletonClass Ω] (observation : Ω → ℝ)
  (hobservation : ∀ (x : Ω), observation x ∈ Set.Icc (-1) 1) {m : ℕ}
  (hm : 0 < m) (ε : ℝ) (hε : 0 ≤ ε) :
  (FABL.uniformPMF (Fin m → Ω)).toMeasure.real
      {samples |
        ε ≤
          |FABL.finiteUniformEmpiricalMean observation samples -
              Finset.univ.expect fun x => observation x|} ≤
    2 * Real.exp (-↑m * ε ^ 2 / 2)

theorem FABL.measure_finiteUniformEmpiricalMean_sub_expect_ge_le.{u_1}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  [MeasurableSpace Ω]
  [MeasurableSingletonClass Ω]
  (observation : Ω → ℝ)
  (hobservation :
    ∀ (x : Ω),
      observation x ∈ Set.Icc (-1) 1)
  {m : ℕ} (hm : 0 < m) (ε : ℝ)
  (hε : 0 ≤ ε) :
  (FABL.uniformPMF
            (Fin m → Ω)).toMeasure.real
      {samples |
        ε ≤
          |FABL.finiteUniformEmpiricalMean
                observation samples -
              Finset.univ.expect fun x =>
                observation x|} ≤
    2 * Real.exp (-↑m * ε ^ 2 / 2)

Two-sided Hoeffding concentration for the empirical mean of any `[-1,1]`-valued observation
on a nonempty finite uniform space.

defdefined in FABL/Chapter03/LearningTheory/FourierEstimation.lean

complete

def FABL.fourierCoeffEstimatorProgram {n : ℕ} (S : Finset (Fin n)) (m : ℕ) :
  FABL.LearningProgram n FABL.LearningAccess.randomExamples ℚ

def FABL.fourierCoeffEstimatorProgram {n : ℕ}
  (S : Finset (Fin n)) (m : ℕ) :
  FABL.LearningProgram n
    FABL.LearningAccess.randomExamples ℚ

The finite random-example program in O'Donnell, Proposition 3.30. It draws exactly `m`
examples and computes their empirical Fourier observation average.

defdefined in FABL/Chapter03/LearningTheory/FourierEstimation.lean

complete

def FABL.scheduledFourierCoeffEstimatorProgram {n : ℕ} (S : Finset (Fin n))
  (ε δ : ↑FABL.PositiveLearningParameter) :
  FABL.LearningProgram n FABL.LearningAccess.randomExamples ℚ

def FABL.scheduledFourierCoeffEstimatorProgram
  {n : ℕ} (S : Finset (Fin n))
  (ε δ :
    ↑FABL.PositiveLearningParameter) :
  FABL.LearningProgram n
    FABL.LearningAccess.randomExamples ℚ

The fully scheduled finite estimator from O'Donnell, Proposition 3.30.

theoremdefined in FABL/Chapter03/LearningTheory/FourierEstimation.lean

complete

theorem FABL.runWithCost_scheduledFourierCoeffEstimatorProgram {n : ℕ}
  (target : FABL.BooleanFunction n) (S : Finset (Fin n))
  (ε δ : ↑FABL.PositiveLearningParameter) :
  FABL.LearningProgram.runWithCost target
      (FABL.scheduledFourierCoeffEstimatorProgram S ε δ) =
    PMF.map
      (fun sampleInputs =>
        (FABL.empiricalFourierCoeff S fun i =>
            (sampleInputs i, target (sampleInputs i)),
          { randomExamples := FABL.fourierEstimatorSampleCount ε δ,
            queries := 0,
            work :=
              FABL.fourierEstimatorSampleCount ε δ +
                FABL.fourierEstimatorSampleCount ε δ * (S.card + 1) }))
      (FABL.uniformPMF
        (Fin (FABL.fourierEstimatorSampleCount ε δ) → FABL.SignCube n))

theorem FABL.runWithCost_scheduledFourierCoeffEstimatorProgram
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (S : Finset (Fin n))
  (ε δ :
    ↑FABL.PositiveLearningParameter) :
  FABL.LearningProgram.runWithCost target
      (FABL.scheduledFourierCoeffEstimatorProgram
        S ε δ) =
    PMF.map
      (fun sampleInputs =>
        (FABL.empiricalFourierCoeff S
            fun i =>
            (sampleInputs i,
              target (sampleInputs i)),
          {
            randomExamples :=
              FABL.fourierEstimatorSampleCount
                ε δ,
            queries := 0,
            work :=
              FABL.fourierEstimatorSampleCount
                  ε δ +
                FABL.fourierEstimatorSampleCount
                    ε δ *
                  (S.card + 1) }))
      (FABL.uniformPMF
        (Fin
            (FABL.fourierEstimatorSampleCount
              ε δ) →
          FABL.SignCube n))

Exact output law and pathwise cost of the scheduled Proposition 3.30 estimator.

theoremdefined in FABL/Chapter03/LearningTheory/FourierEstimation.lean

complete

theorem FABL.scheduledFourierCoeffEstimatorProgram_cost_eq {n : ℕ}
  (target : FABL.BooleanFunction n) (S : Finset (Fin n))
  (ε δ : ↑FABL.PositiveLearningParameter)
  (outcome : ℚ × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.scheduledFourierCoeffEstimatorProgram S ε δ)).support) :
  outcome.2 =
    { randomExamples := FABL.fourierEstimatorSampleCount ε δ,
      queries := 0,
      work :=
        FABL.fourierEstimatorSampleCount ε δ +
          FABL.fourierEstimatorSampleCount ε δ * (S.card + 1) }

theorem FABL.scheduledFourierCoeffEstimatorProgram_cost_eq
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (S : Finset (Fin n))
  (ε δ : ↑FABL.PositiveLearningParameter)
  (outcome : ℚ × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.scheduledFourierCoeffEstimatorProgram
            S ε δ)).support) :
  outcome.2 =
    {
      randomExamples :=
        FABL.fourierEstimatorSampleCount ε
          δ,
      queries := 0,
      work :=
        FABL.fourierEstimatorSampleCount ε
            δ +
          FABL.fourierEstimatorSampleCount
              ε δ *
            (S.card + 1) }

Every scheduled estimator execution uses exactly the constructor-derived sample and work
counts, independently of the target and sampled inputs.

theoremdefined in FABL/Chapter03/LearningTheory/FourierEstimation.lean

complete

theorem FABL.scheduledFourierCoeffEstimatorProgram_failureProbability_le {n : ℕ}
  (target : FABL.BooleanFunction n) (S : Finset (Fin n))
  (ε δ : ↑FABL.PositiveLearningParameter) :
  ((FABL.scheduledFourierCoeffEstimatorProgram S ε δ).eventProbability
      target fun outcome =>
      ↑↑ε ≤ |↑outcome.1 - FABL.fourierCoeff target.toReal S|) ≤
    ↑↑δ

theorem FABL.scheduledFourierCoeffEstimatorProgram_failureProbability_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (S : Finset (Fin n))
  (ε δ :
    ↑FABL.PositiveLearningParameter) :
  ((FABL.scheduledFourierCoeffEstimatorProgram
          S ε δ).eventProbability
      target fun outcome =>
      ↑↑ε ≤
        |↑outcome.1 -
            FABL.fourierCoeff
              target.toReal S|) ≤
    ↑↑δ

O'Donnell, Proposition 3.30: from random examples, the scheduled finite program estimates the
specified Fourier coefficient to additive error `ε`, except with probability at most `δ`.

Proposition3.4.5

uses 1used by 1✓L∃∀N

Tagssection-3-4fidelity-exact

Proposition 3.31. Suppose that f:\{-1,1\}^n\to\{-1,1\} and g:\{-1,1\}^n\to\mathbb R satisfy \|f-g\|_2^2\le\epsilon. Define h:\{-1,1\}^n\to\{-1,1\} by h(x)=\operatorname{sgn}(g(x)), choosing either value in \{-1,1\} when g(x)=0. Then \operatorname{dist}(f,h)\le\epsilon.

Lean code for Proposition3.4.5●3 theorems

theoremdefined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

theorem FABL.indicator_ne_thresholdSign_le_sq (s : FABL.Sign) (t : ℝ) :
  (if s ≠ FABL.thresholdSign t then 1 else 0) ≤
    (FABL.signValue s - t) ^ 2

theorem FABL.indicator_ne_thresholdSign_le_sq
  (s : FABL.Sign) (t : ℝ) :
  (if s ≠ FABL.thresholdSign t then 1
    else 0) ≤
    (FABL.signValue s - t) ^ 2

Pointwise sign rounding has disagreement indicator at most squared approximation error.

theoremdefined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

theorem FABL.relativeHammingDist_thresholdSign_le_uniformLpNorm_two_sq {n : ℕ}
  (f : FABL.BooleanFunction n) (g : FABL.SignCube n → ℝ) :
  (FABL.relativeHammingDist f fun x => FABL.thresholdSign (g x)) ≤
    (FABL.uniformLpNorm 2 fun x => f.toReal x - g x) ^ 2

theorem FABL.relativeHammingDist_thresholdSign_le_uniformLpNorm_two_sq
  {n : ℕ} (f : FABL.BooleanFunction n)
  (g : FABL.SignCube n → ℝ) :
  (FABL.relativeHammingDist f fun x =>
      FABL.thresholdSign (g x)) ≤
    (FABL.uniformLpNorm 2 fun x =>
        f.toReal x - g x) ^
      2

The normalized squared L² error controls relative Hamming distance after sign rounding.

theoremdefined in FABL/Chapter03/LearningTheory/LearningModel.lean

complete

theorem FABL.relativeHammingDist_thresholdSign_le_of_uniformLpNorm_two_sq_le
  {n : ℕ} (f : FABL.BooleanFunction n) (g : FABL.SignCube n → ℝ) (ε : ℝ)
  (herror : (FABL.uniformLpNorm 2 fun x => f.toReal x - g x) ^ 2 ≤ ε) :
  (FABL.relativeHammingDist f fun x => FABL.thresholdSign (g x)) ≤ ε

theorem FABL.relativeHammingDist_thresholdSign_le_of_uniformLpNorm_two_sq_le
  {n : ℕ} (f : FABL.BooleanFunction n)
  (g : FABL.SignCube n → ℝ) (ε : ℝ)
  (herror :
    (FABL.uniformLpNorm 2 fun x =>
          f.toReal x - g x) ^
        2 ≤
      ε) :
  (FABL.relativeHammingDist f fun x =>
      FABL.thresholdSign (g x)) ≤
    ε

O'Donnell, Proposition 3.31: sign rounding converts normalized squared L² error into
classification error.

Theorem3.4.6

Statement uses 2

Statement dependency previews

Preview

Definition 3.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 4

Reverse dependency previews

Preview

Corollary 3.4.7

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagssection-3-4fidelity-exact-with-explicit-cardinality-bound

The Low-Degree Algorithm. Let k\ge1, and 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/2-concentrated up to degree k. Then \mathcal C can be learned using only random examples, with error \epsilon and success probability at least 9/10, in time \operatorname{poly}(n^k,1/\epsilon). The output is the sparse Fourier circuit from Theorem 3.29, indexed by \mathcal F_k=\{S\subseteq[n]:|S|\le k\}, \qquad |\mathcal F_k|=\sum_{j=0}^k\binom nj=O(n^k).

Lean code for Theorem3.4.6●13 declarations

defdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

def FABL.lowDegreeFourierFamily (n k : ℕ) : Finset (Finset (Fin n))

def FABL.lowDegreeFourierFamily (n k : ℕ) :
  Finset (Finset (Fin n))

The family of all Fourier frequencies of degree at most `k`.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.mem_lowDegreeFourierFamily {n : ℕ} (S : Finset (Fin n)) (k : ℕ) :
  S ∈ FABL.lowDegreeFourierFamily n k ↔ S.card ≤ k

theorem FABL.mem_lowDegreeFourierFamily {n : ℕ}
  (S : Finset (Fin n)) (k : ℕ) :
  S ∈ FABL.lowDegreeFourierFamily n k ↔
    S.card ≤ k

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.lowDegreeFourierFamily_nonempty (n k : ℕ) :
  (FABL.lowDegreeFourierFamily n k).Nonempty

theorem FABL.lowDegreeFourierFamily_nonempty
  (n k : ℕ) :
  (FABL.lowDegreeFourierFamily n
      k).Nonempty

The low-degree family always contains the empty frequency.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.card_lowDegreeFourierFamily_eq_sum_choose (n k : ℕ) :
  (FABL.lowDegreeFourierFamily n k).card =
    ∑ j ∈ Finset.range (k + 1), n.choose j

theorem FABL.card_lowDegreeFourierFamily_eq_sum_choose
  (n k : ℕ) :
  (FABL.lowDegreeFourierFamily n k).card =
    ∑ j ∈ Finset.range (k + 1), n.choose j

The number of degree-at-most-`k` frequencies is the sum of the first binomial coefficients.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.card_lowDegreeFourierFamily_le (n k : ℕ) :
  (FABL.lowDegreeFourierFamily n k).card ≤ (k + 1) * (n + 1) ^ k

theorem FABL.card_lowDegreeFourierFamily_le
  (n k : ℕ) :
  (FABL.lowDegreeFourierFamily n k).card ≤
    (k + 1) * (n + 1) ^ k

An explicit polynomial bound on the number of low-degree frequencies.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.fourierWeightOutside_lowDegreeFourierFamily {n : ℕ}
  (f : FABL.SignCube n → ℝ) (k : ℕ) :
  FABL.fourierWeightOutside f ↑(FABL.lowDegreeFourierFamily n k) =
    FABL.fourierWeightAbove k f

theorem FABL.fourierWeightOutside_lowDegreeFourierFamily
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (k : ℕ) :
  FABL.fourierWeightOutside f
      ↑(FABL.lowDegreeFourierFamily n k) =
    FABL.fourierWeightAbove k f

Fourier weight outside the low-degree family is exactly the usual high-degree tail.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.isFourierSpectrumConcentratedOn_lowDegreeFourierFamily_iff {n : ℕ}
  (f : FABL.SignCube n → ℝ) (ε : ℝ) (k : ℕ) :
  FABL.IsFourierSpectrumConcentratedOn f ε
      ↑(FABL.lowDegreeFourierFamily n k) ↔
    FABL.IsFourierSpectrumConcentratedUpTo f ε ↑k

theorem FABL.isFourierSpectrumConcentratedOn_lowDegreeFourierFamily_iff
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (ε : ℝ) (k : ℕ) :
  FABL.IsFourierSpectrumConcentratedOn f ε
      ↑(FABL.lowDegreeFourierFamily n k) ↔
    FABL.IsFourierSpectrumConcentratedUpTo
      f ε ↑k

Concentration on the low-degree family is the natural-cutoff form of Definition 3.1.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.fourierWeightAboveReal_antitone {n : ℕ} (f : FABL.SignCube n → ℝ)
  {a b : ℝ} (hab : a ≤ b) :
  FABL.fourierWeightAboveReal b f ≤ FABL.fourierWeightAboveReal a f

theorem FABL.fourierWeightAboveReal_antitone
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  {a b : ℝ} (hab : a ≤ b) :
  FABL.fourierWeightAboveReal b f ≤
    FABL.fourierWeightAboveReal a f

Raising the degree cutoff can only decrease the Fourier tail.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.IsFourierSpectrumConcentratedUpTo.mono_cutoff {n : ℕ}
  {f : FABL.SignCube n → ℝ} {ε a b : ℝ}
  (h : FABL.IsFourierSpectrumConcentratedUpTo f ε a) (hab : a ≤ b) :
  FABL.IsFourierSpectrumConcentratedUpTo f ε b

theorem FABL.IsFourierSpectrumConcentratedUpTo.mono_cutoff
  {n : ℕ} {f : FABL.SignCube n → ℝ}
  {ε a b : ℝ}
  (h :
    FABL.IsFourierSpectrumConcentratedUpTo
      f ε a)
  (hab : a ≤ b) :
  FABL.IsFourierSpectrumConcentratedUpTo f
    ε b

Fourier concentration persists when the degree cutoff is increased.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.IsFourierSpectrumConcentratedUpTo.mono_error {n : ℕ}
  {f : FABL.SignCube n → ℝ} {ε ε' k : ℝ}
  (h : FABL.IsFourierSpectrumConcentratedUpTo f ε k) (hε : ε ≤ ε') :
  FABL.IsFourierSpectrumConcentratedUpTo f ε' k

theorem FABL.IsFourierSpectrumConcentratedUpTo.mono_error
  {n : ℕ} {f : FABL.SignCube n → ℝ}
  {ε ε' k : ℝ}
  (h :
    FABL.IsFourierSpectrumConcentratedUpTo
      f ε k)
  (hε : ε ≤ ε') :
  FABL.IsFourierSpectrumConcentratedUpTo f
    ε' k

Fourier concentration persists when the permitted error is increased.

defdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

def FABL.lowDegreeFourierEstimatorProgram (n k : ℕ)
  (ε : ↑FABL.PositiveLearningParameter) :
  FABL.LearningProgram n FABL.LearningAccess.randomExamples
    (FABL.SparseFourierHypothesis n)

def FABL.lowDegreeFourierEstimatorProgram
  (n k : ℕ)
  (ε : ↑FABL.PositiveLearningParameter) :
  FABL.LearningProgram n
    FABL.LearningAccess.randomExamples
    (FABL.SparseFourierHypothesis n)

The finite random-example program implementing the Low-Degree Algorithm.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.lowDegreeFourierEstimatorProgram_failureProbability_le_one_tenth
  {n : ℕ} (target : FABL.BooleanFunction n) (k : ℕ)
  (ε : ↑FABL.PositiveLearningParameter)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedUpTo target.toReal (↑↑ε / 2) ↑k) :
  ((FABL.lowDegreeFourierEstimatorProgram n k ε).eventProbability target
      fun outcome =>
      ↑↑ε < FABL.relativeHammingDist target outcome.1.evaluate) ≤
    1 / 10

theorem FABL.lowDegreeFourierEstimatorProgram_failureProbability_le_one_tenth
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ)
  (ε : ↑FABL.PositiveLearningParameter)
  (hconcentration :
    FABL.IsFourierSpectrumConcentratedUpTo
      target.toReal (↑↑ε / 2) ↑k) :
  ((FABL.lowDegreeFourierEstimatorProgram
          n k ε).eventProbability
      target fun outcome =>
      ↑↑ε <
        FABL.relativeHammingDist target
          outcome.1.evaluate) ≤
    1 / 10

The Low-Degree Algorithm fails with probability at most `1/10` under its concentration
premise.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.lowDegreeFourierEstimatorProgram_cost_polyBound {n : ℕ}
  (target : FABL.BooleanFunction n) (k : ℕ)
  (ε : ↑FABL.PositiveLearningParameter)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.lowDegreeFourierEstimatorProgram n k ε)).support) :
  ↑outcome.2.randomExamples ≤
      16 * ↑(FABL.lowDegreeFourierFamily n k).card ^ 3 *
          ↑(Nat.clog 2 (20 * (FABL.lowDegreeFourierFamily n k).card)) /
        ↑ε ^ 2 ∧
    outcome.2.queries = 0 ∧
      ↑outcome.2.work ≤
        16 * ↑(FABL.lowDegreeFourierFamily n k).card ^ 3 * (↑n + 2) *
            ↑(Nat.clog 2
                (20 * (FABL.lowDegreeFourierFamily n k).card)) /
          ↑ε ^ 2

theorem FABL.lowDegreeFourierEstimatorProgram_cost_polyBound
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ)
  (ε : ↑FABL.PositiveLearningParameter)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.lowDegreeFourierEstimatorProgram
            n k ε)).support) :
  ↑outcome.2.randomExamples ≤
      16 *
            ↑(FABL.lowDegreeFourierFamily
                    n k).card ^
              3 *
          ↑(Nat.clog 2
              (20 *
                (FABL.lowDegreeFourierFamily
                    n k).card)) /
        ↑ε ^ 2 ∧
    outcome.2.queries = 0 ∧
      ↑outcome.2.work ≤
        16 *
                ↑(FABL.lowDegreeFourierFamily
                        n k).card ^
                  3 *
              (↑n + 2) *
            ↑(Nat.clog 2
                (20 *
                  (FABL.lowDegreeFourierFamily
                      n k).card)) /
          ↑ε ^ 2

Explicit resource bound for every execution of the Low-Degree Algorithm.

Corollary3.4.7

Statement uses 2

Statement dependency previews

Preview

Proposition 3.1.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagssection-3-4fidelity-exact-with-ceiling-explicit

Corollary 3.32. For t\ge1, let \mathcal C= \{f:\{-1,1\}^n\to\{-1,1\}:\mathbf I[f]\le t\}. Then \mathcal C is learnable from random examples with error \epsilon and success probability at least 9/10 in time n^{O(t/\epsilon)}. The Low-Degree Algorithm uses degree k=\lceil2t/\epsilon\rceil.

Lean code for Corollary3.4.7●3 declarations

defdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

def FABL.totalInfluenceLearningDegree (t : ℝ)
  (ε : ↑FABL.PositiveLearningParameter) : ℕ

def FABL.totalInfluenceLearningDegree (t : ℝ)
  (ε : ↑FABL.PositiveLearningParameter) :
  ℕ

Explicit integral degree cutoff used for the bounded-total-influence learner.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.isFourierSpectrumConcentratedUpTo_totalInfluenceLearningDegree
  {n : ℕ} (target : FABL.BooleanFunction n) (t : ℝ)
  (ε : ↑FABL.PositiveLearningParameter)
  (ht : FABL.totalInfluence target.toReal ≤ t) :
  FABL.IsFourierSpectrumConcentratedUpTo target.toReal (↑↑ε / 2)
    ↑(FABL.totalInfluenceLearningDegree t ε)

theorem FABL.isFourierSpectrumConcentratedUpTo_totalInfluenceLearningDegree
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (t : ℝ)
  (ε : ↑FABL.PositiveLearningParameter)
  (ht :
    FABL.totalInfluence target.toReal ≤
      t) :
  FABL.IsFourierSpectrumConcentratedUpTo
    target.toReal (↑↑ε / 2)
    ↑(FABL.totalInfluenceLearningDegree t
        ε)

Proposition 3.2 supplies the concentration premise for the total-influence learner.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.lowDegreeFourierEstimatorProgram_of_totalInfluence_failure_le_one_tenth
  {n : ℕ} (target : FABL.BooleanFunction n) (t : ℝ)
  (ε : ↑FABL.PositiveLearningParameter)
  (ht : FABL.totalInfluence target.toReal ≤ t) :
  ((FABL.lowDegreeFourierEstimatorProgram n
          (FABL.totalInfluenceLearningDegree t ε) ε).eventProbability
      target fun outcome =>
      ↑↑ε < FABL.relativeHammingDist target outcome.1.evaluate) ≤
    1 / 10

theorem FABL.lowDegreeFourierEstimatorProgram_of_totalInfluence_failure_le_one_tenth
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (t : ℝ)
  (ε : ↑FABL.PositiveLearningParameter)
  (ht :
    FABL.totalInfluence target.toReal ≤
      t) :
  ((FABL.lowDegreeFourierEstimatorProgram
          n
          (FABL.totalInfluenceLearningDegree
            t ε)
          ε).eventProbability
      target fun outcome =>
      ↑↑ε <
        FABL.relativeHammingDist target
          outcome.1.evaluate) ≤
    1 / 10

Corollary 3.32: bounded total influence gives a Low-Degree learner.

Corollary3.4.8

Statement uses 3

Statement dependency previews

Preview

Definition 2.1.9

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagssection-3-4fidelity-exact

Corollary 3.33. Let \mathcal C= \{f:\{-1,1\}^n\to\{-1,1\}:f\text{ is monotone}\}. Then \mathcal C is learnable from random examples with error \epsilon and success probability at least 9/10 in time n^{O(\sqrt n/\epsilon)}.

Lean code for Corollary3.4.8●2 declarations

defdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

def FABL.monotoneLearningDegree (n : ℕ)
  (ε : ↑FABL.PositiveLearningParameter) : ℕ

def FABL.monotoneLearningDegree (n : ℕ)
  (ε : ↑FABL.PositiveLearningParameter) :
  ℕ

Degree cutoff used by the monotone-function specialization.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.lowDegreeFourierEstimatorProgram_of_monotone_failure_le_one_tenth
  {n : ℕ} (target : FABL.BooleanFunction n) (htarget : Monotone target)
  (ε : ↑FABL.PositiveLearningParameter) :
  ((FABL.lowDegreeFourierEstimatorProgram n
          (FABL.monotoneLearningDegree n ε) ε).eventProbability
      target fun outcome =>
      ↑↑ε < FABL.relativeHammingDist target outcome.1.evaluate) ≤
    1 / 10

theorem FABL.lowDegreeFourierEstimatorProgram_of_monotone_failure_le_one_tenth
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (htarget : Monotone target)
  (ε : ↑FABL.PositiveLearningParameter) :
  ((FABL.lowDegreeFourierEstimatorProgram
          n
          (FABL.monotoneLearningDegree n
            ε)
          ε).eventProbability
      target fun outcome =>
      ↑↑ε <
        FABL.relativeHammingDist target
          outcome.1.evaluate) ≤
    1 / 10

Corollary 3.33: Theorem 2.33 gives the Low-Degree learner for monotone functions.

Corollary3.4.9

Statement uses 2

Statement dependency previews

Preview

Proposition 3.1.4

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagssection-3-4fidelity-exact-with-ceiling-explicit

Corollary 3.34. For \delta\in(0,1/2], let \mathcal C= \left\{f:\{-1,1\}^n\to\{-1,1\}: \operatorname{NS}_\delta[f]\le\epsilon/6\right\}. Then \mathcal C is learnable from random examples with error \epsilon and success probability at least 9/10 in time \operatorname{poly}(n^{1/\delta},1/\epsilon).

Lean code for Corollary3.4.9●3 declarations

defdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

def FABL.noiseSensitivityLearningDegree (δ : ℝ) : ℕ

def FABL.noiseSensitivityLearningDegree
  (δ : ℝ) : ℕ

Explicit integral degree cutoff used for the noise-sensitivity learner.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.isFourierSpectrumConcentratedUpTo_noiseSensitivityLearningDegree
  {n : ℕ} (target : FABL.BooleanFunction n) (δ : ℝ) (hδpos : 0 < δ)
  (hδhalf : δ ≤ 1 / 2) (ε : ↑FABL.PositiveLearningParameter)
  (hnoise : FABL.noiseSensitivity δ ⋯ target ≤ ↑↑ε / 6) :
  FABL.IsFourierSpectrumConcentratedUpTo target.toReal (↑↑ε / 2)
    ↑(FABL.noiseSensitivityLearningDegree δ)

theorem FABL.isFourierSpectrumConcentratedUpTo_noiseSensitivityLearningDegree
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (δ : ℝ) (hδpos : 0 < δ)
  (hδhalf : δ ≤ 1 / 2)
  (ε : ↑FABL.PositiveLearningParameter)
  (hnoise :
    FABL.noiseSensitivity δ ⋯ target ≤
      ↑↑ε / 6) :
  FABL.IsFourierSpectrumConcentratedUpTo
    target.toReal (↑↑ε / 2)
    ↑(FABL.noiseSensitivityLearningDegree
        δ)

Proposition 3.3 supplies the concentration premise for the noise-sensitivity learner.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.lowDegreeFourierEstimatorProgram_of_noiseSensitivity_failure_le_one_tenth
  {n : ℕ} (target : FABL.BooleanFunction n) (δ : ℝ) (hδpos : 0 < δ)
  (hδhalf : δ ≤ 1 / 2) (ε : ↑FABL.PositiveLearningParameter)
  (hnoise : FABL.noiseSensitivity δ ⋯ target ≤ ↑↑ε / 6) :
  ((FABL.lowDegreeFourierEstimatorProgram n
          (FABL.noiseSensitivityLearningDegree δ) ε).eventProbability
      target fun outcome =>
      ↑↑ε < FABL.relativeHammingDist target outcome.1.evaluate) ≤
    1 / 10

theorem FABL.lowDegreeFourierEstimatorProgram_of_noiseSensitivity_failure_le_one_tenth
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (δ : ℝ) (hδpos : 0 < δ)
  (hδhalf : δ ≤ 1 / 2)
  (ε : ↑FABL.PositiveLearningParameter)
  (hnoise :
    FABL.noiseSensitivity δ ⋯ target ≤
      ↑↑ε / 6) :
  ((FABL.lowDegreeFourierEstimatorProgram
          n
          (FABL.noiseSensitivityLearningDegree
            δ)
          ε).eventProbability
      target fun outcome =>
      ↑↑ε <
        FABL.relativeHammingDist target
          outcome.1.evaluate) ≤
    1 / 10

Corollary 3.34: small noise sensitivity gives a Low-Degree learner.

Corollary3.4.10

Statement uses 3

Statement dependency previews

Preview

Definition 3.2.11

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagssection-3-4fidelity-exact-with-cube-bridge-explicit

Corollary 3.35. Let \mathcal C= \left\{f:\{-1,1\}^n\to\{-1,1\}: \operatorname{DTsize}(f)\le s\right\}. Then \mathcal C is learnable from random examples with error \epsilon and success probability at least 9/10 in time n^{O(\log(s/\epsilon))}.

Lean code for Corollary3.4.10●2 declarations

defdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

def FABL.decisionTreeLearningDegree {n : ℕ} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available)
  (ε : ↑FABL.PositiveLearningParameter) : ℕ

def FABL.decisionTreeLearningDegree {n : ℕ}
  {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available)
  (ε : ↑FABL.PositiveLearningParameter) :
  ℕ

Exact integer cutoff used by the decision-tree specialization.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.lowDegreeFourierEstimatorProgram_of_decisionTree_failure_le_one_tenth
  {n : ℕ} (target : FABL.BooleanFunction n) {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available)
  (hT :
    T.Computes fun x => target.toReal ((FABL.binaryCubeSignEquiv n) x))
  (ε : ↑FABL.PositiveLearningParameter) :
  ((FABL.lowDegreeFourierEstimatorProgram n
          (FABL.decisionTreeLearningDegree T ε) ε).eventProbability
      target fun outcome =>
      ↑↑ε < FABL.relativeHammingDist target outcome.1.evaluate) ≤
    1 / 10

theorem FABL.lowDegreeFourierEstimatorProgram_of_decisionTree_failure_le_one_tenth
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available)
  (hT :
    T.Computes fun x =>
      target.toReal
        ((FABL.binaryCubeSignEquiv n) x))
  (ε : ↑FABL.PositiveLearningParameter) :
  ((FABL.lowDegreeFourierEstimatorProgram
          n
          (FABL.decisionTreeLearningDegree
            T ε)
          ε).eventProbability
      target fun outcome =>
      ↑↑ε <
        FABL.relativeHammingDist target
          outcome.1.evaluate) ≤
    1 / 10

Corollary 3.35: a small decision tree supplies the Low-Degree concentration premise.

Theorem3.4.11

Statement uses 3

Statement dependency previews

Preview

Definition 3.2.10

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagssection-3-4fidelity-exact-with-explicit-scheduler-bound

Theorem 3.36. Let k\ge1, and let \mathcal C= \{f:\{-1,1\}^n\to\{-1,1\}:\deg(f)\le k\}. Then \mathcal C is learnable from random examples with error 0 and success probability at least 9/10 in time n^k\operatorname{poly}(n,2^k). In particular, this class contains all functions computed by decision trees of depth at most k. The learner outputs a finite sparse Fourier circuit which computes the target exactly on every input.

The production learner uses a positive rational accuracy scheduler. If m_{n,k} is its number of samples per coefficient, Lean proves the exact pathwise cost \left( |\mathcal F_k|m_{n,k},\ 0,\ |\mathcal F_k|m_{n,k}+|\mathcal F_k|m_{n,k}(n+1) \right) and the explicit bound m_{n,k}\le \frac{4\,\operatorname{clog}_2(20|\mathcal F_k|)} {(2^{-(k+1)})^2}. Together with |\mathcal F_k|=O(n^k), this is the displayed n^k\operatorname{poly}(n,2^k) running-time bound.

Lean code for Theorem3.4.11●11 declarations

theoremdefined in FABL/Chapter03/LearningTheory/FiniteFamily.lean

complete

theorem FABL.finiteFamilyCoefficientFailureBits_eq {n : ℕ}
  (𝓕 : Finset (Finset (Fin n))) (h𝓕 : 𝓕.Nonempty) :
  FABL.fourierEstimatorFailureBits
      (FABL.finiteFamilyCoefficientConfidence 𝓕 h𝓕) =
    Nat.clog 2 (20 * 𝓕.card)

theorem FABL.finiteFamilyCoefficientFailureBits_eq
  {n : ℕ} (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty) :
  FABL.fourierEstimatorFailureBits
      (FABL.finiteFamilyCoefficientConfidence
        𝓕 h𝓕) =
    Nat.clog 2 (20 * 𝓕.card)

The family confidence budget has the explicit binary logarithmic scheduler
`clog₂ (20|𝓕|)`.

defdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

def FABL.exactDegreeSamplesPerCoefficient (n k : ℕ) : ℕ

def FABL.exactDegreeSamplesPerCoefficient
  (n k : ℕ) : ℕ

Samples per low-degree coefficient used by the exact Fourier learner.

defdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

def FABL.exactDegreeFourierEstimatorLabeledOutput (n k : ℕ)
  (samples :
    ↥(FABL.lowDegreeFourierFamily n k) →
      Fin (FABL.exactDegreeSamplesPerCoefficient n k) →
        FABL.SignCube n × FABL.Sign) :
  FABL.SparseFourierHypothesis n

def FABL.exactDegreeFourierEstimatorLabeledOutput
  (n k : ℕ)
  (samples :
    ↥(FABL.lowDegreeFourierFamily n k) →
      Fin
          (FABL.exactDegreeSamplesPerCoefficient
            n k) →
        FABL.SignCube n × FABL.Sign) :
  FABL.SparseFourierHypothesis n

Rounded sparse Fourier output computed from a matrix of labeled random examples.

defdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

def FABL.exactDegreeFourierEstimatorProgram (n k : ℕ) :
  FABL.LearningProgram n FABL.LearningAccess.randomExamples
    (FABL.SparseFourierHypothesis n)

def FABL.exactDegreeFourierEstimatorProgram
  (n k : ℕ) :
  FABL.LearningProgram n
    FABL.LearningAccess.randomExamples
    (FABL.SparseFourierHypothesis n)

The random-example exact learner for sign functions of Fourier degree at most `k`.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.runWithCost_exactDegreeFourierEstimatorProgram {n : ℕ}
  (target : FABL.BooleanFunction n) (k : ℕ) :
  FABL.LearningProgram.runWithCost target
      (FABL.exactDegreeFourierEstimatorProgram n k) =
    FABL.LearningProgram.randomExampleMatrixOutputLaw target
      (FABL.lowDegreeFourierFamily n k)
      (FABL.exactDegreeSamplesPerCoefficient n k)
      ((FABL.lowDegreeFourierFamily n k).card *
          FABL.exactDegreeSamplesPerCoefficient n k *
        (n + 1))
      (FABL.exactDegreeFourierEstimatorLabeledOutput n k)

theorem FABL.runWithCost_exactDegreeFourierEstimatorProgram
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ) :
  FABL.LearningProgram.runWithCost target
      (FABL.exactDegreeFourierEstimatorProgram
        n k) =
    FABL.LearningProgram.randomExampleMatrixOutputLaw
      target
      (FABL.lowDegreeFourierFamily n k)
      (FABL.exactDegreeSamplesPerCoefficient
        n k)
      ((FABL.lowDegreeFourierFamily n
              k).card *
          FABL.exactDegreeSamplesPerCoefficient
            n k *
        (n + 1))
      (FABL.exactDegreeFourierEstimatorLabeledOutput
        n k)

The exact learner is interpreted by the corresponding finite matrix-output law.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.exactDegreeFourierEstimatorProgram_cost_eq {n : ℕ}
  (target : FABL.BooleanFunction n) (k : ℕ)
  (outcome : FABL.SparseFourierHypothesis n × FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost target
          (FABL.exactDegreeFourierEstimatorProgram n k)).support) :
  outcome.2 =
    {
      randomExamples :=
        (FABL.lowDegreeFourierFamily n k).card *
          FABL.exactDegreeSamplesPerCoefficient n k,
      queries := 0,
      work :=
        (FABL.lowDegreeFourierFamily n k).card *
            FABL.exactDegreeSamplesPerCoefficient n k +
          (FABL.lowDegreeFourierFamily n k).card *
              FABL.exactDegreeSamplesPerCoefficient n k *
            (n + 1) }

theorem FABL.exactDegreeFourierEstimatorProgram_cost_eq
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ)
  (outcome :
    FABL.SparseFourierHypothesis n ×
      FABL.LearningCost)
  (houtcome :
    outcome ∈
      (FABL.LearningProgram.runWithCost
          target
          (FABL.exactDegreeFourierEstimatorProgram
            n k)).support) :
  outcome.2 =
    {
      randomExamples :=
        (FABL.lowDegreeFourierFamily n
              k).card *
          FABL.exactDegreeSamplesPerCoefficient
            n k,
      queries := 0,
      work :=
        (FABL.lowDegreeFourierFamily n
                k).card *
            FABL.exactDegreeSamplesPerCoefficient
              n k +
          (FABL.lowDegreeFourierFamily n
                  k).card *
              FABL.exactDegreeSamplesPerCoefficient
                n k *
            (n + 1) }

Every execution of the exact learner has the stated target-independent resource cost.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.exactDegreeSamplesPerCoefficient_cast_le (n k : ℕ) :
  ↑(FABL.exactDegreeSamplesPerCoefficient n k) ≤
    4 *
        ↑(FABL.fourierEstimatorFailureBits
            (FABL.finiteFamilyCoefficientConfidence
              (FABL.lowDegreeFourierFamily n k) ⋯)) /
      ↑(FABL.degreeFourierCoefficientAccuracy k) ^ 2

theorem FABL.exactDegreeSamplesPerCoefficient_cast_le
  (n k : ℕ) :
  ↑(FABL.exactDegreeSamplesPerCoefficient
        n k) ≤
    4 *
        ↑(FABL.fourierEstimatorFailureBits
            (FABL.finiteFamilyCoefficientConfidence
              (FABL.lowDegreeFourierFamily
                n k)
              ⋯)) /
      ↑(FABL.degreeFourierCoefficientAccuracy
            k) ^
        2

Direct scheduler bound for the number of samples used to estimate one exact coefficient.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.measure_exactDegreeFourierEstimatorOutput_failure_le_one_tenth
  {n : ℕ} (target : FABL.BooleanFunction n) (k : ℕ) (hk : 1 ≤ k)
  (hdegree : FABL.fourierDegree target.toReal ≤ k) :
  (FABL.LearningProgram.randomExampleMatrixInputLaw
            (FABL.lowDegreeFourierFamily n k)
            (FABL.exactDegreeSamplesPerCoefficient n k)).toMeasure.real
      {sampleInputs |
        (FABL.exactDegreeFourierEstimatorOutput target k
              sampleInputs).evaluate ≠
          target} ≤
    1 / 10

theorem FABL.measure_exactDegreeFourierEstimatorOutput_failure_le_one_tenth
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ) (hk : 1 ≤ k)
  (hdegree :
    FABL.fourierDegree target.toReal ≤
      k) :
  (FABL.LearningProgram.randomExampleMatrixInputLaw
            (FABL.lowDegreeFourierFamily n
              k)
            (FABL.exactDegreeSamplesPerCoefficient
              n k)).toMeasure.real
      {sampleInputs |
        (FABL.exactDegreeFourierEstimatorOutput
              target k
              sampleInputs).evaluate ≠
          target} ≤
    1 / 10

With probability at least `9/10`, rounded empirical coefficients recover a bounded-degree
target exactly.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.exactDegreeFourierEstimatorProgram_failureProbability_le_one_tenth
  {n : ℕ} (target : FABL.BooleanFunction n) (k : ℕ) (hk : 1 ≤ k)
  (hdegree : FABL.fourierDegree target.toReal ≤ k) :
  ((FABL.exactDegreeFourierEstimatorProgram n k).eventProbability target
      fun outcome => outcome.1.evaluate ≠ target) ≤
    1 / 10

theorem FABL.exactDegreeFourierEstimatorProgram_failureProbability_le_one_tenth
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ) (hk : 1 ≤ k)
  (hdegree :
    FABL.fourierDegree target.toReal ≤
      k) :
  ((FABL.exactDegreeFourierEstimatorProgram
          n k).eventProbability
      target fun outcome =>
      outcome.1.evaluate ≠ target) ≤
    1 / 10

The exact learner fails to return the target with probability at most `1/10`.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.fourierDegree_toReal_le_depth_of_decisionTree {n : ℕ}
  (target : FABL.BooleanFunction n) {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available)
  (hT :
    T.Computes fun x =>
      target.toReal ((FABL.binaryCubeSignEquiv n) x)) :
  FABL.fourierDegree target.toReal ≤ T.depth

theorem FABL.fourierDegree_toReal_le_depth_of_decisionTree
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available)
  (hT :
    T.Computes fun x =>
      target.toReal
        ((FABL.binaryCubeSignEquiv n)
          x)) :
  FABL.fourierDegree target.toReal ≤
    T.depth

A Boolean target computed by a decision tree has Fourier degree at most the tree depth.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.exactDegreeFourierEstimatorProgram_of_decisionTree_failureProbability_le_one_tenth
  {n : ℕ} (target : FABL.BooleanFunction n) (k : ℕ) (hk : 1 ≤ k)
  {available : Finset (Fin n)} (T : FABL.F₂DecisionTree n ℝ available)
  (hT :
    T.Computes fun x => target.toReal ((FABL.binaryCubeSignEquiv n) x))
  (hdepth : T.depth ≤ k) :
  ((FABL.exactDegreeFourierEstimatorProgram n k).eventProbability target
      fun outcome => outcome.1.evaluate ≠ target) ≤
    1 / 10

theorem FABL.exactDegreeFourierEstimatorProgram_of_decisionTree_failureProbability_le_one_tenth
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ) (hk : 1 ≤ k)
  {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available)
  (hT :
    T.Computes fun x =>
      target.toReal
        ((FABL.binaryCubeSignEquiv n) x))
  (hdepth : T.depth ≤ k) :
  ((FABL.exactDegreeFourierEstimatorProgram
          n k).eventProbability
      target fun outcome =>
      outcome.1.evaluate ≠ target) ≤
    1 / 10

Theorem 3.36: a decision tree of depth at most `k` is exactly learnable from random examples
with success probability at least `9/10`.

Lemma3.4.12

Statement uses 5

Statement dependency previews

Preview

Theorem 1.2.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagssection-3-4supportfidelity-exact

Exercise 3.36. Prove the exact-learning assertion of Theorem 3.36: for k\ge1, the class of Boolean functions of degree at most k is learnable from random examples with error 0, success probability at least 9/10, and running time n^k\operatorname{poly}(n,2^k). The required exact-recovery guarantee uses the following assertion from Exercise 1.11: if a Boolean function has degree at most k, each of its Fourier coefficients is an integer multiple of 2^{1-k}. Thus simultaneous estimates of all degree-at-most-k coefficients to strictly less than half this spacing can be rounded to their unique exact values; their Fourier expansion then gives a sparse circuit computing f exactly. The learner uses at most \sum_{j=0}^k\binom nj=O(n^k) coefficient estimations, with the individual confidence budgets chosen so that all roundings are correct with probability at least 9/10.

Lean code for Lemma3.4.12●14 declarations

defdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

def FABL.degreeFourierGranularity (k : ℕ) : ℚ

def FABL.degreeFourierGranularity (k : ℕ) : ℚ

Fourier coefficients of a degree-`k` sign-valued function lie on this rational lattice.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.degreeFourierGranularity_pos (k : ℕ) :
  0 < FABL.degreeFourierGranularity k

theorem FABL.degreeFourierGranularity_pos
  (k : ℕ) :
  0 < FABL.degreeFourierGranularity k

The degree-`k` Fourier granularity is strictly positive.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.degreeFourierGranularity_cast (k : ℕ) :
  ↑(FABL.degreeFourierGranularity k) = 2 * 2⁻¹ ^ k

theorem FABL.degreeFourierGranularity_cast
  (k : ℕ) :
  ↑(FABL.degreeFourierGranularity k) =
    2 * 2⁻¹ ^ k

Coercing the rational Fourier granularity gives the corresponding real lattice spacing.

defdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

def FABL.roundToDegreeFourierGranularity (k : ℕ) (q : ℚ) : ℚ

def FABL.roundToDegreeFourierGranularity
  (k : ℕ) (q : ℚ) : ℚ

Round a rational coefficient estimate to the nearest degree-`k` Fourier lattice point.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.roundToDegreeFourierGranularity_eq_of_close (k : ℕ) (q : ℚ) (z : ℤ)
  (hclose :
    |↑q - ↑z * ↑(FABL.degreeFourierGranularity k)| <
      ↑(FABL.degreeFourierGranularity k) / 2) :
  FABL.roundToDegreeFourierGranularity k q =
    ↑z * FABL.degreeFourierGranularity k

theorem FABL.roundToDegreeFourierGranularity_eq_of_close
  (k : ℕ) (q : ℚ) (z : ℤ)
  (hclose :
    |↑q -
          ↑z *
            ↑(FABL.degreeFourierGranularity
                k)| <
      ↑(FABL.degreeFourierGranularity k) /
        2) :
  FABL.roundToDegreeFourierGranularity k
      q =
    ↑z * FABL.degreeFourierGranularity k

Any estimate within half a lattice spacing rounds to the prescribed lattice point.

defdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

def FABL.degreeFourierCoefficientAccuracy (k : ℕ) :
  ↑FABL.PositiveLearningParameter

def FABL.degreeFourierCoefficientAccuracy
  (k : ℕ) :
  ↑FABL.PositiveLearningParameter

Per-coefficient accuracy sufficient for exact recovery on the degree-`k` Fourier lattice.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.degreeFourierCoefficientAccuracy_value (k : ℕ) :
  ↑(FABL.degreeFourierCoefficientAccuracy k) = 2⁻¹ ^ (k + 1)

theorem FABL.degreeFourierCoefficientAccuracy_value
  (k : ℕ) :
  ↑(FABL.degreeFourierCoefficientAccuracy
        k) =
    2⁻¹ ^ (k + 1)

The exact-recovery accuracy is `2⁻(k+1)`.

defdefined in FABL/Chapter03/LearningTheory/FiniteFamily.lean

complete

def FABL.finiteFamilyCoefficientBadSetWithParameters {n : ℕ}
  (target : FABL.BooleanFunction n) (𝓕 : Finset (Finset (Fin n)))
  (accuracy confidence : ↑FABL.PositiveLearningParameter) (S : ↥𝓕) :
  Set
    (↥𝓕 →
      Fin (FABL.fourierEstimatorSampleCount accuracy confidence) →
        FABL.SignCube n)

def FABL.finiteFamilyCoefficientBadSetWithParameters
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n)))
  (accuracy confidence :
    ↑FABL.PositiveLearningParameter)
  (S : ↥𝓕) :
  Set
    (↥𝓕 →
      Fin
          (FABL.fourierEstimatorSampleCount
            accuracy confidence) →
        FABL.SignCube n)

Failure event for one row of a finite coefficient-estimation matrix, with independently
specified accuracy and confidence parameters.

theoremdefined in FABL/Chapter03/LearningTheory/FiniteFamily.lean

complete

theorem FABL.measure_finiteFamilyCoefficientBadSetWithParameters_le {n : ℕ}
  (target : FABL.BooleanFunction n) (𝓕 : Finset (Finset (Fin n)))
  (accuracy confidence : ↑FABL.PositiveLearningParameter) (S : ↥𝓕) :
  (FABL.LearningProgram.randomExampleMatrixInputLaw 𝓕
            (FABL.fourierEstimatorSampleCount accuracy
              confidence)).toMeasure.real
      (FABL.finiteFamilyCoefficientBadSetWithParameters target 𝓕
        accuracy confidence S) ≤
    ↑↑confidence

theorem FABL.measure_finiteFamilyCoefficientBadSetWithParameters_le
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n)))
  (accuracy confidence :
    ↑FABL.PositiveLearningParameter)
  (S : ↥𝓕) :
  (FABL.LearningProgram.randomExampleMatrixInputLaw
            𝓕
            (FABL.fourierEstimatorSampleCount
              accuracy
              confidence)).toMeasure.real
      (FABL.finiteFamilyCoefficientBadSetWithParameters
        target 𝓕 accuracy confidence S) ≤
    ↑↑confidence

A fixed row violates its requested accuracy with probability at most its confidence
budget.

theoremdefined in FABL/Chapter03/LearningTheory/FiniteFamily.lean

complete

theorem FABL.measure_finiteFamily_someCoefficientBadSetWithParameters_le_one_tenth
  {n : ℕ} (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n))) (h𝓕 : 𝓕.Nonempty)
  (accuracy : ↑FABL.PositiveLearningParameter) :
  (FABL.LearningProgram.randomExampleMatrixInputLaw 𝓕
            (FABL.fourierEstimatorSampleCount accuracy
              (FABL.finiteFamilyCoefficientConfidence 𝓕
                h𝓕))).toMeasure.real
      (⋃ S,
        FABL.finiteFamilyCoefficientBadSetWithParameters target 𝓕
          accuracy (FABL.finiteFamilyCoefficientConfidence 𝓕 h𝓕) S) ≤
    1 / 10

theorem FABL.measure_finiteFamily_someCoefficientBadSetWithParameters_le_one_tenth
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (𝓕 : Finset (Finset (Fin n)))
  (h𝓕 : 𝓕.Nonempty)
  (accuracy :
    ↑FABL.PositiveLearningParameter) :
  (FABL.LearningProgram.randomExampleMatrixInputLaw
            𝓕
            (FABL.fourierEstimatorSampleCount
              accuracy
              (FABL.finiteFamilyCoefficientConfidence
                𝓕 h𝓕))).toMeasure.real
      (⋃ S,
        FABL.finiteFamilyCoefficientBadSetWithParameters
          target 𝓕 accuracy
          (FABL.finiteFamilyCoefficientConfidence
            𝓕 h𝓕)
          S) ≤
    1 / 10

With confidence `1/(10|𝓕|)`, the probability that any row violates an arbitrary requested
accuracy is at most `1/10`.

defdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

def FABL.exactDegreeFourierEstimatorOutput {n : ℕ}
  (target : FABL.BooleanFunction n) (k : ℕ)
  (sampleInputs :
    ↥(FABL.lowDegreeFourierFamily n k) →
      Fin (FABL.exactDegreeSamplesPerCoefficient n k) →
        FABL.SignCube n) :
  FABL.SparseFourierHypothesis n

def FABL.exactDegreeFourierEstimatorOutput
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ)
  (sampleInputs :
    ↥(FABL.lowDegreeFourierFamily n k) →
      Fin
          (FABL.exactDegreeSamplesPerCoefficient
            n k) →
        FABL.SignCube n) :
  FABL.SparseFourierHypothesis n

Rounded sparse Fourier output reconstructed from a matrix of unlabeled sample inputs.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.exactDegreeFourierEstimatorOutput_coefficient_cast_eq {n : ℕ}
  (target : FABL.BooleanFunction n) (k : ℕ) (hk : 1 ≤ k)
  (hdegree : FABL.fourierDegree target.toReal ≤ k)
  (sampleInputs :
    ↥(FABL.lowDegreeFourierFamily n k) →
      Fin (FABL.exactDegreeSamplesPerCoefficient n k) → FABL.SignCube n)
  (hgood :
    ∀ (S : ↥(FABL.lowDegreeFourierFamily n k)),
      sampleInputs ∉
        FABL.finiteFamilyCoefficientBadSetWithParameters target
          (FABL.lowDegreeFourierFamily n k)
          (FABL.degreeFourierCoefficientAccuracy k)
          (FABL.finiteFamilyCoefficientConfidence
            (FABL.lowDegreeFourierFamily n k) ⋯)
          S)
  (S : ↥(FABL.lowDegreeFourierFamily n k)) :
  ↑((FABL.exactDegreeFourierEstimatorOutput target k
            sampleInputs).coefficient
        S) =
    FABL.fourierCoeff target.toReal ↑S

theorem FABL.exactDegreeFourierEstimatorOutput_coefficient_cast_eq
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ) (hk : 1 ≤ k)
  (hdegree :
    FABL.fourierDegree target.toReal ≤ k)
  (sampleInputs :
    ↥(FABL.lowDegreeFourierFamily n k) →
      Fin
          (FABL.exactDegreeSamplesPerCoefficient
            n k) →
        FABL.SignCube n)
  (hgood :
    ∀
      (S :
        ↥(FABL.lowDegreeFourierFamily n
            k)),
      sampleInputs ∉
        FABL.finiteFamilyCoefficientBadSetWithParameters
          target
          (FABL.lowDegreeFourierFamily n
            k)
          (FABL.degreeFourierCoefficientAccuracy
            k)
          (FABL.finiteFamilyCoefficientConfidence
            (FABL.lowDegreeFourierFamily n
              k)
            ⋯)
          S)
  (S :
    ↥(FABL.lowDegreeFourierFamily n k)) :
  ↑((FABL.exactDegreeFourierEstimatorOutput
            target k
            sampleInputs).coefficient
        S) =
    FABL.fourierCoeff target.toReal ↑S

If every empirical coefficient is accurate, rounding recovers each true degree-`k`
coefficient exactly.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.exactDegreeFourierEstimatorOutput_realValue_eq {n : ℕ}
  (target : FABL.BooleanFunction n) (k : ℕ) (hk : 1 ≤ k)
  (hdegree : FABL.fourierDegree target.toReal ≤ k)
  (sampleInputs :
    ↥(FABL.lowDegreeFourierFamily n k) →
      Fin (FABL.exactDegreeSamplesPerCoefficient n k) → FABL.SignCube n)
  (hgood :
    ∀ (S : ↥(FABL.lowDegreeFourierFamily n k)),
      sampleInputs ∉
        FABL.finiteFamilyCoefficientBadSetWithParameters target
          (FABL.lowDegreeFourierFamily n k)
          (FABL.degreeFourierCoefficientAccuracy k)
          (FABL.finiteFamilyCoefficientConfidence
            (FABL.lowDegreeFourierFamily n k) ⋯)
          S) :
  (FABL.exactDegreeFourierEstimatorOutput target k
        sampleInputs).realValue =
    target.toReal

theorem FABL.exactDegreeFourierEstimatorOutput_realValue_eq
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ) (hk : 1 ≤ k)
  (hdegree :
    FABL.fourierDegree target.toReal ≤ k)
  (sampleInputs :
    ↥(FABL.lowDegreeFourierFamily n k) →
      Fin
          (FABL.exactDegreeSamplesPerCoefficient
            n k) →
        FABL.SignCube n)
  (hgood :
    ∀
      (S :
        ↥(FABL.lowDegreeFourierFamily n
            k)),
      sampleInputs ∉
        FABL.finiteFamilyCoefficientBadSetWithParameters
          target
          (FABL.lowDegreeFourierFamily n
            k)
          (FABL.degreeFourierCoefficientAccuracy
            k)
          (FABL.finiteFamilyCoefficientConfidence
            (FABL.lowDegreeFourierFamily n
              k)
            ⋯)
          S) :
  (FABL.exactDegreeFourierEstimatorOutput
        target k sampleInputs).realValue =
    target.toReal

Exact recovery of every low-degree coefficient recovers the target's real Fourier
expansion.

theoremdefined in FABL/Chapter03/LearningTheory/LowDegree.lean

complete

theorem FABL.exactDegreeFourierEstimatorOutput_evaluate_eq {n : ℕ}
  (target : FABL.BooleanFunction n) (k : ℕ) (hk : 1 ≤ k)
  (hdegree : FABL.fourierDegree target.toReal ≤ k)
  (sampleInputs :
    ↥(FABL.lowDegreeFourierFamily n k) →
      Fin (FABL.exactDegreeSamplesPerCoefficient n k) → FABL.SignCube n)
  (hgood :
    ∀ (S : ↥(FABL.lowDegreeFourierFamily n k)),
      sampleInputs ∉
        FABL.finiteFamilyCoefficientBadSetWithParameters target
          (FABL.lowDegreeFourierFamily n k)
          (FABL.degreeFourierCoefficientAccuracy k)
          (FABL.finiteFamilyCoefficientConfidence
            (FABL.lowDegreeFourierFamily n k) ⋯)
          S) :
  (FABL.exactDegreeFourierEstimatorOutput target k
        sampleInputs).evaluate =
    target

theorem FABL.exactDegreeFourierEstimatorOutput_evaluate_eq
  {n : ℕ}
  (target : FABL.BooleanFunction n)
  (k : ℕ) (hk : 1 ≤ k)
  (hdegree :
    FABL.fourierDegree target.toReal ≤ k)
  (sampleInputs :
    ↥(FABL.lowDegreeFourierFamily n k) →
      Fin
          (FABL.exactDegreeSamplesPerCoefficient
            n k) →
        FABL.SignCube n)
  (hgood :
    ∀
      (S :
        ↥(FABL.lowDegreeFourierFamily n
            k)),
      sampleInputs ∉
        FABL.finiteFamilyCoefficientBadSetWithParameters
          target
          (FABL.lowDegreeFourierFamily n
            k)
          (FABL.degreeFourierCoefficientAccuracy
            k)
          (FABL.finiteFamilyCoefficientConfidence
            (FABL.lowDegreeFourierFamily n
              k)
            ⋯)
          S) :
  (FABL.exactDegreeFourierEstimatorOutput
        target k sampleInputs).evaluate =
    target

Exact recovery of the real expansion recovers the Boolean target pointwise.