OAI/Probability/PosteriorReplicas/Geometry/FrameTubes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PosteriorReplicas.baseProjectionConstant line 10
2. lemma OAI.PosteriorReplicas.baseProjectionConstant_pos line 16
3. lemma OAI.PosteriorReplicas.baseDensity_le_sup line 22
4. lemma OAI.PosteriorReplicas.baseDensity_le_orthonormal line 47
5. lemma OAI.PosteriorReplicas.projected_base_measure line 53
6. lemma OAI.PosteriorReplicas.orthonormal_in_orthogonal line 65
7. lemma OAI.PosteriorReplicas.pairing_le_infDist line 73
8. lemma OAI.PosteriorReplicas.base_affine_tube line 85