OAI/Probability/PosteriorReplicas/Information/HeadlineInformation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.priorLog_le_dimension_add_log line 10
2. lemma OAI.PosteriorReplicas.priorLog_le_dimension_add_div line 19
3. theorem OAI.PosteriorReplicas.gaussianReplicaBlock line 31
4. theorem OAI.PosteriorReplicas.distanceReplicaBlock line 52
5. theorem OAI.PosteriorReplicas.syntheticReplicaBlock line 68
6. theorem OAI.PosteriorReplicas.incidenceReplicaBlock line 87