OAI/Probability/PosteriorReplicas/Information/HaarInformationEq.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.measurable_gramSchmidtNormed_rows line 11
2. instance OAI.PosteriorReplicas.haarRows_probability line 15
3. lemma OAI.PosteriorReplicas.cmi_attachSide_equiv line 19
4. lemma OAI.PosteriorReplicas.cmi_labels_gramSchmidtNormed line 51
5. lemma OAI.PosteriorReplicas.cmi_haar_eq_gaussian line 62