OAI/Analysis/CircleDomains/Selection/ResidualConstraints.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The rational-interval residual constraints in the allowed path definition are Borel. The incidence side uses the actual prior law or level measure; the toll side retains parameter multiplicity after each finite deletion.

  1. abbrev OAI.CircleDomainRigidity.RationalPathTime line 17
  2. def OAI.CircleDomainRigidity.RationalPathTime.toTime line 19
  3. def OAI.CircleDomainRigidity.deletedWeight line 25
  4. theorem OAI.CircleDomainRigidity.countable_support_deletedWeight line 28
  5. def OAI.CircleDomainRigidity.ResidualIncidenceBound line 43
  6. theorem OAI.CircleDomainRigidity.measurableSet_residualIncidenceBound line 48
  7. def OAI.CircleDomainRigidity.ResidualConstraintFamily line 56
  8. theorem OAI.CircleDomainRigidity.measurableSet_residualConstraintFamily line 62