OAI/Analysis/NumericalRange/DualSeparation.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompleteCrouzeix.StrictPositive line 33
  2. lemma OAI.CompleteCrouzeix.hermitian_smul_one_le_iff line 36
  3. lemma OAI.CompleteCrouzeix.hermitian_lower_norm line 41
  4. lemma OAI.CompleteCrouzeix.StrictPositive.nonneg line 51
  5. lemma OAI.CompleteCrouzeix.strictPositive_one line 57
  6. lemma OAI.CompleteCrouzeix.StrictPositive.add_nonneg line 62
  7. lemma OAI.CompleteCrouzeix.StrictPositive.smul line 68
  8. lemma OAI.CompleteCrouzeix.strictPositive_isOpen line 76
  9. lemma OAI.CompleteCrouzeix.strictPositive_convex line 91
  10. def OAI.CompleteCrouzeix.metricStein line 109
  11. theorem OAI.CompleteCrouzeix.exists_strict_metric line 125
  12. abbrev OAI.CompleteCrouzeix.MetricDualSpace line 152
  13. def OAI.CompleteCrouzeix.metricLinear line 155
  14. def OAI.CompleteCrouzeix.metricOffset line 166
  15. def OAI.CompleteCrouzeix.metricAffine line 167
  16. def OAI.CompleteCrouzeix.metricOpen line 170
  17. lemma OAI.CompleteCrouzeix.metricOpen_isOpen line 173
  18. lemma OAI.CompleteCrouzeix.metricOpen_convex line 179
  19. lemma OAI.CompleteCrouzeix.metricAffine_range_convex line 183
  20. lemma OAI.CompleteCrouzeix.ray_slope_nonpos line 198
  21. lemma OAI.CompleteCrouzeix.affine_functional_constant line 207
  22. lemma OAI.CompleteCrouzeix.metricAffine_feasible line 226
  23. lemma OAI.CompleteCrouzeix.metric_sets_disjoint line 247
  24. theorem OAI.CompleteCrouzeix.metric_separator line 256
  25. def OAI.CompleteCrouzeix.metricAxis0 line 272
  26. def OAI.CompleteCrouzeix.metricAxis1 line 277
  27. def OAI.CompleteCrouzeix.metricAxis2 line 282
  28. def OAI.CompleteCrouzeix.metricAxis3 line 287
  29. lemma OAI.CompleteCrouzeix.metric_functional_decompose line 292
  30. lemma OAI.CompleteCrouzeix.metric_separator_nonpos line 302
  31. lemma OAI.CompleteCrouzeix.metric_separator_scalar_pos line 318
  32. lemma OAI.CompleteCrouzeix.metric_separator_limit line 345
  33. theorem OAI.CompleteCrouzeix.metric_normalized_separator line 361
  34. lemma OAI.CompleteCrouzeix.hermTrace_zero_right line 409
  35. lemma OAI.CompleteCrouzeix.hermTrace_zero_left line 414
  36. lemma OAI.CompleteCrouzeix.hermTrace_add_right line 416
  37. lemma OAI.CompleteCrouzeix.hermTrace_sub_right line 421
  38. lemma OAI.CompleteCrouzeix.hermTrace_smul_right line 426
  39. lemma OAI.CompleteCrouzeix.hermTrace_add_left line 432
  40. lemma OAI.CompleteCrouzeix.hermTrace_sub_left line 435
  41. lemma OAI.CompleteCrouzeix.hermTrace_nondegenerate line 439
  42. def OAI.CompleteCrouzeix.metricPush line 450
  43. lemma OAI.CompleteCrouzeix.hermTrace_stein line 453
  44. theorem OAI.CompleteCrouzeix.metric_dual_certificate line 466