OAI/Probability/PosteriorReplicas/Measures/EqualLabelIdentity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.equal_base_measures line 11
2. lemma OAI.PosteriorReplicas.equal_label_base_identity line 24
3. lemma OAI.PosteriorReplicas.equal_label_tilt_identity line 32
4. lemma OAI.PosteriorReplicas.equal_label_tilt_finite line 41
5. theorem OAI.PosteriorReplicas.equalLabelMeasureIdentity line 54