OAI/Probability/ParisiFinite/Law.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Law.

  1. abbrev OAI.SKQAOA.GaussianEdge.law line 46
  2. lemma OAI.SKQAOA.GaussianEdge.integral_sq line 48
  3. lemma OAI.SKQAOA.GaussianEdge.integrable_sq line 53
  4. lemma OAI.SKQAOA.GaussianEdge.integral_neg_comp line 56
  5. lemma OAI.SKQAOA.GaussianEdge.integral_zero_of_odd line 61
  6. lemma OAI.SKQAOA.GaussianEdge.integral_sq_bound line 68
  7. def OAI.SKQAOA.GaussianEdge.trigWord line 82
  8. lemma OAI.SKQAOA.GaussianEdge.continuous_trigWord line 85
  9. lemma OAI.SKQAOA.GaussianEdge.trigWord_neg line 89
  10. lemma OAI.SKQAOA.GaussianEdge.abs_prod_le_one line 95
  11. lemma OAI.SKQAOA.GaussianEdge.abs_trigWord_le_one line 100
  12. lemma OAI.SKQAOA.GaussianEdge.abs_trigWord_le_subpattern line 108
  13. lemma OAI.SKQAOA.GaussianEdge.abs_trigWord_le_one_sine line 120
  14. lemma OAI.SKQAOA.GaussianEdge.abs_trigWord_le_two_sines line 127
  15. lemma OAI.SKQAOA.GaussianEdge.abs_prod_sub_one_le line 141
  16. lemma OAI.SKQAOA.GaussianEdge.abs_cos_sub_one_le_sq line 156
  17. lemma OAI.SKQAOA.GaussianEdge.abs_trigWord_empty_sub_one line 165
  18. lemma OAI.SKQAOA.GaussianEdge.integral_trigWord_odd line 178
  19. lemma OAI.SKQAOA.GaussianEdge.integral_marked_trigWord_even line 186
  20. lemma OAI.SKQAOA.GaussianEdge.integral_trigWord_two_sines line 193
  21. lemma OAI.SKQAOA.GaussianEdge.integral_marked_trigWord_one_sine line 199
  22. lemma OAI.SKQAOA.GaussianEdge.integral_trigWord_empty_sub_one line 210
  23. theorem OAI.ClassicalGaussian.integrable_real_pow line 225
  24. theorem OAI.ClassicalGaussian.integrable_standard_pow line 231
  25. theorem OAI.ClassicalGaussian.standard_fourth line 238
  26. theorem OAI.ClassicalGaussian.memLp_field_nat line 251
  27. theorem OAI.ClassicalGaussian.integrable_field_pow line 254
  28. theorem OAI.ClassicalGaussian.field_fourth line 260
  29. theorem OAI.ClassicalGaussian.field_add line 293
  30. theorem OAI.ClassicalGaussian.field_sub line 298
  31. theorem OAI.ClassicalGaussian.memLp_field_product line 302
  32. theorem OAI.ClassicalGaussian.integrable_field_four line 309
  33. theorem OAI.ClassicalGaussian.polarization line 314
  34. theorem OAI.ClassicalGaussian.fourth_norm line 320
  35. theorem OAI.ClassicalGaussian.field_wick_four line 325
  36. def OAI.ClassicalGaussian.centeredQuadratic line 373
  37. theorem OAI.ClassicalGaussian.memLp_centeredQuadratic line 376
  38. theorem OAI.ClassicalGaussian.integral_centeredQuadratic line 380
  39. theorem OAI.ClassicalGaussian.covariance_centeredQuadratic line 389
  40. theorem OAI.ClassicalGaussian.quadratic_sum_variance line 415
  41. theorem OAI.ClassicalGaussian.quadratic_sum_variance_le line 443
  42. def OAI.ClassicalGaussian.phaseError line 472
  43. theorem OAI.ClassicalGaussian.phaseError_nonneg line 475
  44. theorem OAI.ClassicalGaussian.continuous_phaseError line 477
  45. theorem OAI.ClassicalGaussian.phaseError_le_sq line 481
  46. theorem OAI.ClassicalGaussian.phaseError_le_four line 486
  47. theorem OAI.ClassicalGaussian.integrable_phaseError line 497
  48. theorem OAI.ClassicalGaussian.integral_phaseError_le line 506
  49. theorem OAI.ClassicalGaussian.quadratic_phase_L2_le line 517
  50. theorem OAI.ClassicalGaussian.weighted_bounded_integral_tendsto line 541
  51. theorem OAI.ClassicalGaussian.phase_weighted_L2_tendsto line 577
  52. theorem OAI.ClassicalGaussian.phase_vector_L2_tendsto line 591
  53. theorem OAI.OrthogonalKernels.norm_sum_sq line 620
  54. theorem OAI.OrthogonalKernels.tensor_sum_norm_sq line 641
  55. theorem OAI.OrthogonalKernels.tensor_sum_norm_sq_le line 651
  56. theorem OAI.OrthogonalKernels.rankOne_sum_apply_sq_le line 665
  57. theorem OAI.OrthogonalKernels.rankOne_sum_norm_le line 683