OAI/Combinatorics/BalancedRyser/Candidates/OppositeAssembly.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.OppositeAssembly.meanBound line 15
  2. theorem OAI.Balanced.OppositeAssembly.meanBound_nonneg line 18
  3. theorem OAI.Balanced.OppositeAssembly.meanBound_mono line 20
  4. theorem OAI.Balanced.OppositeAssembly.witnesses_mean_le line 24
  5. theorem OAI.Balanced.OppositeAssembly.witness_mem_iff_of_agree line 58
  6. def OAI.Balanced.OppositeAssembly.witnessPatternModel line 74
  7. theorem OAI.Balanced.OppositeAssembly.witnessPatternModel_support_card line 84
  8. theorem OAI.Balanced.OppositeAssembly.witnessPatternModel_count line 92
  9. theorem OAI.Balanced.OppositeAssembly.witnessPatternModel_fixedExpectation line 103
  10. theorem OAI.Balanced.OppositeAssembly.witnessPatternModel_fixed_count_le line 123
  11. theorem OAI.Balanced.OppositeAssembly.witnesses_moment_le line 131