OAI/Combinatorics/SharpRamsey/Exposure/SourceExposure.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpLogRamsey.Selection.ExposureModel.contextual_remainingline 17 - lemma
OAI.SharpLogRamsey.Selection.ExposureModel.contextual_positiveline 23 - lemma
OAI.SharpLogRamsey.Selection.ExposureModel.contextual_bad_meanline 30 - lemma
OAI.SharpLogRamsey.Selection.ExposureModel.contextual_selected_meanline 40 - lemma
OAI.SharpLogRamsey.Selection.ExposureModel.contextual_unownedline 49 - theorem
OAI.SharpLogRamsey.Selection.actual_realized_reciprocalline 59