OAI/Probability/SKGap/Localization/StandardArrayLaw.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.Regression.standardArrayLaw line 30
  2. instance OAI.SKGapCutoff.Regression.(instance at line 33) line 33
  3. lemma OAI.SKGapCutoff.Regression.coordinate_hasLaw line 37
  4. lemma OAI.SKGapCutoff.Regression.coordinates_independent line 41
  5. lemma OAI.SKGapCutoff.Regression.coordinates_gaussian line 45
  6. lemma OAI.SKGapCutoff.Regression.coordinate_covariance line 49
  7. def OAI.SKGapCutoff.Regression.linearTest line 61
  8. lemma OAI.SKGapCutoff.Regression.linearTest_apply line 64
  9. lemma OAI.SKGapCutoff.Regression.linearTest_covariance line 67
  10. def OAI.SKGapCutoff.Regression.goe line 76
  11. lemma OAI.SKGapCutoff.Regression.goe_symmetric line 79
  12. def OAI.SKGapCutoff.Regression.goeCLM line 83
  13. lemma OAI.SKGapCutoff.Regression.goeCLM_apply line 87
  14. lemma OAI.SKGapCutoff.Regression.goe_gaussian line 93
  15. lemma OAI.SKGapCutoff.Regression.goe_entry_memLp line 100
  16. lemma OAI.SKGapCutoff.Regression.goe_entry_covariance line 104
  17. def OAI.SKGapCutoff.Regression.sandwichCLM line 127
  18. lemma OAI.SKGapCutoff.Regression.sandwichCLM_apply line 135
  19. def OAI.SKGapCutoff.Regression.residualProjection line 139
  20. lemma OAI.SKGapCutoff.Regression.residualProjection_symmetric line 142
  21. lemma OAI.SKGapCutoff.Regression.residualProjection_mul line 146
  22. lemma OAI.SKGapCutoff.Regression.mul_residualProjection line 150
  23. lemma OAI.SKGapCutoff.Regression.regression_decomposition line 154
  24. lemma OAI.SKGapCutoff.Regression.goe_entry_sandwich_covariance line 163
  25. lemma OAI.SKGapCutoff.Regression.goe_sandwich_covariance line 185
  26. lemma OAI.SKGapCutoff.Regression.residual_answer_covariance line 219
  27. def OAI.SKGapCutoff.Regression.entryCLM line 229
  28. lemma OAI.SKGapCutoff.Regression.entryCLM_apply line 234
  29. def OAI.SKGapCutoff.Regression.regressionCLM line 237
  30. lemma OAI.SKGapCutoff.Regression.regressionCLM_apply line 247
  31. lemma OAI.SKGapCutoff.Regression.residual_answer_independent line 257
  32. def OAI.SKGapCutoff.Regression.revealedCompletion line 268
  33. lemma OAI.SKGapCutoff.Regression.revealedCompletion_answer line 272
  34. lemma OAI.SKGapCutoff.Regression.revealedCompletion_symmetric line 280
  35. lemma OAI.SKGapCutoff.Regression.revealedCompletion_residual line 289
  36. lemma OAI.SKGapCutoff.Regression.revealedCompletion_unique line 300
  37. lemma OAI.SKGapCutoff.Regression.regression_factorization line 306