OAI/Probability/EntangledGames/ExposureChain.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThresholdParallelRepetition.MixedExposure.list_suffix_prefix_disjoint line 13
  2. lemma OAI.ThresholdParallelRepetition.MixedExposure.list_fresh_not_suffix line 20
  3. lemma OAI.ThresholdParallelRepetition.MixedExposure.list_fresh_not_prefix line 26
  4. def OAI.ThresholdParallelRepetition.MixedExposure.chainLeft line 37
  5. def OAI.ThresholdParallelRepetition.MixedExposure.chainRight line 39
  6. lemma OAI.ThresholdParallelRepetition.MixedExposure.chainLeft_step line 43
  7. lemma OAI.ThresholdParallelRepetition.MixedExposure.chainRight_step line 50
  8. lemma OAI.ThresholdParallelRepetition.MixedExposure.chainLeft_next_local line 58
  9. lemma OAI.ThresholdParallelRepetition.MixedExposure.chainRight_prev_local line 64
  10. lemma OAI.ThresholdParallelRepetition.MixedExposure.chain_mass line 71
  11. lemma OAI.ThresholdParallelRepetition.MixedExposure.tested_weight_sum_le line 100
  12. lemma OAI.ThresholdParallelRepetition.MixedExposure.averaged_potential_left_bounds line 109
  13. lemma OAI.ThresholdParallelRepetition.MixedExposure.averaged_potential_right_bounds line 129
  14. lemma OAI.ThresholdParallelRepetition.MixedExposure.fin_telescope_bound line 149
  15. lemma OAI.ThresholdParallelRepetition.MixedExposure.fin_telescope_bound_rev line 157
  16. abbrev OAI.ThresholdParallelRepetition.MixedExposure.ExposureIndex line 178
  17. def OAI.ThresholdParallelRepetition.MixedExposure.chainLeftFamily line 180
  18. def OAI.ThresholdParallelRepetition.MixedExposure.chainRightFamily line 185
  19. lemma OAI.ThresholdParallelRepetition.MixedExposure.chain_error_bounds line 190
  20. def OAI.ThresholdParallelRepetition.MixedExposure.massAt line 293
  21. lemma OAI.ThresholdParallelRepetition.MixedExposure.right_update_eq line 300
  22. lemma OAI.ThresholdParallelRepetition.MixedExposure.left_update_eq line 306
  23. lemma OAI.ThresholdParallelRepetition.MixedExposure.massAt_right line 313
  24. lemma OAI.ThresholdParallelRepetition.MixedExposure.massAt_left line 340