OAI/Analysis/CircleDomains/Probability/BorelDensityBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Borel density budgets for measurable families of finite measures. The finite mass cap lets us use the jointly measurable kernel Radon–Nikodym derivative in Mathlib.

  1. def OAI.CircleDomainRigidity.BoundedDensityBudget line 19
  2. theorem OAI.CircleDomainRigidity.measurableSet_boundedDensityBudget line 23