OAI/Analysis/HyperbolicCones/Model.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

The Choi–Lam form, determinant polynomial, root-defined cone, and quadratic deformation.

  1. abbrev OAI.Paper256.Mat line 15

    Also declared: ComparatorChallenges/HyperbolicCones.lean:13 (same declaration text).

  2. abbrev OAI.Paper256.Sym line 17

    Also declared: ComparatorChallenges/HyperbolicCones.lean:15 (same declaration text).

  3. instance OAI.Paper256.instFiniteDimensionalSym line 19

    Also declared: ComparatorChallenges/HyperbolicCones.lean:17 (same declaration text).

  4. abbrev OAI.Paper256.Ambient line 22

    Also declared: ComparatorChallenges/HyperbolicCones.lean:20 (same declaration text).

  5. abbrev OAI.Paper256.SymIndex line 24

    Also declared: ComparatorChallenges/HyperbolicCones.lean:22 (same declaration text).

  6. abbrev OAI.Paper256.Coord line 26

    Also declared: ComparatorChallenges/HyperbolicCones.lean:24 (same declaration text).

  7. def OAI.Paper256.qMatrix line 28

    Also declared: ComparatorChallenges/HyperbolicCones.lean:26 (same declaration text).

  8. def OAI.Paper256.phi line 31

    Also declared: ComparatorChallenges/HyperbolicCones.lean:29 (same declaration text).

  9. def OAI.Paper256.matrixValue line 40

    Also declared: ComparatorChallenges/HyperbolicCones.lean:38 (same declaration text).

  10. def OAI.Paper256.symmetricCoordinates line 44

    Also declared: ComparatorChallenges/HyperbolicCones.lean:42 (same declaration text).

  11. def OAI.Paper256.polynomial line 48

    Also declared: ComparatorChallenges/HyperbolicCones.lean:46 (same declaration text).

  12. def OAI.Paper256.coordinates line 54

    Also declared: ComparatorChallenges/HyperbolicCones.lean:52 (same declaration text).

  13. def OAI.Paper256.basePoint line 59

    Also declared: ComparatorChallenges/HyperbolicCones.lean:57 (same declaration text).

  14. def OAI.Paper256.linePolynomial line 61

    Also declared: ComparatorChallenges/HyperbolicCones.lean:59 (same declaration text).

  15. def OAI.Paper256.cone line 66

    Also declared: ComparatorChallenges/HyperbolicCones.lean:64 (same declaration text).

  16. def OAI.Paper256.choiLam line 69
  17. def OAI.Paper256.zMatrix line 75
  18. def OAI.Paper256.intervalPolynomial line 78
  19. def OAI.Paper256.timeScale line 81
  20. def OAI.Paper256.deformedPolynomial line 83
  21. def OAI.Paper256.rigidlyConvexSet line 86
  22. abbrev OAI.Paper256.Vec line 92
  23. def OAI.Paper256.outer line 94
  24. def OAI.Paper256.outerSym line 96
  25. def OAI.Paper256.operatorNorm line 102
  26. def OAI.Paper256.kernelProjection line 105
  27. def OAI.Paper256.inverseSquareRoot line 108
  28. def OAI.Paper256.wedgeCoordinates line 114

    Source documentation

    The vector v₀u′−u₀v′ in the rank-one and operator-norm identities.

    def wedgeCoordinates (v u : Vec 4) : Fin 3 → ℝ :=
…

    Mentions: OAI.Paper256.Vec

  29. def OAI.Paper256.tangentCurve line 117
  30. def OAI.Paper256.tangentSpace line 120
  31. structure OAI.Paper256.NormalizedPencil line 123

    Source documentation

    Positive unital diagonal blocks with an exact Schur-complement equivalence.

    structure NormalizedPencil where
…
  32. def OAI.Paper256.NormalizedPencil.leftProjection line 139
  33. def OAI.Paper256.NormalizedPencil.rightProjection line 142
  34. def OAI.Paper256.deformedPencil line 145
  35. def OAI.Paper256.deformedCoefficients line 148