OAI/Probability/SKBarriers/Replicas/TripleRetained.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SK.Analytic.TripleRetainedState line 15
  2. def OAI.SK.Analytic.retainedSingleton line 17
  3. def OAI.SK.Analytic.retainedNoise line 19
  4. def OAI.SK.Analytic.retainedPair line 21
  5. def OAI.SK.Analytic.tripleRetainedEmbedding line 23
  6. theorem OAI.SK.Analytic.tripleRetainedEmbedding_apply line 26
  7. def OAI.SK.Analytic.tripleRetainedCommon line 30
  8. def OAI.SK.Analytic.tripleRetainedMiddle line 33
  9. theorem OAI.SK.Analytic.tripleRetainedCommon_image line 36
  10. theorem OAI.SK.Analytic.tripleRetainedMiddle_image line 40
  11. theorem OAI.SK.Analytic.retained_sum_coordinates line 47
  12. theorem OAI.SK.Analytic.tripleRetained_pressure line 62