OAI/Analysis/Crouzeix/Endpoint.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Endpoint.

  1. abbrev OAI.CrouzeixHilbert.Endpoint.Herm line 21
  2. instance OAI.CrouzeixHilbert.Endpoint.(instance at line 23) line 23
  3. def OAI.CrouzeixHilbert.Endpoint.unit line 28
  4. theorem OAI.CrouzeixHilbert.Endpoint.unit_val line 31
  5. def OAI.CrouzeixHilbert.Endpoint.strictCone line 33
  6. theorem OAI.CrouzeixHilbert.Endpoint.unit_mem_strictCone line 37
  7. theorem OAI.CrouzeixHilbert.Endpoint.strictCone_nonneg line 40
  8. theorem OAI.CrouzeixHilbert.Endpoint.strictCone_add_nonneg line 46
  9. theorem OAI.CrouzeixHilbert.Endpoint.strictCone_smul line 51
  10. theorem OAI.CrouzeixHilbert.Endpoint.convex_strictCone line 58
  11. theorem OAI.CrouzeixHilbert.Endpoint.isOpen_strictCone line 73
  12. theorem OAI.CrouzeixHilbert.Endpoint.orderUnit_bounds line 92
  13. theorem OAI.CrouzeixHilbert.Endpoint.positive_mono line 101
  14. theorem OAI.CrouzeixHilbert.Endpoint.positive_eq_zero line 108
  15. def OAI.CrouzeixHilbert.Endpoint.congruence line 116
  16. theorem OAI.CrouzeixHilbert.Endpoint.congruence_val line 128
  17. lemma OAI.CrouzeixHilbert.Endpoint.slope_nonpos line 133
  18. lemma OAI.CrouzeixHilbert.Endpoint.slope_zero line 143
  19. abbrev OAI.CrouzeixHilbert.Endpoint.SlackSpace line 156
  20. def OAI.CrouzeixHilbert.Endpoint.slacks line 158
  21. def OAI.CrouzeixHilbert.Endpoint.lowerOpen line 161
  22. theorem OAI.CrouzeixHilbert.Endpoint.convex_lowerOpen line 164
  23. theorem OAI.CrouzeixHilbert.Endpoint.isOpen_lowerOpen line 167
  24. theorem OAI.CrouzeixHilbert.Endpoint.convex_slacks line 171
  25. def OAI.CrouzeixHilbert.Endpoint.scalarPart line 190
  26. def OAI.CrouzeixHilbert.Endpoint.firstPart line 192
  27. def OAI.CrouzeixHilbert.Endpoint.secondPart line 196
  28. def OAI.CrouzeixHilbert.Endpoint.thirdPart line 201
  29. theorem OAI.CrouzeixHilbert.Endpoint.functional_decomposition line 207
  30. theorem OAI.CrouzeixHilbert.Endpoint.lowerOpen_disjoint_slacks line 216
  31. theorem OAI.CrouzeixHilbert.Endpoint.separating_parts_nonneg line 231
  32. theorem OAI.CrouzeixHilbert.Endpoint.separating_value_lower line 282
  33. theorem OAI.CrouzeixHilbert.Endpoint.separating_affine_balance line 300
  34. theorem OAI.CrouzeixHilbert.Endpoint.exists_unit_slacks line 328
  35. theorem OAI.CrouzeixHilbert.Endpoint.separating_scalar_pos line 348
  36. structure OAI.CrouzeixHilbert.Endpoint.DualCertificate line 384
  37. theorem OAI.CrouzeixHilbert.Endpoint.exists_dualCertificate line 398
  38. def OAI.CrouzeixHilbert.Endpoint.hermHS line 470
  39. theorem OAI.CrouzeixHilbert.Endpoint.mem_hermHS line 473
  40. def OAI.CrouzeixHilbert.Endpoint.hermHSCoordinate line 484
  41. theorem OAI.CrouzeixHilbert.Endpoint.exists_trace_representative line 489
  42. theorem OAI.CrouzeixHilbert.Endpoint.trace_representative_posSemidef line 507
  43. theorem OAI.CrouzeixHilbert.Endpoint.exists_positive_trace_representative line 525