OAI/Analysis/NumericalRange/FourierExtension.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CompleteCrouzeix.physicalCauchy_extension line 35
  2. theorem OAI.CompleteCrouzeix.physicalCauchy_fourier_extension line 77
  3. lemma OAI.CompleteCrouzeix.scalarCauchy_fourier_ae line 125
  4. def OAI.CompleteCrouzeix.physicalAnalyticTrace line 157
  5. theorem OAI.CompleteCrouzeix.actualExteriorCauchy_fourier_trace line 164
  6. lemma OAI.CompleteCrouzeix.exteriorMap_circle_analytic line 212
  7. theorem OAI.CompleteCrouzeix.actualExteriorCauchy_module line 221
  8. abbrev OAI.CompleteCrouzeix.VectorL2 line 270
  9. def OAI.CompleteCrouzeix.l2Coordinate line 272
  10. def OAI.CompleteCrouzeix.singleCLM line 275
  11. lemma OAI.CompleteCrouzeix.singleCLM_apply line 278
  12. def OAI.CompleteCrouzeix.l2Embedding line 283
  13. lemma OAI.CompleteCrouzeix.l2Coordinate_ae line 286
  14. lemma OAI.CompleteCrouzeix.l2Embedding_ae line 292
  15. lemma OAI.CompleteCrouzeix.l2Coordinate_injective line 296
  16. lemma OAI.CompleteCrouzeix.coordinate_embedding line 307
  17. lemma OAI.CompleteCrouzeix.embedding_inner line 323
  18. lemma OAI.CompleteCrouzeix.coordinate_inner line 331
  19. def OAI.CompleteCrouzeix.entrywiseL2 line 336
  20. lemma OAI.CompleteCrouzeix.coordinate_entrywise line 340
  21. lemma OAI.CompleteCrouzeix.entrywise_inner line 345
  22. def OAI.CompleteCrouzeix.vectorResolution line 354