OAI/Analysis/NumericalRange/CircleIntegrals.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompleteCrouzeix.unitAddCircle_integral_eq_circleAverage line 19
  2. lemma OAI.CompleteCrouzeix.fourier_natCast_toCircle line 37
  3. lemma OAI.CompleteCrouzeix.fourier_neg_natCast_toCircle line 44
  4. lemma OAI.CompleteCrouzeix.integral_analytic_circle line 50
  5. lemma OAI.CompleteCrouzeix.integral_analytic_mul_pow line 61
  6. lemma OAI.CompleteCrouzeix.integral_reciprocal_analytic_mul_inv_pow line 68
  7. lemma OAI.CompleteCrouzeix.integral_reciprocal_analytic line 79
  8. lemma OAI.CompleteCrouzeix.compact_parametric_hasDerivAt line 94
  9. lemma OAI.CompleteCrouzeix.analyticOnNhd_compact_integral line 128
  10. def OAI.CompleteCrouzeix.physicalCauchy line 140
  11. lemma OAI.CompleteCrouzeix.physicalCauchy_analytic line 147
  12. lemma OAI.CompleteCrouzeix.unitAddCircle_integral_affine line 178
  13. lemma OAI.CompleteCrouzeix.analyticOnNhd_integral_of_continuous line 185
  14. lemma OAI.CompleteCrouzeix.circle_cauchy_pow line 269
  15. lemma OAI.CompleteCrouzeix.circle_cauchy_inv_pow line 279
  16. def OAI.CompleteCrouzeix.cauchyCorrectionIntegral line 313
  17. lemma OAI.CompleteCrouzeix.cauchyCorrectionIntegral_analytic line 317
  18. lemma OAI.CompleteCrouzeix.physicalCauchy_decompose line 338
  19. lemma OAI.CompleteCrouzeix.physicalCauchy_pow line 369
  20. lemma OAI.CompleteCrouzeix.physicalCauchy_inv_pow line 380