OAI/Analysis/CircleDomains/Modulus/FiniteCircleBarrierCollapse.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Collapse from vanishing finite-circle barriers

The proved finite-hole line estimate rules out a fixed positive-length set of crossings when both the actual gradient norms and terminal oscillation norms vanish. This is the analytic contradiction used for unmarked limiting complementary components.

  1. theorem OAI.CircleDomainRigidity.measure_zero_of_vanishing_finite_circle_barriers line 22
  2. theorem OAI.CircleDomainRigidity.subsingleton_of_zero_projection_measure line 71