OAI/Analysis/CircleDomains/Selection/ShrinkingJumpTolls.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Square-summable dust tolls are upper semicontinuous in every T1 topology. Consequently, the supremum toll on shrinking jump neighborhoods has limit superior at most the toll at the limiting dust point.

  1. theorem OAI.CircleDomainRigidity.finite_toll_superlevel line 21
  2. theorem OAI.CircleDomainRigidity.square_summable_toll_upperSemicontinuous line 28
  3. def OAI.CircleDomainRigidity.neighborhoodTollSup line 36
  4. theorem OAI.CircleDomainRigidity.eventually_neighborhoodTollSup_le line 39
  5. theorem OAI.CircleDomainRigidity.shrinking_jump_toll_limsup line 48