OAI/Analysis/CircleDomains/Modulus/LoopOscillationMinimum.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Minimizing a uniformly convergent sum of interval oscillations. Every nonconstant loop can strictly decrease one term without increasing any other term.

  1. def OAI.CircleDomainRigidity.pathTestInterval line 20
  2. def OAI.CircleDomainRigidity.loopOscillationTerm line 23
  3. def OAI.CircleDomainRigidity.loopOscillationCost line 26
  4. lemma OAI.CircleDomainRigidity.loopOscillationTerm_nonneg line 29
  5. lemma OAI.CircleDomainRigidity.loopOscillationTerm_le line 33
  6. lemma OAI.CircleDomainRigidity.summable_loopOscillationTerm line 37
  7. lemma OAI.CircleDomainRigidity.continuous_loopOscillationCost line 42
  8. lemma OAI.CircleDomainRigidity.loopOscillationCost_erase_lt line 50
  9. lemma OAI.CircleDomainRigidity.exists_loopOscillation_minimum line 73