OAI/Analysis/CircleDomains/Transfer/RetainedScalarEstimates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Energy and terminal oscillation estimates for the unchanged scalar tests on the actual finite stages of the selected circle model.

  1. theorem OAI.CircleDomainRigidity.intervalFiberHull_value_of_continuousAt line 17
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.CountableRealCoordinates.width_zero_of_continuous line 26
  3. def OAI.CircleDomainRigidity.RetainedRealCircleModel.transferred line 47
  4. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.width_zero line 51
  5. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.eventually_oscillation line 55
  6. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.eventually_energy line 64
  7. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.eventually_retained line 85