OAI/Analysis/NumericalRange/DensityTransport.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompleteCrouzeix.toHSCLM line 188
  2. def OAI.CompleteCrouzeix.fromHSCLM line 194
  3. def OAI.CompleteCrouzeix.densityField line 200
  4. lemma OAI.CompleteCrouzeix.densityField_ae line 206
  5. lemma OAI.CompleteCrouzeix.densityField_hermitian line 211
  6. lemma OAI.CompleteCrouzeix.densityField_inner_continuous line 218
  7. def OAI.CompleteCrouzeix.tensorTesting line 234
  8. lemma OAI.CompleteCrouzeix.densityField_testing line 239
  9. def OAI.CompleteCrouzeix.hsTraceLp line 263
  10. lemma OAI.CompleteCrouzeix.hsTraceLp_ae line 267
  11. lemma OAI.CompleteCrouzeix.hsTraceLp_star line 272
  12. lemma OAI.CompleteCrouzeix.matrixInner_ext_fourier line 282
  13. def OAI.CompleteCrouzeix.matrixFourierTrace line 294
  14. lemma OAI.CompleteCrouzeix.hsTraceLp_matrixFourierTrace line 301
  15. lemma OAI.CompleteCrouzeix.densityInner_ext_fourier line 315
  16. lemma OAI.CompleteCrouzeix.l2Star_inner line 321
  17. theorem OAI.CompleteCrouzeix.density_adjoint_identification line 332