OAI/Analysis/CircleDomains/Topology/BoundaryIndexMean.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Averaging the proved boundary indices against an atomless starting law gives a continuous boundary coordinate with positive period one.

  1. def OAI.CircleDomainRigidity.boundaryIndexMean line 19
  2. lemma OAI.CircleDomainRigidity.measurable_boundaryIndex line 22
  3. lemma OAI.CircleDomainRigidity.boundaryIndex_bound line 27
  4. lemma OAI.CircleDomainRigidity.integrable_boundaryIndex line 35
  5. lemma OAI.CircleDomainRigidity.continuousAt_boundaryIndex line 41
  6. theorem OAI.CircleDomainRigidity.continuous_boundaryIndexMean line 59
  7. theorem OAI.CircleDomainRigidity.boundaryIndexMean_add_one line 78
  8. theorem OAI.CircleDomainRigidity.boundaryIndexMean_eq_cdf_sub_one line 89
  9. theorem OAI.CircleDomainRigidity.boundaryIndexMean_increment_measure line 131