OAI/Probability/PosteriorReplicas/Information/BinCutoff.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PosteriorReplicas.binCutoff line 10
2. lemma OAI.PosteriorReplicas.real_pow_cutoff line 12
3. lemma OAI.PosteriorReplicas.binCutoff_bound line 40
4. lemma OAI.PosteriorReplicas.binCutoff_valid line 48
5. lemma OAI.PosteriorReplicas.binCutoff_log_bound line 57