OAI/Analysis/CircleDomains/Selection/MixedSequenceRetention.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Every fixed coordinate is eventually retained, with its actual values and differential, on every compact source set of the common model sequence.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.MixedModelExhaustion.coordinateIndex line 25
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.MixedModelExhaustion.coordinateIndex_eventually line 30
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.MixedModelExhaustion.eventually_coordinate_eq line 37
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.MixedModelExhaustion.eventually_coordinate_values line 49
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.MixedModelExhaustion.eventually_coordinate_gradient line 54
  6. def OAI.CircleDomainRigidity.FiniteTransfer.MixedModelExhaustion.withRadius line 61