OAI/Analysis/NumericalRange/DilationDensity.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompleteCrouzeix.dilationField line 20
  2. def OAI.CompleteCrouzeix.dilationLM line 23
  3. lemma OAI.CompleteCrouzeix.dilationLM_coe line 34
  4. lemma OAI.CompleteCrouzeix.dilationLM_inner line 42
  5. def OAI.CompleteCrouzeix.positiveDilation line 64
  6. def OAI.CompleteCrouzeix.baseAmplification line 74
  7. lemma OAI.CompleteCrouzeix.baseAmplification_mul line 82
  8. lemma OAI.CompleteCrouzeix.baseAmplification_star line 88
  9. lemma OAI.CompleteCrouzeix.baseAmplification_one line 97
  10. def OAI.CompleteCrouzeix.densityRootField line 102
  11. lemma OAI.CompleteCrouzeix.densityRootField_sq line 108
  12. lemma OAI.CompleteCrouzeix.densityRootField_mass line 121
  13. def OAI.CompleteCrouzeix.matrixPositiveDilation line 133
  14. theorem OAI.CompleteCrouzeix.positiveDilation_compression line 140
  15. def OAI.CompleteCrouzeix.coefficientMatrixHom line 187
  16. lemma OAI.CompleteCrouzeix.coefficientMatrixHom_norm line 200
  17. def OAI.CompleteCrouzeix.coefficientAmplification line 204
  18. lemma OAI.CompleteCrouzeix.coefficientAmplification_norm line 209
  19. lemma OAI.CompleteCrouzeix.coefficientAmplification_star line 213
  20. def OAI.CompleteCrouzeix.coefficientMultiplierField line 231
  21. lemma OAI.CompleteCrouzeix.coefficientMultiplierField_norm line 235
  22. lemma OAI.CompleteCrouzeix.densityRootField_compression line 242
  23. theorem OAI.CompleteCrouzeix.matrixPositiveDilation_compression line 263
  24. theorem OAI.CompleteCrouzeix.isometric_multiplier_saturation line 282
  25. theorem OAI.CompleteCrouzeix.positiveDilation_saturation line 310
  26. def OAI.CompleteCrouzeix.weightedDensity line 353
  27. lemma OAI.CompleteCrouzeix.weightedDensity_star line 356
  28. lemma OAI.CompleteCrouzeix.weightedDensity_pos line 363
  29. lemma OAI.CompleteCrouzeix.weightedDensity_block_pos line 369
  30. lemma OAI.CompleteCrouzeix.weightedDensity_of_sqrt line 379
  31. lemma OAI.CompleteCrouzeix.weightedDensity_right line 389
  32. lemma OAI.CompleteCrouzeix.weightedDensity_left line 397
  33. lemma OAI.CompleteCrouzeix.weightedDensity_ordered_products line 405
  34. def OAI.CompleteCrouzeix.weightedDensityCLM line 421
  35. lemma OAI.CompleteCrouzeix.integral_weightedDensity line 427
  36. lemma OAI.CompleteCrouzeix.weightedDensity_mean line 432
  37. lemma OAI.CompleteCrouzeix.weightedDensity_mean_zero line 438
  38. lemma OAI.CompleteCrouzeix.trace_weightedDensity_one line 444
  39. lemma OAI.CompleteCrouzeix.continuous_weightedDensity line 459
  40. lemma OAI.CompleteCrouzeix.inner_vectorize line 466
  41. theorem OAI.CompleteCrouzeix.weightedDensity_testing line 480
  42. lemma OAI.CompleteCrouzeix.vectorize_injective line 501
  43. theorem OAI.CompleteCrouzeix.actual_density_ordered line 508
  44. theorem OAI.CompleteCrouzeix.actual_density_means line 557