OAI/Analysis/CircleDomains/Probability/MeanVisitDensity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The density on a countable cost atom records the actual mean number of preterminal visits. The squared density budget therefore bounds the counting square norm independently of the auxiliary positive weights.

  1. def OAI.CircleDomainRigidity.meanCodePreVisits line 24
  2. theorem OAI.CircleDomainRigidity.atomicVisitMeasure_singleton line 31
  3. theorem OAI.CircleDomainRigidity.atomicReference_singleton line 39
  4. theorem OAI.CircleDomainRigidity.meanCodeAtomic_singleton line 48
  5. theorem OAI.CircleDomainRigidity.meanCodePreVisits_density line 56
  6. theorem OAI.CircleDomainRigidity.meanCodePreVisits_square_budget line 82