OAI/Analysis/NumericalRange/AnalyticCharts.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompleteCrouzeix.real_clm_complex_apply line 34
  2. def OAI.CompleteCrouzeix.barrierComplexification line 41
  3. lemma OAI.CompleteCrouzeix.barrierComplexification_analytic line 45
  4. lemma OAI.CompleteCrouzeix.barrierComplexification_real line 55
  5. lemma OAI.CompleteCrouzeix.barrierComplexification_conj line 68
  6. def OAI.CompleteCrouzeix.barrierChartComplexification line 75
  7. lemma OAI.CompleteCrouzeix.barrierChartComplexification_analytic line 81
  8. lemma OAI.CompleteCrouzeix.barrierChartComplexification_real line 92
  9. lemma OAI.CompleteCrouzeix.barrierChartComplexification_conj line 103
  10. lemma OAI.CompleteCrouzeix.complex_prod_clm_apply line 117
  11. lemma OAI.CompleteCrouzeix.analytic_real_complexification_deriv line 123
  12. lemma OAI.CompleteCrouzeix.analytic_inverse_at line 178
  13. def OAI.CompleteCrouzeix.normalScaleEquiv line 188
  14. lemma OAI.CompleteCrouzeix.analytic_implicit_real_graph line 198
  15. lemma OAI.CompleteCrouzeix.local_normal_side line 285
  16. lemma OAI.CompleteCrouzeix.local_normal_le_side line 318
  17. lemma OAI.CompleteCrouzeix.analytic_chart_rescale line 352