OAI/Analysis/Cotype/PatternNormalization.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Cotype.average_mul_left line 12
  2. theorem OAI.Cotype.average_mul_right line 15
  3. theorem OAI.Cotype.average_add_real line 18
  4. theorem OAI.Cotype.average_sub_real line 22
  5. theorem OAI.Cotype.average_div_real line 26
  6. theorem OAI.Cotype.average_const_real line 30
  7. theorem OAI.Cotype.abs_average_le_const line 33
  8. theorem OAI.Cotype.average_coordinate line 41
  9. theorem OAI.Cotype.xorCube_negate_right line 57
  10. theorem OAI.Cotype.xorCube_negate_left line 62
  11. def OAI.Cotype.vectorTwist line 66
  12. def OAI.Cotype.matrixTwist line 69
  13. theorem OAI.Cotype.oddPart_vectorTwist line 72
  14. theorem OAI.Cotype.oddPart_matrixTwist line 76
  15. theorem OAI.Cotype.fourier_average_family line 82
  16. theorem OAI.Cotype.vectorTwist_first_coefficient line 87