OAI/Analysis/CircleDomains/Rigidity/TracePrimitivePlateau.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

On an indexed component neighborhood an active zero cutoff fixes the upper endpoint of the primitive. Late intervals absorbed by that same zero interval have no effect, so the infinite masked scalar is locally an actual finite continuous primitive, even when the raw scalar jumps.

  1. theorem OAI.CircleDomainRigidity.infiniteTraceMask_zero_of_active line 14
  2. theorem OAI.CircleDomainRigidity.infiniteTracePrimitive_plateau line 23
  3. theorem OAI.CircleDomainRigidity.infiniteTraceMask_absorbed_tail line 39
  4. theorem OAI.CircleDomainRigidity.infiniteTracePrimitive_absorbed_tail line 51
  5. theorem OAI.CircleDomainRigidity.indexed_masked_scalar_continuousAt line 60