OAI/Probability/PosteriorReplicas/Learners/HaarLawIdentification.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.gramSchmidt_linearIsometry line 10
2. lemma OAI.PosteriorReplicas.gramSchmidtNormed_linearIsometry line 23
3. lemma OAI.PosteriorReplicas.gaussianRows_orthogonal_invariant line 29
4. lemma OAI.PosteriorReplicas.haarRows_orthogonal_invariant line 35
5. lemma OAI.PosteriorReplicas.haarRows_ae_orthonormal line 49