OAI/Probability/ParisiFinite/ScalarPhase.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Scalar Phase.

  1. def OAI.ClassicalGaussian.scalarPhase line 51
  2. theorem OAI.ClassicalGaussian.norm_scalarPhase line 53
  3. theorem OAI.ClassicalGaussian.continuous_scalarPhase line 56
  4. theorem OAI.ClassicalGaussian.memLp_phase_smul line 60
  5. def OAI.ClassicalGaussian.phaseMultiplier line 71
  6. theorem OAI.ClassicalGaussian.phaseMultiplier_ae line 100
  7. theorem OAI.ClassicalGaussian.scalarPhase_zero line 105
  8. theorem OAI.ClassicalGaussian.scalarPhase_add line 108
  9. theorem OAI.ClassicalGaussian.phaseMultiplier_zero line 112
  10. theorem OAI.ClassicalGaussian.phaseMultiplier_add line 118
  11. def OAI.ClassicalGaussian.phaseUnitary line 128
  12. theorem OAI.ClassicalGaussian.phaseUnitary_apply line 135
  13. theorem OAI.ClassicalGaussian.L2_norm_sq_integral line 138
  14. theorem OAI.ClassicalGaussian.phaseMultiplier_tendsto line 146
  15. theorem OAI.StrongIsometryContexts.apply_varying line 184
  16. theorem OAI.StrongIsometryContexts.comp line 198
  17. def OAI.StrongIsometryContexts.word line 206
  18. theorem OAI.StrongIsometryContexts.word_tendsto line 212
  19. theorem OAI.StrongIsometryContexts.phase_in_context line 221
  20. def OAI.ClassicalGaussian.Shifted.form line 244
  21. def OAI.ClassicalGaussian.Shifted.kernel line 247
  22. def OAI.ClassicalGaussian.Shifted.kernelSq line 250
  23. theorem OAI.ClassicalGaussian.Shifted.kernelSq_nonneg line 254
  24. theorem OAI.ClassicalGaussian.Shifted.kernelSq_swap line 258
  25. theorem OAI.ClassicalGaussian.Shifted.field_kernel line 263
  26. theorem OAI.ClassicalGaussian.Shifted.form_translate line 268
  27. theorem OAI.ClassicalGaussian.Shifted.memLp_form line 281
  28. theorem OAI.ClassicalGaussian.Shifted.memLp_form_translate line 285
  29. theorem OAI.ClassicalGaussian.Shifted.form_second_moment_le line 291
  30. theorem OAI.ClassicalGaussian.Shifted.kernel_apply_sq_le line 305
  31. theorem OAI.ClassicalGaussian.Shifted.kernel_pairing_sq_le line 311
  32. theorem OAI.ClassicalGaussian.Shifted.translated_second_moment_le line 323
  33. abbrev OAI.GaussianCoherent.Quadratic.RealMode line 375
  34. theorem OAI.GaussianCoherent.Quadratic.coordinate_preserving line 379
  35. def OAI.GaussianCoherent.Quadratic.symbol line 384
  36. theorem OAI.GaussianCoherent.Quadratic.memLp_symbol line 387
  37. theorem OAI.GaussianCoherent.Quadratic.symbol_second_moment_le line 392
  38. def OAI.GaussianCoherent.Quadratic.unitary line 407
  39. theorem OAI.GaussianCoherent.Quadratic.gaussian_unitary_apply line 412
  40. theorem OAI.GaussianCoherent.Quadratic.unitary_coherent_ae line 422
  41. theorem OAI.GaussianCoherent.Quadratic.unitary_zero line 431
  42. theorem OAI.GaussianCoherent.Quadratic.unitary_add line 436
  43. theorem OAI.GaussianCoherent.Quadratic.unitary_tendsto line 444
  44. def OAI.GaussianFourier.dot line 471
  45. theorem OAI.GaussianFourier.integrable_real_exp_dot line 473
  46. theorem OAI.GaussianFourier.integral_real_exp_dot line 481
  47. theorem OAI.GaussianFourier.linear_eq_dot line 489
  48. theorem OAI.GaussianFourier.charFunDual_eq_dot line 502
  49. theorem OAI.GaussianFourier.tilted_dot_eq_map_add line 518
  50. theorem OAI.GaussianFourier.integral_exp_dot_mul line 550
  51. def OAI.GaussianCoherent.realShift line 573
  52. theorem OAI.GaussianCoherent.realShift_complex line 575
  53. theorem OAI.GaussianCoherent.offset_shift line 579
  54. theorem OAI.GaussianCoherent.norm_wave_sq line 589
  55. theorem OAI.GaussianCoherent.coherent_tilt_integral line 606
  56. theorem OAI.GaussianCoherent.Quadratic.continuous_symbol line 624
  57. theorem OAI.GaussianCoherent.Quadratic.memLp_symbol_translate line 630
  58. theorem OAI.GaussianCoherent.Quadratic.translated_symbol_second_moment_le line 636
  59. theorem OAI.GaussianCoherent.Quadratic.coherent_error_integral line 654
  60. theorem OAI.GaussianCoherent.Quadratic.coherent_error_sq_le line 681