OAI/Analysis/CircleDomains/Probability/CountableVisitNorm.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Restoring the terminal visit adds at most one to the counting square norm. The estimate is independent of the auxiliary positive atomic weights.

  1. def OAI.CircleDomainRigidity.countingSquareNorm line 17
  2. theorem OAI.CircleDomainRigidity.countingSquareNorm_mono line 20
  3. theorem OAI.CircleDomainRigidity.countingSquareNorm_add_le line 25
  4. theorem OAI.CircleDomainRigidity.countingSquareNorm_terminal_le line 33
  5. theorem OAI.CircleDomainRigidity.meanVisitCount_codePathLaw_norm line 59
  6. theorem OAI.CircleDomainRigidity.meanVisitCount_codePathLaw_budget line 67