OAI/NumberTheory/Ostmann/Construction/FiniteProductBins.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Construction.dependentProductPrior_mean line 10
2. theorem OAI.Ostmann.Construction.dependentProductPrior_mean_lower line 18
3. theorem OAI.Ostmann.Construction.finitePrior_logCell_partition line 28
4. theorem OAI.Ostmann.Construction.exists_finitePrior_logCell line 44