OAI/Probability/FreeIsing/Conditioning/GaussianVector.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.ConditionalGaussianVector.map_restrict_eq_smul_of_condExp_inner_character line 19
  2. theorem OAI.Problem367.ConditionalGaussianVector.law_and_indep_of_condExp_inner_character line 46
  3. theorem OAI.Problem367.ConditionalGaussianVector.charFun_product_gaussian line 73
  4. theorem OAI.Problem367.ConditionalGaussianVector.product_gaussian_law_and_indep_of_condExp_linear_character line 80
  5. theorem OAI.Problem367.ConditionalGaussianVector.condExp_linear_character_of_unit_character line 110
  6. theorem OAI.Problem367.ConditionalGaussianVector.condExp_weighted_character_of_unit_character line 156
  7. theorem OAI.Problem367.ConditionalGaussianVector.product_gaussian_law_and_indep_of_condExp_unit_character line 174
  8. theorem OAI.Problem367.ConditionalGaussianVector.infinite_product_gaussian_law_and_indep_of_condExp_linear_character line 192