OAI/Analysis/MatrixSigning/Optimization/ValueOuterRadius.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentKS.RationalSDP.euclidean_norm_le_card line 16
  2. lemma OAI.CurrentKS.RationalSDP.norm_hermitian_entry line 28
  3. lemma OAI.CurrentKS.RationalSDP.abs_encode_le line 32
  4. lemma OAI.CurrentKS.RationalSDP.norm_packValue line 38
  5. lemma OAI.CurrentKS.RationalSDP.norm_psd_order_bound line 53
  6. def OAI.CurrentKS.RationalSDP.valueOuterRadius line 67
  7. def OAI.CurrentKS.RationalSDP.valueInnerRadius line 69
  8. lemma OAI.CurrentKS.RationalSDP.valueOuterRadius_nonneg line 71
  9. lemma OAI.CurrentKS.RationalSDP.valueInnerRadius_pos line 74
  10. lemma OAI.CurrentKS.RationalSDP.valueInnerRadius_le line 75
  11. lemma OAI.CurrentKS.RationalSDP.oracleBox_norm_packValue line 80
  12. lemma OAI.CurrentKS.RationalSDP.unpackValue_sub line 96
  13. lemma OAI.CurrentKS.RationalSDP.timeCoordinate_norm line 106
  14. lemma OAI.CurrentKS.RationalSDP.unpackValue_matrix_norm line 111
  15. lemma OAI.CurrentKS.RationalSDP.value_center_coordinate_ball line 119