OAI/Probability/BinarySweep/TensorBounds/TypeMass.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.Density.factorial_mode line 13
  2. lemma OAI.BinaryCoordinateSweeps.Density.multinomial_mode line 33
  3. lemma OAI.BinaryCoordinateSweeps.Density.card_types_le line 51
  4. theorem OAI.BinaryCoordinateSweeps.Density.type_mass_lower_nat line 68
  5. theorem OAI.BinaryCoordinateSweeps.Density.type_mass_lower line 84
  6. def OAI.BinaryCoordinateSweeps.Density.wordCounts line 106
  7. lemma OAI.BinaryCoordinateSweeps.Density.wordCounts_apply line 109
  8. lemma OAI.BinaryCoordinateSweeps.Density.wordCounts_fiber line 114
  9. lemma OAI.BinaryCoordinateSweeps.Density.wordCounts_total line 119
  10. lemma OAI.BinaryCoordinateSweeps.Density.wordCounts_sum line 124
  11. lemma OAI.BinaryCoordinateSweeps.Density.prod_wordCounts line 130
  12. lemma OAI.BinaryCoordinateSweeps.Density.wordCounts_comp line 138
  13. lemma OAI.BinaryCoordinateSweeps.Density.exists_perm_eq_of_wordCounts line 143
  14. lemma OAI.BinaryCoordinateSweeps.Density.word_polynomial line 155
  15. lemma OAI.BinaryCoordinateSweeps.Density.card_words_counts line 168
  16. lemma OAI.BinaryCoordinateSweeps.Density.card_words_counts_fun line 177