OAI/Analysis/CircleDomains/Probability/DensityMassBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A finite reference measure turns the square-density estimate into the uniform mass cap needed for the Borel family of candidate laws.

  1. def OAI.CircleDomainRigidity.densityMassBound line 17
  2. theorem OAI.CircleDomainRigidity.densityMassBound_lt_top line 20
  3. theorem OAI.CircleDomainRigidity.mass_le_densityMassBound line 26
  4. theorem OAI.CircleDomainRigidity.boundedDensityBudget_of_square_bound line 39