OAI/Combinatorics/SharpRamsey/Exposure/MixtureRealization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLogRamsey.Selection.Law.eq_of_integrals line 12
2. lemma OAI.SharpLogRamsey.ActualPivot.Realization.integral line 30
3. def OAI.SharpLogRamsey.ActualPivot.Realization.mix line 36
4. def OAI.SharpLogRamsey.ActualPivot.Realization.attach line 56
5. lemma OAI.SharpLogRamsey.ActualPivot.Realization.attach_agrees line 75
6. lemma OAI.SharpLogRamsey.Selection.ExposureModel.afterDraw_tagged_map line 92