OAI/Analysis/DirectCrouzeix/CircleFourier.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectCrouzeix.continuous_integrable_compact line 18
  2. theorem OAI.DirectCrouzeix.continuous_integral_compact line 24
  3. theorem OAI.DirectCrouzeix.markov_kernel_contraction line 33
  4. abbrev OAI.DirectCrouzeix.BoundaryCircle line 65
  5. abbrev OAI.DirectCrouzeix.circleMeasure line 67
  6. theorem OAI.DirectCrouzeix.scalar_circle_parseval line 69
  7. theorem OAI.DirectCrouzeix.fourierCoeff_euclidean_apply line 84
  8. theorem OAI.DirectCrouzeix.euclidean_circle_parseval line 91
  9. def OAI.DirectCrouzeix.hsCLM line 106
  10. theorem OAI.DirectCrouzeix.hsCLM_apply line 113
  11. theorem OAI.DirectCrouzeix.continuous_hsSq line 116
  12. theorem OAI.DirectCrouzeix.fourierCoeff_clm line 122
  13. theorem OAI.DirectCrouzeix.matrix_circle_parseval line 130
  14. def OAI.DirectCrouzeix.compressionCLM line 139
  15. theorem OAI.DirectCrouzeix.compressionCLM_apply line 146
  16. theorem OAI.DirectCrouzeix.fourierCoeff_compression line 149
  17. def OAI.DirectCrouzeix.conjugateTransposeCLM line 154
  18. theorem OAI.DirectCrouzeix.conjugateTransposeCLM_apply line 161
  19. theorem OAI.DirectCrouzeix.fourierCoeff_star_matrix line 164