OAI/Probability/PosteriorReplicas/Information/ReplicaCost.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.gaussianMomentConstant_log_le line 10
2. lemma OAI.PosteriorReplicas.wishartMoment_log_le line 33
3. lemma OAI.PosteriorReplicas.label_unitBall_log_le line 42
4. lemma OAI.PosteriorReplicas.binMeanBound_log_le line 62
5. lemma OAI.PosteriorReplicas.scaled_dimension_log_le line 75
6. lemma OAI.PosteriorReplicas.comparisonCost_le line 82