OAI/Probability/GaussianRegression/Main.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Quadratic and subquadratic memory lower bounds for Gaussian regression.

  1. theorem OAI.NoiselessRegression.fixed_quadratic_memory line 20
  2. lemma OAI.NoiselessRegression.prod_null_set_lower_bound line 43
  3. lemma OAI.NoiselessRegression.Learner.uniformSuccess_of_pointwise line 64
  4. theorem OAI.NoiselessRegression.subquadratic_memory line 74
  5. theorem OAI.NoiselessRegression.main line 91

    Distinct definitions of this name: ComparatorChallenges/NoiselessRegression.lean:118 (same statement text; different proof or body). Qualify references as OAI.NoiselessRegression.main@path.