OAI/NumberTheory/Ostmann/Construction/SelectedInitialPriorBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Probability and point-mass bounds for the selected original half-list

  1. def OAI.Ostmann.selectedInitialHalfPrior line 11
  2. theorem OAI.Ostmann.selected_initial_prior_bounds line 20