OAI/NumberTheory/Ostmann/Tree/MeanInner.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.FiniteField.meanInner line 11
  2. theorem OAI.Ostmann.FiniteField.meanInner_self line 13
  3. theorem OAI.Ostmann.FiniteField.mean_add line 18
  4. theorem OAI.Ostmann.FiniteField.mean_const_mul line 21
  5. theorem OAI.Ostmann.FiniteField.mean_const line 26
  6. theorem OAI.Ostmann.FiniteField.mean_conj line 31
  7. theorem OAI.Ostmann.FiniteField.l2Sq_const_mul line 34
  8. theorem OAI.Ostmann.FiniteField.l2Sq_const line 39
  9. theorem OAI.Ostmann.FiniteField.l2Sq_conj line 44
  10. theorem OAI.Ostmann.FiniteField.mean_sub_mean line 47
  11. theorem OAI.Ostmann.FiniteField.meanInner_norm_sq_le line 54
  12. theorem OAI.Ostmann.FiniteField.l2Sq_add_const line 64