OAI/Combinatorics/BalancedRyser/Incidence/PartialIncidenceCounts.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.Balanced.PartialAlignment.IncidenceCodeline 12 - def
OAI.Balanced.PartialAlignment.transverseHitCodesline 15 - def
OAI.Balanced.PartialAlignment.transverseHitCodeProbabilityline 20 - theorem
OAI.Balanced.PartialAlignment.card_transverseHitCodes_one_leline 29 - theorem
OAI.Balanced.PartialAlignment.transverseHitCodeProbability_one_leline 41 - theorem
OAI.Balanced.PartialAlignment.sum_transverseHitCodeProbability_one_leline 53