OAI/Analysis/CircleDomains/Selection/RebasedLevelPresentations.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Adding a target or prior law changes the code space, but preserves the actual selected coordinates and their real/mean presentations.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateData.rebaseDust line 19
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateData.graph_rebaseDust line 25
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateData.mask_rebaseDust line 31
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateData.physical_rebaseDust line 37
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateData.singular_rebaseDust line 43
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateData.dustWeight_rebaseDust line 49
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateData.width_rebaseDust line 55
  8. def OAI.CircleDomainRigidity.SmoothMeanPeriodData.rebaseDomain line 69
  9. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.graph_rebaseDomain line 75
  10. def OAI.CircleDomainRigidity.RealCoordinatePresentation.rebase line 88
  11. def OAI.CircleDomainRigidity.MeanCoordinatePresentation.rebase line 111
  12. def OAI.CircleDomainRigidity.SelectedLevelPresentation.rebase line 147