OAI/Analysis/CircleDomains/Transfer/RetainedScalarTails.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual retained planar exhaustion has vanishing original energy outside it. The same finite models transfer this tail estimate to the target.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.realPlane line 18
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.realPlane_open line 20
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.realPlane_monotone line 23
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.realPlane_core line 25
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.iUnion_realPlane line 30
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.source_energy_tail_tendsto line 46
  7. def OAI.CircleDomainRigidity.RetainedRealCircleModel.targetTail line 81
  8. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.eventually_tail_energy_bound line 85
  9. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.tail_energy_tendsto line 109