OAI/Analysis/Cotype/CubeNoise.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Cotype.cubeCons line 11
  2. theorem OAI.Cotype.average_cons line 17
  3. def OAI.Cotype.cubeNoise line 23
  4. theorem OAI.Cotype.cubeNoise_cons_false line 33
  5. theorem OAI.Cotype.cubeNoise_cons_true line 38
  6. theorem OAI.Cotype.cubeNoise_add line 43
  7. theorem OAI.Cotype.cubeNoise_smul line 52
  8. theorem OAI.Cotype.cubeNoise_const line 61
  9. theorem OAI.Cotype.cubeNoise_norm_le line 69
  10. theorem OAI.Cotype.rademacherSum_cons line 87
  11. theorem OAI.Cotype.cubeNoise_rademacherSum line 91