OAI/NumberTheory/Ostmann/Construction/FrozenNonbulkPrior.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Freeze nonbulk data while resampling the original product law

  1. theorem OAI.Ostmann.finiteCoordinatePriors_frozen line 11
  2. theorem OAI.Ostmann.finite_prior_frozen_mean line 29
  3. theorem OAI.Ostmann.bulkCoordinateInsert_update_base line 38