OAI/Probability/SKBarriers/Replicas/TriplePerturbation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.Analytic.tripleSymmetricMatrix line 13
  2. def OAI.SK.Analytic.tripleImbalance line 16
  3. def OAI.SK.Analytic.tripleQuadraticCorrection line 17
  4. def OAI.SK.Analytic.triplePerturbedMatrix line 19
  5. def OAI.SK.Analytic.tripleGram line 23
  6. def OAI.SK.Analytic.tripleModifiedIncrement line 26
  7. theorem OAI.SK.Analytic.tripleModifiedIncrement_psd line 28
  8. theorem OAI.SK.Analytic.tripleModifiedIncrement_change line 32
  9. theorem OAI.SK.Analytic.triplePerturbedMatrix_square line 40
  10. theorem OAI.SK.Analytic.triplePerturbedMatrix_endpoint line 48
  11. theorem OAI.SK.Analytic.triplePerturbedMatrix_mismatch line 55
  12. theorem OAI.SK.Analytic.triplePerturbedMatrix_penalty_step line 62
  13. theorem OAI.SK.Analytic.triplePerturbedMatrix_penalty_lower line 72