OAI/Probability/EntangledGames/SpectralBins.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThresholdParallelRepetition.QuantumSampling.floor_shift_monotone line 20
  2. lemma OAI.ThresholdParallelRepetition.QuantumSampling.integral_floor_shift line 25
  3. def OAI.ThresholdParallelRepetition.QuantumSampling.separated line 54
  4. lemma OAI.ThresholdParallelRepetition.QuantumSampling.separated_nonneg line 56
  5. lemma OAI.ThresholdParallelRepetition.QuantumSampling.separated_le_one line 57
  6. lemma OAI.ThresholdParallelRepetition.QuantumSampling.separated_symm line 58
  7. lemma OAI.ThresholdParallelRepetition.QuantumSampling.separated_measurable line 60
  8. lemma OAI.ThresholdParallelRepetition.QuantumSampling.separated_integrable line 65
  9. lemma OAI.ThresholdParallelRepetition.QuantumSampling.separated_le_floor_sub line 69
  10. lemma OAI.ThresholdParallelRepetition.QuantumSampling.integral_separated_le line 78
  11. def OAI.ThresholdParallelRepetition.QuantumSampling.binEnvelope line 94
  12. lemma OAI.ThresholdParallelRepetition.QuantumSampling.binEnvelope_nonneg line 97
  13. lemma OAI.ThresholdParallelRepetition.QuantumSampling.binEnvelope_integrable line 102
  14. lemma OAI.ThresholdParallelRepetition.QuantumSampling.log_difference_bound line 106
  15. lemma OAI.ThresholdParallelRepetition.QuantumSampling.logarithmic_envelope_bound line 116
  16. lemma OAI.ThresholdParallelRepetition.QuantumSampling.integral_binEnvelope_le line 139
  17. def OAI.ThresholdParallelRepetition.QuantumSampling.binWeight line 155
  18. lemma OAI.ThresholdParallelRepetition.QuantumSampling.binWeight_nonneg line 158
  19. lemma OAI.ThresholdParallelRepetition.QuantumSampling.binWeight_le line 161
  20. lemma OAI.ThresholdParallelRepetition.QuantumSampling.sub_binWeight_le line 174
  21. lemma OAI.ThresholdParallelRepetition.QuantumSampling.unitary_row_normSq line 201
  22. lemma OAI.ThresholdParallelRepetition.QuantumSampling.unitary_col_normSq line 207
  23. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_cfc_eq line 212
  24. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_eq_sum_eigenvalues_sq line 228
  25. def OAI.ThresholdParallelRepetition.QuantumSampling.overlap line 234
  26. lemma OAI.ThresholdParallelRepetition.QuantumSampling.overlap_nonneg line 238
  27. lemma OAI.ThresholdParallelRepetition.QuantumSampling.overlap_row line 241
  28. lemma OAI.ThresholdParallelRepetition.QuantumSampling.overlap_col line 251
  29. lemma OAI.ThresholdParallelRepetition.QuantumSampling.overlap_distance line 261
  30. lemma OAI.ThresholdParallelRepetition.QuantumSampling.overlap_square_sum_le line 267
  31. lemma OAI.ThresholdParallelRepetition.QuantumSampling.overlap_transport_le line 283
  32. def OAI.ThresholdParallelRepetition.QuantumSampling.spectralEnvelope line 318
  33. lemma OAI.ThresholdParallelRepetition.QuantumSampling.spectralEnvelope_integrable line 321
  34. lemma OAI.ThresholdParallelRepetition.QuantumSampling.integral_spectralEnvelope_le line 328
  35. lemma OAI.ThresholdParallelRepetition.QuantumSampling.hsSq_sqrt_gram line 350
  36. lemma OAI.ThresholdParallelRepetition.QuantumSampling.integral_spectralEnvelope_unit_le line 355
  37. lemma OAI.ThresholdParallelRepetition.QuantumSampling.weighted_sqrt_le line 364
  38. lemma OAI.ThresholdParallelRepetition.QuantumSampling.exists_shift_spectralEnvelope_le line 374
  39. def OAI.ThresholdParallelRepetition.QuantumSampling.binScale line 405
  40. def OAI.ThresholdParallelRepetition.QuantumSampling.binIndicator line 406
  41. lemma OAI.ThresholdParallelRepetition.QuantumSampling.binIndicator_nonneg line 409
  42. lemma OAI.ThresholdParallelRepetition.QuantumSampling.binIndicator_sq line 411
  43. lemma OAI.ThresholdParallelRepetition.QuantumSampling.binIndicator_mul_ne line 413
  44. lemma OAI.ThresholdParallelRepetition.QuantumSampling.sum_binIndicator_weight_sq_le line 418
  45. lemma OAI.ThresholdParallelRepetition.QuantumSampling.scalar_mismatch_le line 429
  46. def OAI.ThresholdParallelRepetition.QuantumSampling.binProjection line 462
  47. lemma OAI.ThresholdParallelRepetition.QuantumSampling.binProjection_hermitian line 465
  48. lemma OAI.ThresholdParallelRepetition.QuantumSampling.binProjection_pos line 468
  49. lemma OAI.ThresholdParallelRepetition.QuantumSampling.binProjection_sq line 472
  50. lemma OAI.ThresholdParallelRepetition.QuantumSampling.binProjection_orthogonal line 481
  51. lemma OAI.ThresholdParallelRepetition.QuantumSampling.binProjection_mismatch_le line 490