OAI/Analysis/CircleDomains/Rigidity/SelectableMaskedCoordinate.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The selected coordinate retains the precise level and flag data needed for a later endpoint-law construction. Weighted coarea is proved for the actual physical mean before placing it in this interface.

  1. structure OAI.CircleDomainRigidity.SelectableMaskedCoordinate line 19
  2. def OAI.CircleDomainRigidity.SelectableMaskedCoordinate.CompatibleWith line 38
  3. theorem OAI.CircleDomainRigidity.SelectableMaskedCoordinate.CompatibleWith.mono line 46
  4. def OAI.CircleDomainRigidity.SelectableMaskedCoordinate.priorLevels line 51
  5. def OAI.CircleDomainRigidity.SelectableMaskedCoordinate.pathData line 57
  6. theorem OAI.CircleDomainRigidity.SelectableMaskedCoordinate.point_bound line 60
  7. theorem OAI.CircleDomainRigidity.SelectableMaskedCoordinate.weight_finite line 65
  8. theorem OAI.CircleDomainRigidity.SelectableMaskedCoordinate.common_flags line 69
  9. theorem OAI.CircleDomainRigidity.SelectableMaskedCoordinate.unique_free_trace line 79
  10. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.domain_fiber_subsingleton line 87
  11. theorem OAI.CircleDomainRigidity.SelectableMaskedCoordinate.exists_of_mean line 99
  12. theorem OAI.CircleDomainRigidity.SelectableMaskedCoordinate.exists_of_real line 132