OAI/Probability/ParisiFinite/Field.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

Field.

  1. def OAI.ClassicalGaussian.field line 29
  2. theorem OAI.ClassicalGaussian.memLp_field line 31
  3. def OAI.ClassicalGaussian.vector line 34
  4. theorem OAI.ClassicalGaussian.vector_ae line 36
  5. theorem OAI.ClassicalGaussian.field_covariance line 39
  6. theorem OAI.ClassicalGaussian.inner_vector line 45
  7. def OAI.ClassicalGaussian.linearMap line 52
  8. def OAI.ClassicalGaussian.aggregate line 74
  9. theorem OAI.ClassicalGaussian.aggregate_apply line 77
  10. theorem OAI.ClassicalGaussian.norm_aggregate_sub line 79
  11. theorem OAI.ClassicalGaussian.aggregate_centered line 83
  12. theorem OAI.ClassicalGaussian.reflection line 90
  13. theorem OAI.ClassicalGaussian.aggregate_odd line 94
  14. theorem OAI.ClassicalGaussian.field_law line 103
  15. abbrev OAI.ClassicalGaussian.ColumnSpan line 122
  16. instance OAI.ClassicalGaussian.span_finiteDimensional line 124
  17. instance OAI.ClassicalGaussian.span_measurableSpace line 127
  18. instance OAI.ClassicalGaussian.span_borelSpace line 128
  19. def OAI.ClassicalGaussian.column line 131
  20. theorem OAI.ClassicalGaussian.inner_column line 134
  21. theorem OAI.ClassicalGaussian.norm_column_sub line 136
  22. def OAI.ClassicalGaussian.jointColumn line 140
  23. theorem OAI.ClassicalGaussian.jointColumn_covariance line 143
  24. theorem OAI.ClassicalGaussian.jointColumn_centered line 154
  25. theorem OAI.ClassicalGaussian.jointColumn_norm_sub line 158
  26. theorem OAI.ClassicalGaussian.jointColumn_odd line 162
  27. theorem OAI.ClassicalGaussian.projection_gaussian line 179
  28. theorem OAI.ClassicalGaussian.projection_preserving line 188
  29. theorem OAI.ClassicalGaussian.aggregate_pullback line 195
  30. theorem OAI.ClassicalGaussian.exists_robust_gaussian_operation line 219
  31. theorem OAI.ClassicalGaussian.exists_robust_gaussian_angle line 239
  32. theorem OAI.ClassicalGaussian.covariance_field line 267
  33. theorem OAI.ClassicalGaussian.joint_gaussian line 279
  34. theorem OAI.ClassicalGaussian.fields_independent line 286
  35. theorem OAI.ClassicalGaussian.orthogonal_families_independent line 296
  36. theorem OAI.TrigLp.sine_pullback line 323
  37. theorem OAI.TrigLp.polynomial_pullback line 337
  38. theorem OAI.TrigLp.readout_pullback line 343
  39. def OAI.TrigLp.coefficientBound line 351
  40. theorem OAI.TrigLp.coefficientBound_nonneg line 354
  41. theorem OAI.TrigLp.polynomial_norm_sub_uniform line 358
  42. def OAI.ClassicalGaussian.localValue line 382
  43. theorem OAI.ClassicalGaussian.exists_ambient_robust_operation line 391
  44. theorem OAI.ClassicalGaussian.exists_ambient_robust_angle line 454
  45. def OAI.FiniteOccupations.weight line 515
  46. theorem OAI.FiniteOccupations.card_pos line 518
  47. theorem OAI.FiniteOccupations.star_weight line 523
  48. theorem OAI.FiniteOccupations.card_mul_weight_sq line 527
  49. theorem OAI.FiniteOccupations.weight_ne_zero line 536
  50. def OAI.FiniteOccupations.liftLinear line 542
  51. theorem OAI.FiniteOccupations.liftLinear_apply line 548
  52. theorem OAI.FiniteOccupations.inner_lift line 552
  53. def OAI.FiniteOccupations.lift line 568
  54. theorem OAI.FiniteOccupations.lift_apply line 571
  55. theorem OAI.FiniteOccupations.mem_range_iff line 575
  56. def OAI.FiniteTensorOccupations.counts line 597
  57. theorem OAI.FiniteTensorOccupations.counts_eq_iff line 600
  58. def OAI.FiniteTensorOccupations.occupancySetoid line 617
  59. abbrev OAI.FiniteTensorOccupations.Occupation line 622
  60. instance OAI.FiniteTensorOccupations.(instance at line 625) line 625
  61. instance OAI.FiniteTensorOccupations.(instance at line 627) line 627
  62. def OAI.FiniteTensorOccupations.register line 629
  63. theorem OAI.FiniteTensorOccupations.register_eq_iff line 632
  64. theorem OAI.FiniteTensorOccupations.register_surjective line 636
  65. def OAI.FiniteTensorOccupations.embedding line 642
  66. theorem OAI.FiniteTensorOccupations.mem_range_iff_symmetric line 647
  67. def OAI.FiniteTensorOccupations.symmetricSector line 662
  68. def OAI.FiniteTensorOccupations.symmetricEmbedding line 669
  69. theorem OAI.FiniteTensorOccupations.symmetricEmbedding_surjective line 675
  70. def OAI.FiniteTensorOccupations.occupationMap line 685
  71. theorem OAI.FiniteTensorOccupations.occupationMap_symm_apply line 689