OAI/Probability/SKRatio/Matrices/PlantedGOE.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Planted.augmented line 17
  2. def OAI.SKRatio.Planted.augmentedDisorder line 20
  3. lemma OAI.SKRatio.Planted.augmented_symmetric line 23
  4. lemma OAI.SKRatio.Planted.augmentedDisorder_gaussian line 28
  5. lemma OAI.SKRatio.Planted.augmented_mean line 40
  6. lemma OAI.SKRatio.Planted.augmented_covariance line 47
  7. lemma OAI.SKRatio.Planted.augmentedDisorder_covariance line 57
  8. theorem OAI.SKRatio.Planted.augmentedDisorder_hasLaw line 72
  9. lemma OAI.SKRatio.Planted.coupling_augmentedDisorder line 85
  10. def OAI.SKRatio.Planted.augmentedField line 95
  11. lemma OAI.SKRatio.Planted.augmentedField_gaussian line 98
  12. lemma OAI.SKRatio.Planted.augmentedField_mean line 110
  13. lemma OAI.SKRatio.Planted.augmentedField_covariance line 120
  14. theorem OAI.SKRatio.Planted.augmentedField_law line 134
  15. def OAI.SKRatio.Planted.constantDirection line 146
  16. lemma OAI.SKRatio.Planted.constantDirection_unit line 148
  17. lemma OAI.SKRatio.Planted.constantColumn_unit line 153
  18. def OAI.SKRatio.Planted.fieldProjection line 157
  19. lemma OAI.SKRatio.Planted.augmentedField_query line 160
  20. theorem OAI.SKRatio.Planted.field_residual_independent line 169
  21. lemma OAI.SKRatio.Planted.projected_rows_formula line 184
  22. theorem OAI.SKRatio.Planted.augmented_decomposition line 206