OAI/Probability/EntangledGames/ExposureData.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ThresholdParallelRepetition.MixedExposure.EventSystem line 16
  2. abbrev OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.J line 45
  3. abbrev OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.f line 46
  4. abbrev OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.h line 47
  5. abbrev OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.A line 48
  6. abbrev OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.B line 49
  7. def OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.U line 51
  8. def OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.V line 52
  9. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.f_pos line 55
  10. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.h_pos line 58
  11. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.U_gram line 60
  12. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.V_gram line 63
  13. def OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.D line 67
  14. def OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.rawA line 69
  15. def OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.rawB line 71
  16. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.rawA_eq line 74
  17. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.rawB_eq line 83
  18. def OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.density line 93
  19. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.density_nonneg line 95
  20. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.density_total line 97
  21. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.density_le line 100
  22. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.D_norm line 103
  23. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.rawA_norm line 111
  24. lemma OAI.ThresholdParallelRepetition.MixedExposure.EventSystem.rawB_norm line 124