OAI/Analysis/CircleDomains/Rigidity/TraceBalloonRadii.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Explicit shrinking balloon radii. The geometric extra radii reserve at least half of every zero-radius balloon after all later deletions.

  1. def OAI.CircleDomainRigidity.traceExtraRadius line 14
  2. theorem OAI.CircleDomainRigidity.traceExtraRadius_pos line 16
  3. theorem OAI.CircleDomainRigidity.traceExtraRadius_sq line 19
  4. theorem OAI.CircleDomainRigidity.traceExtraRadius_summable_sq line 24
  5. theorem OAI.CircleDomainRigidity.traceExtraRadius_tail line 28
  6. def OAI.CircleDomainRigidity.traceBalloonRadius line 35
  7. theorem OAI.CircleDomainRigidity.traceBalloonRadius_pos line 38
  8. theorem OAI.CircleDomainRigidity.traceBalloonRadius_lt line 45
  9. theorem OAI.CircleDomainRigidity.traceBalloonRadius_le_double line 55
  10. theorem OAI.CircleDomainRigidity.traceBalloonRadius_summable_sq line 64
  11. theorem OAI.CircleDomainRigidity.traceBalloonRadius_tendsto line 81
  12. theorem OAI.CircleDomainRigidity.traceBalloonRadius_zero_tail line 90