OAI/Probability/SKGap/Localization/AffineBilinear.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.gaussianCoordinate_mean line 15
  2. lemma OAI.SKGap.goeEntry_integral line 22
  3. lemma OAI.SKGap.signConjugate_diagonal line 30
  4. lemma OAI.SKGap.signConjugate_sub line 40
  5. lemma OAI.SKGap.signConjugate_smul line 45
  6. def OAI.SKGap.affineRight line 49
  7. lemma OAI.SKGap.affineRight_sign line 52
  8. lemma OAI.SKGap.affineRight_lip line 60
  9. lemma OAI.SKGap.affineRight_diag line 77
  10. lemma OAI.SKGap.affineRight_bias line 83
  11. lemma OAI.SKGap.affineRight_concentration line 105