OAI/Analysis/NumericalRange/DiskCalculus.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompleteCrouzeix.primaryEval_tendsto_apply line 19
  2. def OAI.CompleteCrouzeix.matrixAnalyticEval line 58

    Also declared: ComparatorChallenges/StructuralCrouzeix.lean:107 (same declaration text).

  3. lemma OAI.CompleteCrouzeix.matrixAnalyticEval_polynomial line 61
  4. lemma OAI.CompleteCrouzeix.matrixAnalyticEval_tendsto line 67
  5. lemma OAI.CompleteCrouzeix.locallyUniform_iteratedDeriv line 86
  6. lemma OAI.CompleteCrouzeix.matrixAnalyticEval_tendsto_locallyUniform line 100
  7. def OAI.CompleteCrouzeix.seriesPolynomial line 117
  8. lemma OAI.CompleteCrouzeix.seriesPolynomial_eval line 120
  9. lemma OAI.CompleteCrouzeix.analytic_closed_disk_polynomial_approximation line 126
  10. theorem OAI.CompleteCrouzeix.summable_norm_powers line 156
  11. abbrev OAI.CompleteCrouzeix.circleMeasure line 181
  12. def OAI.CompleteCrouzeix.diskResolventSeries line 184
  13. lemma OAI.CompleteCrouzeix.fourier_norm_value line 187
  14. lemma OAI.CompleteCrouzeix.summable_diskResolvent line 190
  15. lemma OAI.CompleteCrouzeix.continuous_diskResolvent line 195
  16. lemma OAI.CompleteCrouzeix.fourier_neg_nat_pow line 204
  17. lemma OAI.CompleteCrouzeix.diskResolvent_inverse line 214
  18. def OAI.CompleteCrouzeix.diskDensity line 225
  19. lemma OAI.CompleteCrouzeix.continuous_diskDensity line 228
  20. lemma OAI.CompleteCrouzeix.diskDensity_nonneg line 233
  21. lemma OAI.CompleteCrouzeix.integral_fourier line 266
  22. lemma OAI.CompleteCrouzeix.integral_fourier_smul line 272
  23. lemma OAI.CompleteCrouzeix.integral_matrix_fourier_series line 277
  24. lemma OAI.CompleteCrouzeix.diskResolvent_moment line 299
  25. lemma OAI.CompleteCrouzeix.diskResolvent_star_moment line 307
  26. theorem OAI.CompleteCrouzeix.diskDensity_moment line 324
  27. lemma OAI.CompleteCrouzeix.contraction_block_iff line 349
  28. lemma OAI.CompleteCrouzeix.positive_density_block line 360
  29. def OAI.CompleteCrouzeix.entryCLM line 375
  30. lemma OAI.CompleteCrouzeix.matrix_integral_entry line 381
  31. def OAI.CompleteCrouzeix.kronCLM line 386
  32. lemma OAI.CompleteCrouzeix.integral_kron_const line 392
  33. lemma OAI.CompleteCrouzeix.integral_fromBlocks line 397
  34. def OAI.CompleteCrouzeix.conjTransposeRCLM line 419
  35. lemma OAI.CompleteCrouzeix.integral_conjTranspose line 425
  36. theorem OAI.CompleteCrouzeix.norm_integral_density_kron line 430
  37. lemma OAI.CompleteCrouzeix.continuous_kron line 447
  38. def OAI.CompleteCrouzeix.circlePolynomial line 457
  39. lemma OAI.CompleteCrouzeix.continuous_circlePolynomial line 460
  40. lemma OAI.CompleteCrouzeix.integrable_diskDensity_monomial_kron line 465
  41. lemma OAI.CompleteCrouzeix.diskDensity_monomial_kron line 475
  42. lemma OAI.CompleteCrouzeix.kron_circlePolynomial line 485
  43. lemma OAI.CompleteCrouzeix.diskDensity_polynomial_moment line 497
  44. theorem OAI.CompleteCrouzeix.stable_complete_disk_bound line 506