OAI/Probability/ParisiFinite/RealShiftNormSqLe.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Real Shift Norm Sq Le.

  1. theorem OAI.GaussianCoherent.realShift_norm_sq_le line 55
  2. def OAI.GaussianCoherent.Quadratic.packetConstant line 68
  3. theorem OAI.GaussianCoherent.Quadratic.packetConstant_nonneg line 70
  4. theorem OAI.GaussianCoherent.Quadratic.coherent_error_sq_le_uniform line 76
  5. theorem OAI.GaussianCoherent.Quadratic.packet_error_le line 96
  6. theorem OAI.GaussianCoherent.Quadratic.varying_dimension_packet_limit line 133
  7. theorem OAI.GaussianCoherent.Quadratic.error_le_packet_error line 158
  8. theorem OAI.ClassicalGaussian.Shifted.kernelSq_le_mass_square line 189
  9. theorem OAI.ClassicalGaussian.Shifted.mass_square_le_max line 200
  10. theorem OAI.ClassicalGaussian.Shifted.kernelSq_le_max_mass line 210
  11. theorem OAI.GaussianCoherent.Quadratic.sender_dilution_limit line 223
  12. def OAI.SKQAOA.stateDistance line 256
  13. theorem OAI.SKQAOA.normSq_sub_abs_le line 258
  14. theorem OAI.SKQAOA.sum_abs_normSq_sub_le line 268
  15. def OAI.SKQAOA.spectralWidth line 288
  16. theorem OAI.SKQAOA.spectralWidth_nonneg line 290
  17. def OAI.SKQAOA.stateEnergy line 298
  18. theorem OAI.SKQAOA.stateEnergy_sub_bound line 301
  19. theorem OAI.SKQAOA.spectralWidth_integrable line 350
  20. theorem OAI.SKQAOA.integral_spectralWidth_div line 354
  21. theorem OAI.SKQAOA.expectedEnergy_sub_bound_of_stateDistance line 371
  22. theorem OAI.SKQAOA.value_sub_bound_of_stateDistance line 395
  23. theorem OAI.SKQAOA.unitary_preserves_stateDistance line 408
  24. theorem OAI.SKQAOA.stateDistance_nonneg line 423
  25. theorem OAI.SKQAOA.stateDistance_le_two line 426
  26. theorem OAI.SKQAOA.qaoaStateDistance_continuous line 443
  27. def OAI.SKQAOA.weightedStateError line 454
  28. theorem OAI.SKQAOA.weightedStateError_integrable line 458
  29. theorem OAI.SKQAOA.expectedEnergy_sub_le_weightedStateError line 475
  30. theorem OAI.SKQAOA.value_eq_of_weightedStateError_tendsto_zero line 497
  31. theorem OAI.ClassicalGaussian.phase_weighted_integral_le line 520
  32. theorem OAI.ClassicalGaussian.phase_varying_weight_limit line 548
  33. theorem OAI.ClassicalGaussian.phaseMultiplier_error_integral line 568
  34. theorem OAI.ClassicalGaussian.phaseMultiplier_varying_limit line 584
  35. theorem OAI.GaussianCoherent.Quadratic.varying_dimension_L4_limit line 610
  36. theorem OAI.SKQAOA.tendsto_integral_groundMaximum_atTop line 648
  37. theorem OAI.SKQAOA.not_bddAbove_integral_groundMaximum line 660