OAI/Probability/FreeIsing/Gaussian/ArrayCharacterization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.GaussianArrayCharacterization.isGaussianProcess_array_of_finite_coordinate_processes line 13
  2. theorem OAI.Problem367.GaussianArrayCharacterization.gaussianPi_law_and_indep_of_weighted_characters line 34
  3. theorem OAI.Problem367.GaussianArrayCharacterization.isGaussianProcess_vector_of_conditional_weighted_characters line 53
  4. theorem OAI.Problem367.GaussianArrayCharacterization.isGaussianProcess_array_of_conditional_finite_characters line 96
  5. theorem OAI.Problem367.GaussianArrayCharacterization.conditional_character_coordinate line 118
  6. theorem OAI.Problem367.GaussianArrayCharacterization.preBrownian_coordinate_of_conditional_finite_characters line 136
  7. theorem OAI.Problem367.GaussianArrayCharacterization.law_finite_coordinates_of_conditional_finite_characters line 150
  8. theorem OAI.Problem367.GaussianArrayCharacterization.covariance_coordinate_ne_of_gaussianPi_law line 175
  9. theorem OAI.Problem367.GaussianArrayCharacterization.crossCovariance_of_conditional_finite_characters line 188
  10. theorem OAI.Problem367.GaussianArrayCharacterization.map_brownianArray_eq_infinitePi_of_conditional_finite_characters line 229
  11. theorem OAI.Problem367.GaussianArrayCharacterization.map_continuousBrownianArray_eq_infinitePi_of_conditional_finite_characters line 249