OAI/Probability/ParisiFinite/Sine.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Sine.

  1. def OAI.TrigLp.sine line 29
  2. theorem OAI.TrigLp.sine_ae line 33
  3. theorem OAI.TrigLp.sine_norm_sub_le line 37
  4. theorem OAI.TrigLp.sine_continuous line 42
  5. theorem OAI.TrigLp.sum_ae line 46
  6. def OAI.TrigLp.linear line 58
  7. theorem OAI.TrigLp.linear_ae line 60
  8. theorem OAI.TrigLp.linear_norm_sub_le line 71
  9. def OAI.TrigLp.polynomial line 76
  10. theorem OAI.TrigLp.polynomial_ae line 79
  11. theorem OAI.TrigLp.polynomial_norm_sub_le line 98
  12. theorem OAI.TrigLp.polynomial_continuous line 112
  13. def OAI.GaussianCoherent.linearField line 131
  14. theorem OAI.GaussianCoherent.memLp_linearField line 133
  15. def OAI.GaussianCoherent.fieldVector line 144
  16. theorem OAI.GaussianCoherent.fieldVector_ae line 146
  17. theorem OAI.GaussianCoherent.conj_wave line 150
  18. theorem OAI.GaussianCoherent.conjugate_exponent line 155
  19. theorem OAI.GaussianCoherent.integrable_wave_coord line 166
  20. theorem OAI.GaussianCoherent.integral_wave_coord line 175
  21. theorem OAI.GaussianCoherent.inner_vector_fieldVector line 195
  22. theorem OAI.GaussianCoherent.gaussianUnitary_creationVacuum line 226
  23. theorem OAI.GaussianCoherent.norm_fieldVector line 242
  24. theorem OAI.GaussianCoherent.inner_fieldVector line 246
  25. def OAI.BoundedSeed.truncate line 258
  26. lemma OAI.BoundedSeed.scale_pos line 260
  27. theorem OAI.BoundedSeed.truncate_neg line 262
  28. theorem OAI.BoundedSeed.truncate_bounded line 265
  29. theorem OAI.BoundedSeed.truncate_dominated line 269
  30. theorem OAI.BoundedSeed.truncate_eq_sinc line 276
  31. theorem OAI.BoundedSeed.tendsto_truncate line 284
  32. theorem OAI.BoundedSeed.contDiff_truncate line 292
  33. theorem OAI.BoundedSeed.memLp_truncate line 298
  34. theorem OAI.BoundedSeed.tendsto_error_moment line 306
  35. theorem OAI.BoundedSeed.tendsto_gaussian_error_moment line 335
  36. theorem OAI.TrigLp.pullback_sine line 354
  37. theorem OAI.TrigLp.pullback_polynomial line 371
  38. theorem OAI.TrigLp.exists_local_approx line 382
  39. theorem OAI.TrigLp.exists_robust_local_approx line 398
  40. theorem OAI.FourierDensity.sineOutput_odd line 423
  41. theorem OAI.FourierDensity.sineOutput_bounded line 427
  42. theorem OAI.FourierDensity.sineOutput_contDiff line 430
  43. def OAI.TrigLp.readout line 443
  44. theorem OAI.TrigLp.readout_ae line 446
  45. theorem OAI.TrigLp.readout_norm_sub_le line 457
  46. theorem OAI.TrigLp.readout_continuous line 463
  47. theorem OAI.TrigLp.pullback_readout line 475
  48. theorem OAI.TrigLp.exists_robust_readout line 491
  49. def OAI.TrigLp.inputMap line 525
  50. theorem OAI.TrigLp.measurable_inputMap line 528
  51. def OAI.TrigLp.inputLaw line 531
  52. instance OAI.TrigLp.inputLaw_finite line 533
  53. theorem OAI.TrigLp.inputMap_preserving line 537
  54. theorem OAI.TrigLp.inputLaw_symmetric line 543
  55. theorem OAI.TrigLp.polynomial_odd line 555
  56. theorem OAI.TrigLp.readout_odd line 565
  57. theorem OAI.TrigLp.exists_robust_odd_operation line 579
  58. theorem OAI.TrigLp.exists_robust_odd_readout line 614