OAI/Probability/SKRatio/Matrices/AugmentedSquares.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatio.Planted.continuous_affineDisorder line 16
  2. lemma OAI.SKRatio.Planted.diagonal_affine_hasLaw line 20
  3. def OAI.SKRatio.Planted.diagonalSquareError line 28
  4. lemma OAI.SKRatio.Planted.continuous_diagonalSquareError line 33
  5. lemma OAI.SKRatio.Planted.diagonal_square_event_measurable line 42
  6. theorem OAI.SKRatio.Planted.planted_weighted_diagonal_rare line 50
  7. def OAI.SKRatio.Planted.augmentedDiagonal line 65
  8. lemma OAI.SKRatio.Planted.augmentedPair_gaussian line 68
  9. lemma OAI.SKRatio.Planted.augmentedDiagonal_independent line 87
  10. def OAI.SKRatio.Planted.diagonalLaw line 99
  11. lemma OAI.SKRatio.Planted.continuous_augmentedDiagonal line 102
  12. instance OAI.SKRatio.Planted.diagonalLaw_probability line 106
  13. lemma OAI.SKRatio.Planted.augmentedPair_hasLaw line 110
  14. lemma OAI.SKRatio.Planted.diagonalField_augmented line 116
  15. theorem OAI.SKRatio.Planted.augmented_weighted_diagonal_rare line 124