OAI/Analysis/CircleDomains/Probability/CompactMeasureContinuity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Continuity of pointwise modulus on decreasing compact measure families avoiding zero. The limiting probability plan supplies the lower bound.

  1. lemma OAI.CircleDomainRigidity.compact_intersection_modulus_lower line 14