OAI/NumberTheory/Ostmann/Construction/SmoothGiantAmbientPrior.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The full smooth giant law inside an ambient prime set

  1. theorem OAI.Ostmann.smoothGiantMass_ambient line 9
  2. theorem OAI.Ostmann.smoothGiantPrior_ambient_zero line 21
  3. theorem OAI.Ostmann.smoothGiantPrior_ambient_mean line 30