OAI/Analysis/NumericalRange/CauchyProjection.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompleteCrouzeix.circleTest line 26
  2. lemma OAI.CompleteCrouzeix.circleTest_apply line 29
  3. lemma OAI.CompleteCrouzeix.circleTest_add line 39
  4. lemma OAI.CompleteCrouzeix.circleTest_fourier line 44
  5. lemma OAI.CompleteCrouzeix.circleCLM_ext line 51
  6. lemma OAI.CompleteCrouzeix.circleTest_const_positive line 59
  7. def OAI.CompleteCrouzeix.AnalyticBidiskKernel.rowB line 78
  8. def OAI.CompleteCrouzeix.AnalyticBidiskKernel.rowKernel line 81
  9. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.rowKernel_eq line 85
  10. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.testB_positive line 89
  11. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.testConjB_positive line 103
  12. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.testKernel_positive line 117
  13. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.scalarM_positive_ae line 123
  14. def OAI.CompleteCrouzeix.analyticCircleTrace line 143
  15. lemma OAI.CompleteCrouzeix.analyticTrace_negative_coefficient line 149
  16. lemma OAI.CompleteCrouzeix.analyticTrace_negative line 160
  17. lemma OAI.CompleteCrouzeix.scalarCauchy_fix_of_parts line 180
  18. theorem OAI.CompleteCrouzeix.analytic_circle_gluing line 198
  19. lemma OAI.CompleteCrouzeix.circleTest_toLp line 231
  20. lemma OAI.CompleteCrouzeix.scalarCauchy_fix_of_analytic_correction line 240
  21. lemma OAI.CompleteCrouzeix.canonicalCircleCauchy_analytic line 284
  22. lemma OAI.CompleteCrouzeix.scalarCauchy_fix_physical_trace line 298
  23. theorem OAI.CompleteCrouzeix.reciprocalCorrection_continuousOn line 342