OAI/Analysis/NumericalRange/OrderedMultiplication.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompleteCrouzeix.FourierResolution.star_negative line 46
  2. lemma OAI.CompleteCrouzeix.FourierResolution.nonnegative_decompose line 50
  3. lemma OAI.CompleteCrouzeix.FourierResolution.hermitian_fourier_norm line 56
  4. lemma OAI.CompleteCrouzeix.FourierResolution.adjoint_module_apply line 86
  5. lemma OAI.CompleteCrouzeix.FourierResolution.hermitian_diagonal_bound line 97
  6. lemma OAI.CompleteCrouzeix.FourierResolution.opposite_adjoint_orthogonal line 120
  7. theorem OAI.CompleteCrouzeix.FourierResolution.density_comparison_core line 141
  8. lemma OAI.CompleteCrouzeix.scalarFourier_star_zero line 185
  9. lemma OAI.CompleteCrouzeix.scalarFourier_star_positive line 197
  10. abbrev OAI.CompleteCrouzeix.MatrixCircleL2 line 213
  11. def OAI.CompleteCrouzeix.matrixFourier line 215
  12. lemma OAI.CompleteCrouzeix.coordinate_matrixStar line 218
  13. lemma OAI.CompleteCrouzeix.coordinate_matrixFourier line 228
  14. lemma OAI.CompleteCrouzeix.matrixFourier_star_zero line 232
  15. lemma OAI.CompleteCrouzeix.matrixFourier_star_positive line 239
  16. def OAI.CompleteCrouzeix.AnalyticBidiskKernel.matrixM line 254
  17. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.matrixM_norm_le line 257
  18. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.coordinate_matrixM line 262
  19. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.matrixM_swap line 279
  20. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.matrixM_star line 288
  21. lemma OAI.CompleteCrouzeix.l2_sum_embedding_coordinate line 304
  22. lemma OAI.CompleteCrouzeix.entrywise_embedding line 311
  23. lemma OAI.CompleteCrouzeix.entrywise_module_of_blocks line 318
  24. theorem OAI.CompleteCrouzeix.actualExteriorCauchy_vector_module line 334
  25. lemma OAI.CompleteCrouzeix.matrixCauchy_eq_entrywise line 380
  26. theorem OAI.CompleteCrouzeix.actualExteriorCauchy_field_module line 394
  27. theorem OAI.CompleteCrouzeix.actualExteriorCauchy_ordered_modules line 432