OAI/Probability/EntangledGames/Resolvent.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThresholdParallelRepetition.Resolvent.shift_posDef line 19
  2. lemma OAI.ThresholdParallelRepetition.Resolvent.second_resolvent_identity line 23
  3. def OAI.ThresholdParallelRepetition.Resolvent.resolvent line 38
  4. def OAI.ThresholdParallelRepetition.Resolvent.purificationKernel line 41
  5. lemma OAI.ThresholdParallelRepetition.Resolvent.resolvent_posSemidef line 44
  6. lemma OAI.ThresholdParallelRepetition.Resolvent.resolvent_mul_shift line 48
  7. lemma OAI.ThresholdParallelRepetition.Resolvent.shift_mul_resolvent line 52
  8. lemma OAI.ThresholdParallelRepetition.Resolvent.purificationKernel_eq line 56
  9. lemma OAI.ThresholdParallelRepetition.Resolvent.resolvent_mul_eq line 62
  10. lemma OAI.ThresholdParallelRepetition.Resolvent.resolvent_square_le line 67
  11. lemma OAI.ThresholdParallelRepetition.Resolvent.purificationKernel_sub line 76
  12. lemma OAI.ThresholdParallelRepetition.Resolvent.purificationKernel_square_le line 91
  13. lemma OAI.ThresholdParallelRepetition.Resolvent.weighted_resolvent_identity line 109
  14. lemma OAI.ThresholdParallelRepetition.Resolvent.weighted_kernel_square_le line 141
  15. lemma OAI.ThresholdParallelRepetition.Resolvent.scalar_square_integral line 167
  16. lemma OAI.ThresholdParallelRepetition.Resolvent.scalar_entropy_integral line 189