OAI/Probability/EntangledGames/TestMoments.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThresholdParallelRepetition.FiniteProbability.Tests.event line 14
  2. def OAI.ThresholdParallelRepetition.FiniteProbability.Tests.mass line 15
  3. def OAI.ThresholdParallelRepetition.FiniteProbability.Tests.rate line 16
  4. def OAI.ThresholdParallelRepetition.FiniteProbability.Tests.moment line 17
  5. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.event_nonneg line 20
  6. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.event_le_one line 22
  7. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.mass_nonneg line 24
  8. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.mass_le_one line 26
  9. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.rate_nonneg line 28
  10. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.rate_le_one line 31
  11. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.event_empty line 34
  12. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.mass_empty line 36
  13. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.event_insert line 41
  14. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.avg_event_insert line 46
  15. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.moment_zero line 51
  16. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.moment_step line 52
  17. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.moment_upper line 64
  18. lemma OAI.ThresholdParallelRepetition.FiniteProbability.Tests.threshold_moment_lower line 88