OAI/Probability/EntangledGames/CoherentFilters.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_mul_contraction line 22
  2. def OAI.ThresholdParallelRepetition.QuantumSampling.rightAbs line 30
  3. def OAI.ThresholdParallelRepetition.QuantumSampling.polar line 31
  4. lemma OAI.ThresholdParallelRepetition.QuantumSampling.rightAbs_pos line 33
  5. lemma OAI.ThresholdParallelRepetition.QuantumSampling.rightAbs_sq line 35
  6. lemma OAI.ThresholdParallelRepetition.QuantumSampling.supportInverse_mul_le_one line 38
  7. lemma OAI.ThresholdParallelRepetition.QuantumSampling.polar_gram line 51
  8. lemma OAI.ThresholdParallelRepetition.QuantumSampling.polar_contraction line 67
  9. lemma OAI.ThresholdParallelRepetition.QuantumSampling.polar_mul_rightAbs line 71
  10. lemma OAI.ThresholdParallelRepetition.QuantumSampling.supportInverse_bin line 84
  11. lemma OAI.ThresholdParallelRepetition.QuantumSampling.polar_gram_bin line 103
  12. lemma OAI.ThresholdParallelRepetition.QuantumSampling.projection_le_one line 116
  13. def OAI.ThresholdParallelRepetition.QuantumSampling.binFilter line 124
  14. lemma OAI.ThresholdParallelRepetition.QuantumSampling.binFilter_gram line 127
  15. lemma OAI.ThresholdParallelRepetition.QuantumSampling.binFilter_contraction line 145
  16. def OAI.ThresholdParallelRepetition.QuantumSampling.roundedAbs line 159
  17. lemma OAI.ThresholdParallelRepetition.QuantumSampling.roundedAbs_energy_le line 161
  18. lemma OAI.ThresholdParallelRepetition.QuantumSampling.roundedAbs_error_le line 168
  19. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_neg line 191
  20. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_sub_comm line 193
  21. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_smul line 195
  22. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_add_le line 200
  23. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_sum_orthogonal line 209
  24. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_mul_right_contraction line 221
  25. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_mul_projection_le line 227
  26. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_orthogonal_projection_sum line 235
  27. def OAI.ThresholdParallelRepetition.QuantumSampling.CoversBins line 255
  28. lemma OAI.ThresholdParallelRepetition.QuantumSampling.sum_binScale_indicator line 258
  29. lemma OAI.ThresholdParallelRepetition.QuantumSampling.roundedAbs_eq_sum line 267
  30. lemma OAI.ThresholdParallelRepetition.QuantumSampling.exists_common_bins line 283
  31. def OAI.ThresholdParallelRepetition.QuantumSampling.crossBins line 295
  32. def OAI.ThresholdParallelRepetition.QuantumSampling.binMismatch line 298
  33. lemma OAI.ThresholdParallelRepetition.QuantumSampling.crossBins_error_le line 301
  34. lemma OAI.ThresholdParallelRepetition.QuantumSampling.polar_crossBins_error_le line 316
  35. def OAI.ThresholdParallelRepetition.QuantumSampling.vec line 346
  36. def OAI.ThresholdParallelRepetition.QuantumSampling.eval line 348
  37. def OAI.ThresholdParallelRepetition.QuantumSampling.prob line 351
  38. lemma OAI.ThresholdParallelRepetition.QuantumSampling.eval_eq_sum line 354
  39. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_nonneg line 359
  40. lemma OAI.ThresholdParallelRepetition.QuantumSampling.eval_add_left line 363
  41. lemma OAI.ThresholdParallelRepetition.QuantumSampling.eval_add_right line 366
  42. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_add_left line 369
  43. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_add_right line 372
  44. lemma OAI.ThresholdParallelRepetition.QuantumSampling.eval_one line 376
  45. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_one line 384
  46. lemma OAI.ThresholdParallelRepetition.QuantumSampling.eval_real line 387
  47. lemma OAI.ThresholdParallelRepetition.QuantumSampling.eval_eq_trace line 394
  48. lemma OAI.ThresholdParallelRepetition.QuantumSampling.eval_kronecker line 405
  49. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_kronecker line 411
  50. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_kronecker line 419
  51. lemma OAI.ThresholdParallelRepetition.QuantumSampling.eval_pullback line 426
  52. lemma OAI.ThresholdParallelRepetition.QuantumSampling.prob_pullback line 435