OAI/Analysis/FreeWords/DirichletMoments.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKFreeWords.dirichletRow line 43
  2. def OAI.KKFreeWords.regularizedScalar line 46
  3. theorem OAI.KKFreeWords.positiveMap_real_smul line 76
  4. theorem OAI.KKFreeWords.haar_upow_orthonormal line 79
  5. theorem OAI.KKFreeWords.haar_dirichlet_coefficient line 90
  6. theorem OAI.KKFreeWords.haar_dirichlet_energy line 109
  7. theorem OAI.KKFreeWords.dirichletRow_square line 122
  8. theorem OAI.KKFreeWords.dirichletRow_square_centered line 131
  9. theorem OAI.KKFreeWords.dirichletRow_energy_lower line 139