OAI/Analysis/CircleDomains/Probability/IncreasingMeasureLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Pointwise increasing limits of the finite-stage occupation measures.

  1. theorem OAI.CircleDomainRigidity.tsum_iSup_of_monotone line 15
  2. theorem OAI.CircleDomainRigidity.increasingMeasureLimit_iUnion line 22
  3. def OAI.CircleDomainRigidity.increasingMeasureLimit line 29
  4. theorem OAI.CircleDomainRigidity.increasingMeasureLimit_apply line 33
  5. theorem OAI.CircleDomainRigidity.le_increasingMeasureLimit line 38
  6. theorem OAI.CircleDomainRigidity.measurable_increasingMeasureLimit line 45